Publications

2013

• D. Fischer. The Quantitative mu-Calculus. PhD thesis, RWTH Aachen University, 2013.                                 
  Abstract   BibTeX

  This thesis studies a generalisation of the modal mu-calculus, a modal fixed-point logic that is an important specification language in formal verification. We define a quantitative generalisation of this logic, meaning that a formula no longer evaluates to true or false but instead to an arbitrary real number. First, this logic is evaluated on a quantitative extension of transition systems equipped with quantitative predicates that assign real values to the nodes of the system. Having fixed a quantitative semantics, we investigate which of the classical theorems established for the modal mu-calculus can be lifted to this quantitative setting. The modal mu-calculus is connected to bisimulation, a notion of behavioural equivalence for transition systems. We define a quantitative notion of bisimulation as a distance between systems. We show that for systems that have a fixed maximal distance, the evaluation of formulae also differs by at most this distance, thus providing a quantitative version of the classical result that the modal mu-calculus is invariant under bisimulation. The converse direction does not hold for Qmu on arbitrary systems. However, as in the classical case, on finitely-branching systems the converse can be shown for the modal fragment and thus already quantitative modal logic characterises quantitative bisimulation on finitely-branching systems. Next, we consider the model-checking problem which, given a system and a formula, is to decide whether the system is a model of the formula. In the quantitative world, this translates to computing the numerical value of a formula at a given node of the system. The model-checking problem for the modal mu-calculus can be solved by parity games, a class of infinite zero-sum graph games. We introduce a quantitative extension of these games and show that they are the corresponding model-checking games for our logic. After establishing bisimulation invariance and developing model-checking games, we move to systems that are closer to the scenarios arising in practical applications. First, we consider discounted systems, i.e. systems where additionally the edges are labelled with quantities. It is not straightforward to define a negation operator in this setting that allows for the duality properties needed for a game-based approach to model checking. We show that in this setting there is only one reasonable way to define it. Again, we define an appropriate extension of parity games and show that they correctly describe the evaluation of a discounted quantitative mu-calculus formula. Finally, we provide an algorithm for solving these games, thus also for model checking the quantitative mu-calculus on discounted systems. In the final chapter, we go even further towards practical applications and evaluate the quantitative mu-calculus on a simple class of hybrid systems, namely initialised linear hybrid systems. We show how to approximate the value of a quantitative mu-calculus formula with arbitrary precision on such systems. We define a corresponding version of parity games and use the previously obtained results to prove that they are the correct model-checking games. Then we show how to simplify these games in several steps. We provide a detailed mathematical analysis of these games. In particular we introduce a new class of almost discrete strategies that permit us to simplify the games and to compute their values.

  @phdthesis{Fischer13,
       author = {Diana Fischer},
       school = {{RWTH} Aachen University},
       title = {The {Q}uantitative mu-{C}alculus},
       url = {http://www.logic.rwth-aachen.de/pub/fischer/diss_fischer.pdf},
       year = {2013},
  }
  

2012

• D. Fischer and Ł. Kaiser. Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems. Logical Methods in Computer Science, vol. 8(3), 2012.                                 
  Abstract   BibTeX

  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.

  @article{FK12,
       author = {Diana Fischer and \L{}ukasz Kaiser},
       title = {Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems},
       journal = {Logical Methods in Computer Science},
       volume = {8},
       number = {3},
       year = {2012},
       ee = {http://dx.doi.org/10.2168/LMCS-8(3:21)2012},
       url = {http://arxiv.org/pdf/1209.1738.pdf},
  }
  

2011

• D. Fischer and Ł. Kaiser. Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems. In Proceedings of the 38th International Colloquium on Automata, Languages and Programming, ICALP 2011 (2), vol. 6756 of Lecture Notes in Computer Science, pp. 404–415. Springer, 2011.                                 
  Abstract   BibTeX

  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.

  @inproceedings{FK11,
       author = {Diana Fischer and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 38th International Colloquium on Automata, Languages and Programming, ICALP~2011 (2)}},
       pages = {404--415},
       publisher = {Springer},
       series = {{Lecture Notes in Computer Science}},
       title = {{Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems}},
       url = {http://www.liafa.jussieu.fr/~kaiser/pub/linear_hybrid_qmu.pdf},
       volume = {6756},
       year = {2011},
  }
  

2010

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative mu-Calculus. Theory Comput. Syst., vol. 47(3), pp. 696–719, 2010.                                 
  Abstract   BibTeX

  We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

  @article{FGK10,
       author = {Diana Fischer and Erich Gr{\"a}del and {\L}ukasz Kaiser},
       journal = {Theory Comput. Syst.},
       number = {3},
       pages = {696--719},
       title = {{Model Checking Games for the Quantitative mu-Calculus}},
       url = {http://logic.rwth-aachen.de/~kaiser/quantitative_games_journal.pdf},
       volume = {47},
       year = {2010},
  }
  

2008

• D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative μ-Calculus. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 301–312, 2008.                                 
  Abstract   BibTeX

  We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

  @inproceedings{FGK08,
       author = {Diana Fischer and Erich Gr{\"a}del and {\L}ukasz Kaiser},
       booktitle = {{Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS~2008}},
       editor = {Susanne Albers and Pascal Weil},
       pages = {301--312},
       title = {{Model Checking Games for the Quantitative $\mu$-Calculus}},
       year = {2008},
  }