| Summary: | 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.
|
|---|