Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems

TL;DR

This paper presents a method for model checking the quantitative mu-calculus on linear hybrid systems, enabling precise analysis of quantitative properties in hybrid models.

Contribution

It introduces a novel approach for model checking the quantitative mu-calculus on linear hybrid systems using discretisation and reduction to counter parity games.

Findings

Model checking the quantitative mu-calculus is feasible on initialised linear hybrid systems.

New discretisation techniques based on strategies in model-checking games are developed.

Reduction to counter parity games allows for arbitrary precision in analysis.

Abstract

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.