Top

Published in:

2019 | OriginalPaper | Chapter

Genesis and Evolution of ULTraS: Metamodel, Metaequivalences, Metaresults

Author : Marco Bernardo

Published in: Models, Languages, and Tools for Concurrent and Distributed Programming

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We discuss the genesis of the ULTraS metamodel and summarize its evolution arising from the introduction of coherent resolutions of nondeterminism and reachability-consistent semirings.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter Playing with Bisimulation in Erlang

next chapter X-Klaim Is Back

Requiring only injectivity as in [3] is not enough because it does not ensure that the former distribution preserves the overall reachability mass of the latter distribution (unlike the probabilistic case, in general there is no predefined reachability mass).

The proof is the same as the third property of Proposition 3.5 of [3], which is now correct in its inductive part (\(|\alpha | = n + 1\), \(a' = a\), “either \(\alpha '\) ...”) due to resolution coherency.

The definition of \(T_{1} \oplus T_{2}\) before Lemma 4.11 of [3] should be rectified by removing the two instances of “\(\alpha \) occurring only in ...” as resolutions are not coherent there (otherwise the if part of Lemma 4.11(2) would not hold).

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRef

Bernardo, M.: Non-bisimulation-based Markovian behavioral equivalences. J. Logic Algebraic Program. 72, 3–49 (2007)MathSciNetCrossRef

Bernardo, M.: ULTraS at work: compositionality metaresults for bisimulation andtrace semantics. J. Logical Algebraic Methods Program. 94, 150–182 (2018)MathSciNetCrossRef

Bernardo, M., De Nicola, R., Loreti, M.: Uniform labeled transition systems for nondeterministic, probabilistic, and stochastic processes. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010. LNCS, vol. 6084, pp. 35–56. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15640-3_3CrossRef

Bernardo, M., De Nicola, R., Loreti, M.: Uniform labeled transition systems for nondeterministic, probabilistic, and stochastic process calculi. In: Proceedings of the 1st International Workshop on Process Algebra and Coordination, PACO 2011, EPTCS, vol. 60, pp. 66–75 (2011)CrossRef

Bernardo, M., De Nicola, R., Loreti, M.: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Inf. Comput. 225, 29–82 (2013)MathSciNetCrossRef

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.: Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes. Acta Informatica 52, 61–106 (2015)MathSciNetCrossRef

Bernardo, M., Tesei, L.: Encoding timed models as uniform labeled transition systems. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds.) EPEW 2013. LNCS, vol. 8168, pp. 104–118. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40725-3_9CrossRef

10.

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

11.

Christoff, I.: Testing equivalences and fully abstract models for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 126–138. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039056CrossRef

12.

Cleaveland, R., Dayar, Z., Smolka, S.A., Yuen, S.: Testing preorders for probabilistic processes. Inf. Comput. 154, 93–148 (1999)MathSciNetCrossRef

13.

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

14.

De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-based transition systems for stochastic process calculi. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 435–446. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_36CrossRef

15.

De Nicola, R., Latella, D., Loreti, M., Massink, M.: A uniform definition of stochastic process calculi. ACM Comput. Surv. 46(1:5), 1–35 (2013)CrossRef

16.

Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Characterising testing preorders for finite probabilistic processes. Logical Methods Comput. Sci. 4(4:4), 1–33 (2008)MathSciNetMATH

17.

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

18.

Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of the 25th IEEE Symposium on Logic in Computer Science (LICS 2010), pp. 342–351. IEEE-CS Press (2010)

19.

Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of the 1st IFIP Working Conference on Programming Concepts and Methods (PROCOMET 1990), North-Holland, pp. 443–458 (1990)

20.

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

21.

van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121, 59–80 (1995)MathSciNetCrossRef

22.

Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings of the 11th IEEE Real-Time Systems Symposium (RTSS 1990), pp. 278–287. IEEE-CS Press (1990)

23.

Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137–162 (1985)MathSciNetCrossRef

24.

Hermanns, H., Rettelbach, M.: Syntax, semantics, equivalences, and axioms for MTIPP. In: Proceedings of the 2nd International Workshop on Process Algebra and Performance Modelling (PAPM 1994), pp. 71–87. University of Erlangen, Technical Report 27–4 (1994)

25.

Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)CrossRef

26.

Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)MATH

27.

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

28.

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)

29.

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

30.

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

31.

Knast, R.: Continuous-time probabilistic automata. Inf. Control 15, 335–352 (1969)MathSciNetCrossRef

32.

Kwiatkowska, M., Norman, G.: A testing equivalence for reactive probabilistic processes. In: Proceedings of the 5th International Workshop on Expressiveness in Concurrency (EXPRESS 1998), ENTCS, vol. 16, no. 2, pp. 114–132. Elsevier (1998)

33.

Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282, 101–150 (2002)MathSciNetCrossRef

34.

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

35.

Latella, D., Massink, M., de Vink, E.P.: Bisimulation of labelled state-to-function transition systems coalgebraically. Logical Methods Comput. Sci. 11(4:16), 1–40 (2015)MathSciNetMATH

36.

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

37.

Neuhäußer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412–427. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_28CrossRef

38.

Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309CrossRef

39.

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

40.

Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (1994)CrossRef

41.

Rabin, M.O.: Probabilistic automata. Inf. Control 6, 230–245 (1963)CrossRef

42.

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

43.

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

44.

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

45.

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

46.

Seidel, K.: Probabilistic communicating processes. Theor. Comput. Sci. 152, 219–249 (1995)MathSciNetCrossRef

47.

Song, L., Zhang, L., Godskesen, J.C., Nielson, F.: Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods Comput. Sci. 9(2:7), 1–34 (2013)MathSciNetMATH

48.

Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)MATH

49.

Tracol, M., Desharnais, J., Zhioua, A.: Computing distances between probabilistic automata. In: Proceedings of the 9th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), EPTCS, vol. 57, pp. 148–162 (2011)CrossRef

50.

Wolf, V., Baier, C., Majster-Cederbaum, M.: Trace machines for observing continuous-time Markov chains. In: Proceedings of the 3rd International Workshop on Quantitative Aspects of Programming Languages (QAPL 2005), ENTCS, vol. 153, no. 2, pp. 259–277. Elsevier (2005)

51.

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), North-Holland, pp. 47–61 (1992)CrossRef

Title: Genesis and Evolution of ULTraS: Metamodel, Metaequivalences, Metaresults
Author: Marco Bernardo
Publisher: Springer International Publishing
Book: Models, Languages, and Tools for Concurrent and Distributed Programming
Print ISBN: 978-3-030-21484-5

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

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-21485-2_7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner