nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

An Axiomatization of Strong Distribution Bisimulation for a Language with a Parallel Operator and Probabilistic Choice

verfasst von : Jan Friso Groote, Erik P. de Vink

Erschienen in: From Software Engineering to Formal Methods and Tools, and Back

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In the setting of a simple process language featuring non-deterministic choice and a parallel operator on the one hand and probabilistic choice on the other hand, we propose an axiomatization capturing strong distribution bisimulation. Contrary to other process equivalences for probabilistic process languages, in this paper distributions rather than states are the leading ingredients for building the semantics and the accompanying equational theory, for which we establish soundness and completeness.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Formal Verification of Railway Timetables - Using the UPPAAL Model Checker

Nächstes Kapitel Enabling Auditing of Smart Contracts Through Process Mining

Andova, S., Baeten, J.C.M., Willemse, T.A.C.: A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 327–342. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949_22CrossRef

Andova, S., Willemse, T.A.C.: Branching bisimulation for probabilistic systems: characteristics and decidability. Theor. Comput. Sci. 356, 325–355 (2006)MathSciNetCrossRef

Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. CUP, Cambridge (2010)MATH

Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes: ACP with generative probabilities. Inf. Comput. 121(2), 234–255 (1995)MathSciNetCrossRef

Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60, 187–231 (2000)MathSciNetCrossRef

Bandini, E., Segala, R.: Axiomatizations for probabilistic bisimulation. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 370–381. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-48224-5_31CrossRef

ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 312–328. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15545-6_20CrossRef

Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)MathSciNetCrossRef

Bernardo, M., Gorrieri, R.: Extended Markovian process algebra. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 315–330. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61604-7_63CrossRef

10.

Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2CrossRef

11.

Crafa, S., Ranzato, F.: Logical characterizations of behavioral relations on transition systems of probability distributions. ACM Trans. Comput. Logic 16(1), 2:1–2:24 (2014)MathSciNetCrossRef

12.

Deng, Y., Hennessy, M.: On the semantics of Markov automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 307–318. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22012-8_24CrossRefMATH

13.

Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139–168 (2013)MathSciNetCrossRef

14.

Deng, Y., Palamidessi, C.: Axiomatizations for probabilistic finite-state behaviors. Theor. Comput. Sci. 373, 92–114 (2007)MathSciNetCrossRef

15.

Deng, Y., Palamidessi, C., Pang, J.: Compositional reasoning for probabilistic finite-state behaviors. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 309–337. Springer, Heidelberg (2005). https://doi.org/10.1007/11601548_17CrossRef

16.

Eisentraut, C., Hermanns, H., Krämer, J., Turrini, A., Zhang, L.: Deciding bisimilarities on distributions. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 72–88. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_6CrossRef

17.

Fischer, N., van Glabbeek, R.: Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours. J. Log. Algebr. Methods Program. 102, 64–102 (2019)MathSciNetCrossRef

18.

Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Broy, M. (ed.) Proceedings of IFIP WG 2.2 & 2.3 Working Conference on Programming Concepts and Methods, pp. 443–458 (1990)

19.

Gnesi, S., ter Beek, M.H.: From the archives of the formal methods and tools lab. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 219–235. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_13CrossRef

20.

Gnesi, S., Larosa, S.: A sound and complete axiom system for the logic ACTL. In: De Santis, A. (ed.) Proceedings of ICTCS 1995, Ravello, 9–11 November 1995, pp. 291–306 (1995)

21.

Groote, J.F., Rivera Verduzco, H.J., de Vink, E.P.: An efficient algorithm to determine probabilistic bisimulation. Algorithms 11(9), 131–1-22 (2018)MathSciNetCrossRef

22.

Groote, J.F., de Vink, E.P.: A complete axiomatization of branching bisimulation for a simple process language with probabilistic choice, Submitted

23.

Groote, J.F., de Vink, E.P.: Problem solving using process algebra considered insightful. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 48–63. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_3CrossRef

24.

Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings of RTSS 1990, pp. 278–287. IEEE (1990)

25.

Hennessy, M.: Exploring probabilistic bisimulations, part I. Formal Aspects Comput. 24, 749–768 (2012)MathSciNetCrossRef

26.

Hillston, J.: A compositional approach to performance modelling. Ph.D thesis, University of Edinburgh (1994)

27.

Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991) MathSciNetCrossRef

28.

Latella, D., Massink, M., de Vink, E.P.: Bisimulation of labelled state-to-function transition systems coalgebraically. Log. Methods Comput. Sci. 11(4) (2015). https://doi.org/10.2168/LMCS-11(4:16)2015, https://lmcs.episciences.org/1617

29.

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

30.

Moller, F.: The importance of the left merge operator in process algebras. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 752–764. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0032072CrossRef

31.

Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 287–301. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71389-0_21CrossRefMATH

32.

Segala, R.: Modeling and Verification of Randomzied Distributed Real-Time Systems. Ph.D thesis, MIT (1995). Technical report MIT/LCS/TR-676

33.

Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994). https://doi.org/10.1007/978-3-540-48654-1_35CrossRef

34.

Stark, E.W., Smolka, S.A.: A complete axiom system for finite-state probabilistic processes. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 571–596. The MIT Press (2000)

35.

Valmari, A.: Simple bisimilarity minimization in O(mlogn) time. Fundamenta Informaticae 105(3), 319–339 (2010)MathSciNetMATH

Titel: An Axiomatization of Strong Distribution Bisimulation for a Language with a Parallel Operator and Probabilistic Choice
verfasst von: Jan Friso Groote
Erik P. de Vink
Verlag: Springer International Publishing
Buch: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_26

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner