Input/Output Stochastic Automata - Compositionality and Determinism
| Title | Input/Output Stochastic Automata - Compositionality and Determinism |
| Publication Type | Book Chapter |
| Year of Publication | 2016 |
| Authors | D'Argenio, PR, Lee, MD, Monti, RE |
| Editor | Fränzle, M, Markey, N |
| Book Title | Formal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings |
| Series Title | Lecture Notes in Computer Science |
| Volume | 9884 |
| Pagination | 53–68 |
| Publisher | Springer |
| ISBN Number | 978-3-319-44877-0 |
| Abstract | Stochastic automata provide a way to symbolically model systems in which the occurrence time of events may respond to any continuous random variable. We introduce here an input/output variant of stochastic automata that, once the model is closed —i.e., all synchronizations are resolved—, the resulting automaton does not contain non-deterministic choices. This is important since fully probabilistic models are amenable to simulation in the general case and to much more efficient analysis if restricted to Markov models. We present here a theoretical introduction to input/output stochastic automata (IOSA) for which we (i) provide a concrete semantics in terms of non-deterministic labeled Markov processes (NLMP), (ii) prove that bisimulation is a congruence for parallel composition both in NLMP and IOSA, (iii) show that parallel composition commutes in the symbolic and concrete level, and (iv) provide a proof that a closed IOSA is indeed deterministic. |
| URL | http://dx.doi.org/10.1007/978-3-319-44878-7_4 |
| DOI | 10.1007/978-3-319-44878-7_4 |
PDF (Full text):
