nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Coherent Resolutions of Nondeterminism

verfasst von : Marco Bernardo

Erschienen in: Computer Performance Engineering

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

We study the impact that different ways of resolving nondeterminism within probabilistic automata have on the properties of probabilistic behavioral equivalences. Firstly, we provide a uniform definition of structure-preserving and structure-modifying resolutions of nondeterminism, respectively generated by different families of schedulers. Secondly, we exhibit a number of anomalies arising from the excessive power of the various families of schedulers, which affect the discriminating power, the compositionality, and the backward compatibility of probabilistic trace equivalence. Thirdly, we propose to remove those anomalies by enforcing coherency within resolutions of nondeterminism. This ensures that a scheduler cannot select different continuations in equivalent states of an automaton, so that also the states to which they correspond in any resolution of the automaton have equivalent continuations.

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 Abandonment Attack on the LEACH Protocol

Nächstes Kapitel Emulating Self-adaptive Stochastic Petri Nets

Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200, 149–214 (2005)MathSciNetCrossRef

Bernardo, M.: Genesis and evolution of ULTraS: metamodel, metaequivalences, metaresults. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 92–111. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_7CrossRef

Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. Logical Methods Comput. Sci. 10(1:16), 1–42 (2014)MathSciNetMATH

Bernardo, M., De Nicola, R., Loreti, M.: Relating strong behavioral equivalences for processes with nondeterminism and probabilities. Theor. Comput. Sci. 546, 63–92 (2014)MathSciNetCrossRef

Bernardo, M., Sangiorgi, D., Vignudelli, V.: On the discriminating power of testing equivalences for reactive probabilistic systems: results and open problems. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 281–296. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10696-0_23CrossRefMATH

Bonchi, F., Sokolova, A., Vignudelli, V.: The theory of traces for systems with nondeterminism and probability. In: Proceedings of the 34th ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), no. (19:62), pp. 1–14. IEEE-CS Press (2019)

Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31, 560–599 (1984)MathSciNetCrossRef

De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24, 211–237 (1987)MathSciNetCrossRef

De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984)MathSciNetCrossRef

10.

Deng, Y., van Glabbeek, R., Morgan, C., Zhang, C.: Scalar outcomes suffice for finitary probabilistic testing. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 363–378. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_25CrossRef

11.

Derman, C.: Finite State Markovian Decision Processes. Academic Press, Cambridge (1970)MATH

12.

Georgievska, S., Andova, S.: Probabilistic may/must testing: retaining probabilities by restricted schedulers. Formal Aspects Comput. 24, 727–748 (2012)MathSciNetCrossRef

13.

van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Handbook of Process Algebra, pp. 3–99. Elsevier (2001)

14.

Huynh, D.T., Tian, L.: On some equivalence relations for probabilistic processes. Fundamenta Informaticae 17, 211–234 (1992)MathSciNetMATH

15.

Jonsson, B., Ho-Stuart, C., Yi, W.: Testing and refinement for nondeterministic and probabilistic processes. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 418–430. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58468-4_176CrossRef

16.

Jonsson, B., Yi, W.: Compositional testing preorders for probabilistic processes. In: Proceedings of the 10th IEEE Symposium on Logic in Computer Science (LICS 1995), pp. 431–441. IEEE-CS Press (1995)

17.

Jou, C.-C., Smolka, S.A.: Equivalences, congruences, and complete axiomatizations for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 367–383. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039071CrossRef

18.

Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)MathSciNetCrossRef

19.

Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Van Nostrand, New York (1960)MATH

20.

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

21.

Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATH

22.

Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis (1995)

23.

Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60218-6_17CrossRef

24.

Segala, R.: Testing probabilistic automata. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 299–314. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61604-7_62CrossRef

25.

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

26.

Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. In: Proceedings of the 12th International Symposium on Protocol Specification, Testing and Verification (PSTV 1992), pp. 47–61. North-Holland (1992)

Titel: Coherent Resolutions of Nondeterminism
verfasst von: Marco Bernardo
Verlag: Springer International Publishing
Buch: Computer Performance Engineering
Print ISBN: 978-3-030-44410-5

Electronic ISBN: 978-3-030-44411-2

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-44411-2_2

Neuer Inhalt

Bildnachweise

VDI-Icon, Profil Icon, inhalt2, Springer Professional Modul/© Springer Fachmedien Wiesbaden GmbH, Nachhaltigkeitsaward Key Visual/© Cometis AG/Global ESG Monitor | Daniel Rupp | Generiert mit KI, Search Icon, Banner Hanser, Interview Entropie Bild 1/© Bernhard Weßling, Joerg Schweinsberg/© Datacore Software, Smart Factory Symbolbild/© TensorSpark | Generated with AI | Getty Images, Zeitschrift Wissensmanagement Cover, PatentFit-Logo/© Springer Fachmedien Wiesbaden GmbH, Sustainibility Finance/© Robert Kneschke / stock.adobe.com / Springer Fachmedien Wiesbaden GmbH, Zukunftswerkstatt Sales Excellence 2024/© AndreyPopov / Getty Images / iStock, 2023_Antrieb/© supervisuell

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"

Neuer Inhalt

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

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