Input/Output Stochastic Automata - Compositionality and Determinism

TitleInput/Output Stochastic Automata - Compositionality and Determinism
Publication TypeBook Chapter
Year of Publication2016
AuthorsD'Argenio, PR, Lee, MD, Monti, RE
EditorFränzle, M, Markey, N
Book TitleFormal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings
Series TitleLecture Notes in Computer Science
ISBN Number978-3-319-44877-0
AbstractStochastic 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.
PDF (Full text): 
Powered by Drupal