×

Model checking the quantitative \(\mu \)-calculus on linear hybrid systems. (English) Zbl 1333.68178

Aceto, Luca (ed.) et al., Automata, languages and programming. 38th international colloquium, ICALP 2011, Zurich, Switzerland, July 4–8, 2011. Proceedings, Part II. Berlin: Springer (ISBN 978-3-642-22011-1/pbk). Lecture Notes in Computer Science 6756, 404-415 (2011).
Summary: In this work, we consider the model-checking problem for a quantitative extension of the modal \(\mu \)-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions, which arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and additionally allow to measure interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative \(\mu \)-calculus, can be model-checked with arbitrary precision on initialised linear hybrid systems. To this end, we develop new techniques for the discretisation of continuous state spaces based on a special class of strategies in model-checking games and show decidability of a class of counter-reset games that may be of independent interest.
For the entire collection see [Zbl 1217.68004].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

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. Theoretical Computer Science 138(1), 3–34 (1995) · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T
[2] Colcombet, T., Löding, C.: Regular cost functions over finite trees. In: LICS, pp. 70–79. IEEE Computer Society, Los Alamitos (2010)
[3] de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 103–127. Springer, Heidelberg (2003) · Zbl 1274.68209 · doi:10.1007/978-3-540-45187-7_7
[4] 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) · Zbl 1098.68092 · doi:10.1007/978-3-540-27836-8_11
[5] Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermann and primitive-recursive bounds with dickson’s lemma. CoRR, abs/1007.2989 (2010)
[6] Fischer, D., Grädel, E., Kaiser, L.: Model checking games for the quantitative {\(\mu\)}-calculus. Theory Comput. Syst. 47(3), 696–719 (2010) · Zbl 1205.68243 · doi:10.1007/s00224-009-9201-y
[7] Gawlitza, T., Seidl, H.: Computing game values for crash games. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 177–191. Springer, Heidelberg (2007) · Zbl 1141.91345 · doi:10.1007/978-3-540-75596-8_14
[8] Henzinger, T.A., Horowitz, B., Majumdar, R.: Rectangular hybrid games. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 320–335. Springer, Heidelberg (1999) · Zbl 0937.91005 · doi:10.1007/3-540-48320-9_23
[9] Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proceedings of STOC 1995, pp. 373–382. ACM, New York (1995) · Zbl 0978.68534
[10] McAloon, K.: Petri nets and large finite sets. Theoretical Computer Science 32, 173–183 (1984) · Zbl 0569.68046 · doi:10.1016/0304-3975(84)90029-X
[11] McIver, A., Morgan, C.: Results on the quantitative {\(\mu\)}-calculus qM{\(\mu\)}. ACM Trans. Comput. Log. 8(1) (2007) · Zbl 1367.68199 · doi:10.1145/1182613.1182616
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.