Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2013: Programming Languages and Systems pp 192–208Cite as

Generalized Quantitative Analysis of Metric Transition Systems

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8301))

Abstract

The formalism of metric transition systems, as introduced by de Alfaro, Faella and Stoelinga, is convenient for modeling systems and properties with quantitative information, such as probabilities or time. For a number of applications however, one needs other distances than the point-wise (and possibly discounted) linear and branching distances introduced by de Alfaro et.al. for analyzing quantitative behavior.

In this paper, we show a vast generalization of the setting of de Alfaro et.al., to a framework where any of a large number of other useful distances can be applied. Concrete instantiations of our framework hence give e.g limit-average, discounted-sum, or maximum-lead linear and branching distances; in each instantiation, properties similar to the ones of de Alfaro et.al. hold.

In the end, we achieve a framework which is not only suitable for modeling different kinds of quantitative systems and properties, but also for analyzing these by using different application-determined ways of measuring quantitative behavior.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS 138(1), 3–34 (1995)

    Article  MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  4. Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 1–15. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.: Weighted modal transition systems. Form. Meth. Syst. Design (2013) (online first)

    Google Scholar 

  6. Bauer, S.S., Fahrenberg, U., Legay, A., Thrane, C.: General quantitative specification theories with modalities. In: Hirsch, E.A., Karhumäki, J., Lepistö, A., Prilutskii, M. (eds.) CSR 2012. LNCS, vol. 7353, pp. 18–30. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Boker, U., Henzinger, T.A.: Approximate determinization of quantitative automata. In: FSTTCS, pp. 362–373 (2012)

    Google Scholar 

  8. Bouyer, P., Larsen, K.G., Markey, N., Sankur, O., Thrane, C.: Timed automata can always be made implementable. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 76–91. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Černý, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 253–268. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Černý, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: POPL, pp. 115–128 (2013)

    Google Scholar 

  11. Chatterjee, K., de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: QEST, pp. 179–188 (2006)

    Google Scholar 

  12. Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4) (2010)

    Google Scholar 

  13. de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. TCS 345(1), 139–170 (2005)

    Article  MATH  Google Scholar 

  14. de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching metrics for quantitative transition systems. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 97–109. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Softw. Eng. 35(2), 258–273 (2009)

    Article  Google Scholar 

  16. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. TCS 318(3), 323–354 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Droste, M., Gastin, P.: Weighted automata and weighted logics. TCS 380(1-2), 69–86 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  18. Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comp. 220, 44–59 (2012)

    Article  MathSciNet  Google Scholar 

  19. Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. TCS 410(37), 3481–3494 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  20. Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International Journal of Game Theory 8, 109–113 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  21. Fahrenberg, U., Legay, A., Thrane, C.: The quantitative linear-time–branching-time spectrum. In: FSTTCS, pp. 103–114 (2011)

    Google Scholar 

  22. 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)

    Chapter  Google Scholar 

  23. Gilmore, S., Hillston, J.: The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In: CPE, pp. 353–368 (1994)

    Google Scholar 

  24. Girard, A.: Synthesis using approximately bisimilar abstractions: Time-optimal control problems. In: CDC, pp. 5893–5898 (2010)

    Google Scholar 

  25. Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Automat. Contr. 52(5), 782–798 (2007)

    Article  MathSciNet  Google Scholar 

  26. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  27. 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)

    Article  MATH  Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comp. 111(2), 193–244 (1994)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  31. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)

    Article  Google Scholar 

  32. 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)

    Chapter  Google Scholar 

  33. Larsen, K.G., Legay, A., Traonouez, L.-M., Wąsowski, A.: Robust specification of real time components. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 129–144. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  34. Larsen, K.G., Mardare, R., Panangaden, P.: Taking it to the limit: Approximate reasoning for markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 681–692. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  35. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Techn. Trans. 1(1-2), 134–152 (1997)

    Article  MATH  Google Scholar 

  36. Lawvere, F.W.: Metric spaces, generalized logic, and closed categories. In: Rendiconti del seminario matématico e fisico di Milano, vol. XLIII, pp. 135–166 (1973)

    Google Scholar 

  37. Panangaden, P.: Labelled Markov Processes. Imperial College Press (2009)

    Google Scholar 

  38. Quesel, J.-D., Fränzle, M., Damm, W.: Crossing the bridge between similar games. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 160–176. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  39. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

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

    Google Scholar 

  41. 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)

    Chapter  Google Scholar 

  42. Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Log. Alg. Prog. 79(7), 689–703 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  43. van Breugel, F.: An introduction to metric semantics: operational and denotational models for programming and specification languages. TCS 258(1-2), 1–98 (2001)

    Article  MATH  Google Scholar 

  44. van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. TCS 331(1), 115–142 (2005)

    Article  MATH  Google Scholar 

  45. van Breugel, F., Worrell, J.: Approximating and computing behavioural distances in probabilistic transition systems. TCS 360(1-3), 373–385 (2006)

    Article  MATH  Google Scholar 

  46. Wang, F., Mok, A.K., Emerson, E.A.: Symbolic model checking for distributed real-time systems. In: Larsen, P.G., Wing, J.M. (eds.) FME 1993. LNCS, vol. 670, pp. 632–651. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  47. Zheng, G., Girard, A.: Bounded and unbounded safety verification using bisimulation metrics. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 426–440. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  48. Zwick, U., Paterson, M.: The complexity of mean payoff games. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol. 959, pp. 1–10. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Irisa / INRIA Rennes, France

    Uli Fahrenberg & Axel Legay

Authors
  1. Uli Fahrenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indiana University, 150 S. Woodlawn Avenue, 47405-7104, Bloomington, IN, USA

    Chung-chieh Shan

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Fahrenberg, U., Legay, A. (2013). Generalized Quantitative Analysis of Metric Transition Systems. In: Shan, Cc. (eds) Programming Languages and Systems. APLAS 2013. Lecture Notes in Computer Science, vol 8301. Springer, Cham. https://doi.org/10.1007/978-3-319-03542-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-03542-0_14

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-03541-3

  • Online ISBN: 978-3-319-03542-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation