Fischer, Diana and Kaiser, Lukasz - Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems

lmcs:760 - Logical Methods in Computer Science, September 20, 2012, Volume 8, Issue 3
Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems

Authors: Fischer, Diana and Kaiser, Lukasz

We study 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 that arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and allow the measurement of 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 present a reduction to a class of counter parity games.


Source : oai:arXiv.org:1209.1738
DOI : 10.2168/LMCS-8(3:21)2012
Volume: Volume 8, Issue 3
Published on: September 20, 2012
Submitted on: December 23, 2011
Keywords: Computer Science - Logic in Computer Science,D.2.4, F.4.1


Share

Consultation statistics

This page has been seen 32 times.
This article's PDF has been downloaded 17 times.