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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
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).
- 2.
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.
- 3.
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).
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Bernardo, M.: Non-bisimulation-based Markovian behavioral equivalences. J. Logic Algebraic Program. 72, 3–49 (2007)
Bernardo, M.: ULTraS at work: compositionality metaresults for bisimulation andtrace semantics. J. Logical Algebraic Methods Program. 94, 150–182 (2018)
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_3
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)
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)
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)
Bernardo, M., De Nicola, R., Loreti, M.: Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes. Acta Informatica 52, 61–106 (2015)
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_9
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31, 560–599 (1984)
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/BFb0039056
Cleaveland, R., Dayar, Z., Smolka, S.A., Yuen, S.: Testing preorders for probabilistic processes. Inf. Comput. 154, 93–148 (1999)
De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984)
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_36
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)
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)
Derman, C.: Finite State Markovian Decision Processes. Academic Press, Cambridge (1970)
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)
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)
van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Handbook of Process Algebra, pp. 3–99. Elsevier (2001)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121, 59–80 (1995)
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)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137–162 (1985)
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)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)
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_176
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)
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/BFb0039071
Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)
Knast, R.: Continuous-time probabilistic automata. Inf. Control 15, 335–352 (1969)
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)
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)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)
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)
Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)
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_28
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/BFb0017309
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_21
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (1994)
Rabin, M.O.: Probabilistic automata. Inf. Control 6, 230–245 (1963)
Segala, R.: Modeling and verification of randomized distributed real-time systems. PhD thesis (1995)
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_17
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_62
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_35
Seidel, K.: Probabilistic communicating processes. Theor. Comput. Sci. 152, 219–249 (1995)
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)
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Bernardo, M. (2019). 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. Lecture Notes in Computer Science(), vol 11665. Springer, Cham. https://doi.org/10.1007/978-3-030-21485-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-21485-2_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-21484-5
Online ISBN: 978-3-030-21485-2
eBook Packages: Computer ScienceComputer Science (R0)