Abstract
In a previous work, we introduced an input/output variant of stochastic automata (IOSA) that, once the model is closed (i.e., all synchronizations are resolved), the resulting automaton is fully stochastic, that is, it does not contain non-deterministic choices. However, such variant is not sufficiently versatile for compositional modelling. In this article, we extend IOSA with urgent actions. This extension greatly increases the modularization of the models, allowing to take better advantage on compositionality than its predecessor. However, this extension introduces non-determinism even in closed models. We first show that confluent models are weakly deterministic in the sense that, regardless the resolution of the non-determinism, the stochastic behaviour is the same. In addition, we provide sufficient conditions to ensure that a network of interacting IOSAs is confluent without the need to analyse the larger composed IOSA.
This work was supported by grants ANPCyT PICT-2017-3894 (RAFTSys), SeCyT-UNC 33620180100354CB (ARES), and the ERC Advanced Grant 695614 (POWVER).
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 subscriptionsReferences
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https://doi.org/10.1017/cbo9781139172752
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelber (2004). https://doi.org/10.1007/978-3-540-30080-9_7
Bengtsson, J., et al.: Verification of an audio protocol with bus collision using Uppaal. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 244–256. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61474-5_73
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). https://doi.org/10.1109/tse.2006.104
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). https://doi.org/10.1007/978-3-540-24611-4_2
Budde, C.E.: Automation of importance splitting techniques for rare event simulation. Ph.D. thesis, Universidad Nacional de Córdoba (2017)
Budde, C.E., D’Argenio, P.R., Monti, R.E.: Compositional construction of importance functions in fully automated importance splitting. In: Puliafito, A., Trivedi, K.S., Tuffin, B., Scarpa, M., Machida, F., Alonso, J. (eds.) Proceedings of 10th EAI International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2016, October 2016, Taormina. ICST (2017). https://doi.org/10.4108/eai.25-10-2016.2266501
Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151–168. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_9
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, Universiteit Twente (1999)
D’Argenio, P.R., Katoen, J.P.: A theory of stochastic systems, part I: Stochastic automata. Inf. Comput. 203(1), 1–38 (2005). https://doi.org/10.1016/j.ic.2005.07.001
D’Argenio, P.R., Katoen, J., Brinksma, E.: An algebraic approach to the specification of stochastic systems (extended abstract). In: Gries, D., de Roever, W.P. (eds.) PROCOMET 1998. IFIP Conference Proceedings, vol. 125, pp. 126–147. Chapman & Hall, Boca Raton (1998). https://doi.org/10.1007/978-0-387-35358-6_12
D’Argenio, P.R., Lee, M.D., Monti, R.E.: Input/Output stochastic automata. In: Fränzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 53–68. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44878-7_4
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). https://doi.org/10.1017/s0960129511000454
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002). https://doi.org/10.1006/inco.2001.2962
Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. LNM, vol. 915, pp. 68–85. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0092872
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995). https://doi.org/10.1006/inco.1995.1123
Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.: A compositional modelling and analysis framework for stochastic hybrid systems. Form. Methods Syst. Des. 43(2), 191–232 (2013). https://doi.org/10.1007/s10703-012-0167-z
Hartmanns, A.: On the analysis of stochastic timed systems. Ph.D. thesis, Saarlandes University, Saarbrücken (2015). http://scidok.sulb.uni-saarland.de/volltexte/2015/6054/
Hermanns, H.: Interactive Markov Chains: And the Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45804-2
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991). https://doi.org/10.1016/0890-5401(91)90030-6
Law, A.M., Kelton, W.D.: Simulation Modeling and Analysis, 3rd edn. McGraw-Hill Higher Education, New York City (1999)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29–62 (2015). https://doi.org/10.1016/j.cosrev.2015.03.001
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). https://doi.org/10.1016/S0304-3975(97)00056-X
Wang, Y.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039080
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
D’Argenio, P.R., Monti, R.E. (2018). Input/Output Stochastic Automata with Urgency: Confluence and Weak Determinism. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-02508-3_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02507-6
Online ISBN: 978-3-030-02508-3
eBook Packages: Computer ScienceComputer Science (R0)