Simon Lessenich: Counting Logics and Games with Counters

Referent: Dipl.-Inform. Simon Lessenich

Titel: Counting Logics and Games with Counters

In verification and synthesis, properties or models of interest are often quantitative, and many quantitative aspects involve counting. For example, one might be interested in the amount of memory required by a system, how many simultaneous requests a system has to process along a run, or how many infixes belonging to some regular language a word contains. In this talk, we present two quantitative counting logics and two models of games with counter. We first study Qmu[#MSO], a counting logic based on the quantitative mu-calculus. This logic is designed specifically for transition systems where the states are labeled with finite relational structures. Counting is introduced to Qmu with the help of counting terms of monadic second-order logic, which are evaluated on the relational structures the states are labeled with. We prove that the model-checking problem for Qmu[#MSO] on a generalization of pushdown systems is reducible to solving finite counter parity games. We then present the model of counter parity games, which are quantitative games in which a finite set of counters is updated along the edges. Payoffs of finite plays are obtained via the counters, while payoffs of infinite plays are determined via a parity condition. We show that finite counter parity games are effectively solvable, using games with imperfect recall to solve the unboundedness problem for the value. Thus, it follows that the above model-checking problem for Qmu[#MSO] is decidable. In the last part of the talk, we discuss a quantitative counting extension of monadic second-order logic called qcMSO and a model of games with counters where payoffs are obtained via a mean-payoff objective on a special counter.

Es laden ein: Die Dozenten der Informatik


Bookmark the permalink.