Skip to main content
SpringerLink
Log in

Input/Output Stochastic Automata with Urgency: Confluence and Weak Determinism

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2018 (ICTAC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11187))

Included in the following conference series:

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 to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https://doi.org/10.1017/cbo9781139172752

    Book  MATH  Google Scholar 

  2. 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

    Chapter  Google Scholar 

  3. 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

    Chapter  Google Scholar 

  4. 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

    Article  Google Scholar 

  5. 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

    Chapter  MATH  Google Scholar 

  6. Budde, C.E.: Automation of importance splitting techniques for rare event simulation. Ph.D. thesis, Universidad Nacional de Córdoba (2017)

    Google Scholar 

  7. 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

  8. 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

    Chapter  Google Scholar 

  9. Crouzen, P.: Modularity and determinism in compositional markov models. Ph.D. thesis, Universität des Saarlandes, Saarbrücken (2014)

    Google Scholar 

  10. D’Argenio, P.R.: Algebras and automata for timed and stochastic systems. Ph.D. thesis, Universiteit Twente (1999)

    Google Scholar 

  11. 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

    Article  MATH  Google Scholar 

  12. 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

    Chapter  Google Scholar 

  13. 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

    Chapter  MATH  Google Scholar 

  14. 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

    Article  MathSciNet  MATH  Google Scholar 

  15. 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

    Article  MathSciNet  MATH  Google Scholar 

  16. 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

    Chapter  Google Scholar 

  17. 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

    Article  MathSciNet  MATH  Google Scholar 

  18. 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

    Article  MATH  Google Scholar 

  19. 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/

  20. 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

    Book  MATH  Google Scholar 

  21. 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

    Article  MathSciNet  MATH  Google Scholar 

  22. Law, A.M., Kelton, W.D.: Simulation Modeling and Analysis, 3rd edn. McGraw-Hill Higher Education, New York City (1999)

    MATH  Google Scholar 

  23. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  24. 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

    Article  MathSciNet  MATH  Google Scholar 

  25. Wolovick, N.: Continuous probability and nondeterminism in labeled transition systems. Ph.D. thesis, Universidad Nacional de Córdoba, Argentina (2012)

    Google Scholar 

  26. 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

    Article  MathSciNet  MATH  Google Scholar 

  27. 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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Nacional de Córdoba, FAMAF, Córdoba, Argentina

    Pedro R. D’Argenio & Raúl E. Monti

  2. CONICET, Córdoba, Argentina

    Pedro R. D’Argenio & Raúl E. Monti

  3. Saarland University, Department of Computer Science, Saarbrücken, Germany

    Pedro R. D’Argenio

Authors
  1. Pedro R. D’Argenio
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raúl E. Monti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pedro R. D’Argenio .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation