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

lmcs:760 - Logical Methods in Computer Science, September 20, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:21)2012
Model Checking the Quantitative mu-Calculus on Linear Hybrid SystemsArticle

Authors: Diana Fischer ; Lukasz Kaiser

    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.


    Volume: Volume 8, Issue 3
    Published on: September 20, 2012
    Imported on: December 23, 2011
    Keywords: Computer Science - Logic in Computer Science,D.2.4, F.4.1

    Consultation statistics

    This page has been seen 948 times.
    This article's PDF has been downloaded 372 times.