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.
Supported by ANPCyT PICT-2012-1823 and SeCyT-UNC 05/BP12 and 05/B497.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Strictly speaking, \(\mathcal {P}(\mathcal {I}_1)||\mathcal {P}(\mathcal {I}_2)\) should also contain states of the form \((s,\vec {v}_1)||(\mathsf {init},\vec {v}_2)\) and \((\mathsf {init},\vec {v}_1)||(s,\vec {v}_2)\) with \(s\ne \mathsf {init}\). Nonetheless, these states are not reachable. Thus, we do not consider them since otherwise the result would not be strictly an isomorphism and it would only add irrelevant technical problems to the proof.
- 2.
Note that the domain and image of \(H\!f\) appear apparently inverted. This is necessary in [12] since they only deal with morphisms, and we are following their definitions. In our case, we could have also defined a direct map from \(\varDelta (\mathscr {B}(\mathbf S ))\) to \(\varDelta (\mathscr {B}(\mathbf S '))\) since \(\varDelta f\) is bimeasurable, namely \(H(f^{-1})=(\varDelta (f^{-1}))^{-1}\).
References
Ash, R., Doléans-Dade, C.: Probability and Measure Theory. Academic Press, Cambridge (2000)
Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011)
Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006)
Bravetti, M., D’Argenio, P.R.: Tutte le algebre insieme: concepts, discussions and relations of stochastic process algebras with general distributions. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 44–88. Springer, Heidelberg (2004)
Budde, C.E., D’Argenio, P.R., Hermanns, H.: Rare event simulation with fully automated importance splitting. In: Beltrán, M., Knottenbelt, W.J., Bradley, J.T. (eds.) Computer Performance Engineering. LNCS, vol. 9272, pp. 275–290. Springer International Publishing, Switzerland (2015)
Crouzen, P.: Modularity and Determinism in Compositional Markov Models. Ph.D. thesis, Universität des Saarlandes, Saarbrücken (2014)
D’Argenio, P.R.: Algebras and Automata for Timed and Stochastic Systems. Ph.D. thesis, University of Twente, Enschede (1999)
D’Argenio, P.R., Katoen, J.P.: A theory of stochastic systems part I: stochastic automata. Inf. Comput. 203(1), 1–38 (2005)
D’Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. STTT 17(4), 469–484 (2015)
D’Argenio, P.R., Sánchez Terraf, P., Wolovick, N.: Bisimulations for non-deterministic labelled Markov processes. Math. Struct. Comput. Sci. 22(1), 43–68 (2012)
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002)
Doberkat, E.E., Sánchez Terraf, P.: Stochastic non-determinism and effectivity functions. J. Logic Comput. (2015, to appear). doi:10.1093/logcom/exv049
Gburek, D., Baier, C., Klüppelholz, S.: Composition of stochastic transition systems based on spans and couplings. In: ICALP 2016. LIPICS (2016, to appear)
Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. Lecture Notes in Mathematics, vol. 915, pp. 68–85. Springer, Heidelberg (1982)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995)
Hartmanns, A., Timmer, M.: Sound statistical model checking for MDP using partial order and confluence reduction. STTT 17(4), 429–456 (2015)
Hermanns, H.: Interactive Markov Chains: and the Quest for Quantified Quality. Springer, Heidelberg (2002)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)
Viglizzo, I.: Coalgebras on Measurable Spaces. Ph.D. thesis, Indiana University, Argentina (2005)
Wolovick, N.: Continuous Probability and Nondeterminism in Labeled Transition Systems. Ph.D. thesis, Universidad Nacional de Córdoba, Argentina (2012)
Wu, S., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic I/O automata. Theor. Comput. Sci. 176(1–2), 1–38 (1997)
Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR ’90 Theories of Concurrency: Unification and Extension. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990)
Acknowledgments
We thank Pedro Sánchez Terraf for the help provided in measure theory, and Carlos E. Budde for early discussions on IOSAs.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
D’Argenio, P.R., Lee, M.D., Monti, R.E. (2016). Input/Output Stochastic Automata. In: Fränzle, M., Markey, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2016. Lecture Notes in Computer Science(), vol 9884. Springer, Cham. https://doi.org/10.1007/978-3-319-44878-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-44878-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-44877-0
Online ISBN: 978-3-319-44878-7
eBook Packages: Computer ScienceComputer Science (R0)