Advertisement

Computing Branching Distances Using Quantitative Games

  • Uli FahrenbergEmail author
  • Axel Legay
  • Karin Quaas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11884)

Abstract

We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.

Keywords

Quantitative verification Branching distance Quantitative game Path-building game 

References

  1. 1.
    Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continous-time Markov chains. ACM Trans. Comput. Log. 1(1), 162–170 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85778-5_4zbMATHCrossRefGoogle Scholar
  5. 5.
    Byg, J., Jørgensen, K.Y., Srba, J.: TAPAAL: editor, simulator and verifier of timed-arc Petri nets. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 84–89. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04761-9_7CrossRefGoogle Scholar
  6. 6.
    Černý, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21–35 (2012)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4), 23:1–23:38 (2010) MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1), 139–170 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Software Eng. 35(2), 258–273 (2009)zbMATHCrossRefGoogle Scholar
  10. 10.
    de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-45061-0_79CrossRefGoogle Scholar
  11. 11.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes. In: QEST, pp. 264–273. IEEE Computer Society (2008)Google Scholar
  13. 13.
    Dhingra, V., Gaubert, S.: How to solve large scale deterministic games with mean payoff by policy iteration. In: Lenzini, L., Cruz, R.L. (eds.) VALUETOOLS. ACM International Conference Proceedings, vol. 180, p. 12. ACM (2006)Google Scholar
  14. 14.
    Doyen, L., Henzinger, T.A., Legay, A., Ničković, D.: Robustness of sequential circuits. In: Gomes, L., Khomenko, V., Fernandes, J.M. (eds.) ACSD, pp. 77–84. IEEE Computer Society, Washington, D.C. (2010)Google Scholar
  15. 15.
    Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fund. Math. 49, 129–141 (1961)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. Game Theory 8, 109–113 (1979)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Fahrenberg, U., Křetínský, J., Legay, A., Traonouez, L.-M.: Compositionality for quantitative specifications. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 306–324. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-15317-9_19CrossRefGoogle Scholar
  18. 18.
    Fahrenberg, U., Křetínský, J., Legay, A., Traonouez, L.-M.: Compositionality for quantitative specifications. Soft. Comput. 22(4), 1139–1158 (2018)zbMATHCrossRefGoogle Scholar
  19. 19.
    Fahrenberg, U., Larsen, K.G., Thrane, C.: A quantitative characterization of weighted Kripke structures in temporal logic. Comput. Inform. 29(6+), 1311–1324 (2010)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Fahrenberg, U., Legay, A.: A robust specification theory for modal event-clock automata. In: Bauer, S.S., Raclet, J.-B. (eds.) Proceedings Fourth Workshop on Foundations of Interface Technologies, FIT 2012. EPTCS, Tallinn, Estonia, 25 March 2012, vol. 87, pp. 5–16 (2012)CrossRefGoogle Scholar
  21. 21.
    Fahrenberg, U., Legay, A.: The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci. 538, 54–69 (2014)MathSciNetzbMATHCrossRefGoogle Scholar
  22. 22.
    Fahrenberg, U., Legay, A.: A linear-time–branching-time spectrum of behavioral specification theories. In: Steffen, B., Baier, C., van den Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds.) SOFSEM 2017. LNCS, vol. 10139, pp. 49–61. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-51963-0_5zbMATHCrossRefGoogle Scholar
  23. 23.
    Fraïssé, R.: Sur quelques classifications des systèmes de relations. Publ. Scient. de l’Univ. d’Alger Série A 1, 35–182 (1954)Google Scholar
  24. 24.
    Fränzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Meth. Syst. Design 30(3), 179–198 (2007)zbMATHCrossRefGoogle Scholar
  25. 25.
    Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_30CrossRefGoogle Scholar
  26. 26.
    Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time Petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_41CrossRefGoogle Scholar
  27. 27.
    Gilmore, S., Hillston, J.: The PEPA workbench: a tool to support a process algebra-based approach to performance modelling. In: Haring, G., Kotsis, G. (eds.) TOOLS 1994. LNCS, vol. 794, pp. 353–368. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58021-2_20CrossRefGoogle Scholar
  28. 28.
    Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Automat. Contr. 52(5), 782–798 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  29. 29.
    Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100(2), 202–260 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  30. 30.
    Hanisch, H.-M.: Analysis of place/transition nets with timed arcs and its application to batch process control. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 282–299. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56863-8_52CrossRefGoogle Scholar
  31. 31.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)zbMATHCrossRefGoogle Scholar
  32. 32.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)MathSciNetzbMATHCrossRefGoogle Scholar
  33. 33.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: a model checker for hybrid systems. Int. J. Softw. Tools Techn. Trans. 1(1–2), 110–122 (1997)zbMATHCrossRefGoogle Scholar
  34. 34.
    Henzinger, T.A., Majumdar, R., Prabhu, V.S.: Quantifying similarities between timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 226–241. Springer, Heidelberg (2005).  https://doi.org/10.1007/11603009_18zbMATHCrossRefGoogle Scholar
  35. 35.
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  36. 36.
    Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  37. 37.
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRefGoogle Scholar
  38. 38.
    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-46002-0_5CrossRefGoogle Scholar
  39. 39.
    Larsen, K.G., Fahrenberg, U., Thrane, C.: Metrics for weighted transition systems: axiomatization and complexity. Theor. Comput. Sci. 412(28), 3358–3369 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  40. 40.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Techn. Trans. 1(1–2), 134–152 (1997)zbMATHCrossRefGoogle Scholar
  41. 41.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: POPL, pp. 344–352. ACM Press (1989)Google Scholar
  42. 42.
    Merlin, P.M., Farber, D.J.: Recoverability of communication protocols-implications of a theoretical study. IEEE Trans. Commun. 24(9), 1036–1043 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  43. 43.
    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_35CrossRefGoogle Scholar
  44. 44.
    Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)zbMATHGoogle Scholar
  45. 45.
    Stirling, C.: Modal and temporal logics for processes. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 149–237. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60915-6_5CrossRefGoogle Scholar
  46. 46.
    Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Log. Alg. Prog. 79(7), 689–703 (2010)MathSciNetzbMATHCrossRefGoogle Scholar
  47. 47.
    van Breugel, F.: An introduction to metric semantics: operational and denotational models for programming and specification languages. Theor. Comput. Sci. 258(1–2), 1–98 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  48. 48.
    van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115–142 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  49. 49.
    van Breugel, F., Worrell, J.: The complexity of computing a bisimilarity pseudometric on probabilistic automata. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 191–213. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-06880-0_10zbMATHCrossRefGoogle Scholar
  50. 50.
    van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3–99. Elsevier, Amsterdam (2001)zbMATHCrossRefGoogle Scholar
  51. 51.
    Wang, F., Mok, A., Emerson, E.A.: Symbolic model checking for distributed real-time systems. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME 1993. LNCS, vol. 670, pp. 632–651. Springer, Heidelberg (1993).  https://doi.org/10.1007/BFb0024671CrossRefGoogle Scholar
  52. 52.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1&2), 343–359 (1996)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.École polytechniquePalaiseauFrance
  2. 2.Université catholique de LouvainLouvain-la-NeuveBelgium
  3. 3.Aalborg UniversityAalborgDenmark
  4. 4.Universität LeipzigLeipzigGermany

Personalised recommendations