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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continous-time Markov chains. ACM Trans. Comput. Log. 1(1), 162–170 (2000)
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)
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)
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)
Boker, U., Henzinger, T.A.: Approximate determinization of quantitative automata. In: FSTTCS, pp. 362–373 (2012)
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)
Č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)
Černý, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: POPL, pp. 115–128 (2013)
Chatterjee, K., de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: QEST, pp. 179–188 (2006)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4) (2010)
de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. TCS 345(1), 139–170 (2005)
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)
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Softw. Eng. 35(2), 258–273 (2009)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. TCS 318(3), 323–354 (2004)
Droste, M., Gastin, P.: Weighted automata and weighted logics. TCS 380(1-2), 69–86 (2007)
Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comp. 220, 44–59 (2012)
Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. TCS 410(37), 3481–3494 (2009)
Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International Journal of Game Theory 8, 109–113 (1979)
Fahrenberg, U., Legay, A., Thrane, C.: The quantitative linear-time–branching-time spectrum. In: FSTTCS, pp. 103–114 (2011)
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)
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)
Girard, A.: Synthesis using approximately bisimilar abstractions: Time-optimal control problems. In: CDC, pp. 5893–5898 (2010)
Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Automat. Contr. 52(5), 782–798 (2007)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)
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)
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)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comp. 111(2), 193–244 (1994)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
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)
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)
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)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Techn. Trans. 1(1-2), 134–152 (1997)
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)
Panangaden, P.: Labelled Markov Processes. Imperial College Press (2009)
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)
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)
Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)
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)
Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Log. Alg. Prog. 79(7), 689–703 (2010)
van Breugel, F.: An introduction to metric semantics: operational and denotational models for programming and specification languages. TCS 258(1-2), 1–98 (2001)
van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. TCS 331(1), 115–142 (2005)
van Breugel, F., Worrell, J.: Approximating and computing behavioural distances in probabilistic transition systems. TCS 360(1-3), 373–385 (2006)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)