Counting logics and games with counters

Leßenich, Simon Robert; Thomas, Wolfgang; Grädel, Erich; Bojańczyk, Mikołaj

doi:urn:nbn:de:hbz:82-rwth-2015-023225

Counting logics and games with counters = Zähllogiken und Spiele mit Zählern

Leßenich, Simon Robert

2015

Verantwortlichkeitsangabevorgelegt von Simon Robert Leßenich

ImpressumAachen : Publikationsserver der RWTH Aachen University 2015

UmfangVII, 164 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2015

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor) ; Bojańczyk, Mikołaj (Thesis advisor) ; Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-05-13

Online
URN: urn:nbn:de:hbz:82-rwth-2015-023225
URL: https://publications.rwth-aachen.de/record/466786/files/466786.pdf
URL: https://publications.rwth-aachen.de/record/466786/files/466786.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; quantitative logics (frei) ; games with counters (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Eigenschaften oder Modelle bei der Verifikation und Synthese von Systemen sindoft quantitativ und beinhalten häufig eine Art von Zählen. Fragen können sein,wie groß der Speicherbedarf eines Systems ist, wie viele gleichzeitige Anfragenein System bearbeiten muss, oder wie viele Infixe eines Wortes zu einerregulären Sprache gehören. Diese Arbeit beschäftigt sich mit zwei Modellen vonunendlichen Spielen mit Zählern und zwei quantitativen Zähllogiken.Die ersten Spiele, die wir betrachten, sind Zählerparitätsspiele. In diesenquantitativen Spielen wird eine endliche Menge von Zählern entlang der Kantenaktualisiert. Die Auszahlungen für endliche Partien hängen von den Zählern ab,während Auszahlungen für unendliche Partien mittels einer Paritätsbedingungbestimmt werden. Das Ziel des einen Spielers ist die Maximierung der Auszahlung,während sein Gegner diese minimieren will. Wir zeigen, dass der Wert vonZählerparitätsspielen effektiv berechnet werden kann. Der wichtigste Schritt imAlgorithmus ist dabei das Lösen des Unbeschränktheitsproblems für den Wert. Diesmachen wir mit Hilfe eines Spieles mit imperfekter Erinnerung, für das wirzeigen, dass Strategien mit endlichem Speicher für den Spieler mit imperfekterErinnerung ausreichen.In Durchschnitts-Zähler-Spielen, der zweiten Klasse von Spielen, die wirbetrachten, werden Auszahlungen für unendliche Partien mittels einerDurchschnittsbedingung an einen speziellen Zähler bestimmt. Wir zeigen, dasssich das Unbeschränktheitsproblem des Wertes in Ein-Zähler-Spielen lösen lässt,und dass in Ein-Zähler-Solitärspielen der Wert effektiv berechnet werden kann.Die erste Logik, die wir betrachten, ist Qμ[#MSO], eine auf dem quantitativenμ-Kalkül basierende Zähllogik für Transitionssysteme, deren Zustände mitendlichen relationalen Strukturen beschriftet sind. Der Zählaspekt besteht ausder Auswertung von MSO-Zähltermen auf eben diesen Strukturen. Mittels einerReduktion zu Zählerparitätsspielen beweisen wir, dass das Model-Checking-Problemfür diese Zähllogik auf einer Erweiterung von Pushdown-Systemen entscheidbarist.Wir führen außerdem eine quantitative Erweiterung namens qcMSO der monadischenLogik zweiter Stufe ein. Bei dieser Logik folgen wir der klassischenInterpretation von Disjunktionen als Maxima und Konjunktionen als Minima, undnutzen Zählatome der Form |X| für das Bestimmen der Größe von Mengen. Wiruntersuchen die Beziehungen dieser Logik zu zwei anderen Erweiterungen von MSO,nämlich costMSO und MSO+U. Wir beweisen mittels einer Reduktion zu einemModel-Checking-Problem für eine Erweiterung von FO+RR überRessource-automatischen Strukturen, dass die qcWMSO-Theorie der natürlichenZahlen mit Ordnung entscheidbar ist. Zusätzlich präsentieren wirDekompositionsalgorithmen für qcMSO auf den natürlichen Zahlen mit Ordnung undauf dem unendlichen Binärbaum.

In verification and synthesis, properties or models of interest are oftenquantitative, and many quantitative aspects involve counting. For example, onemight be interested in the amount of memory required by a system, how manysimultaneous requests a system has to process along a run, or how many infixesbelonging to some regular language a word contains. In this thesis, we study twomodels of infinite games with counters as well as two quantitative countinglogics.The first game model we consider is that of counter parity games. In thesequantitative games, a finite set of counters is updated along the edges. Payoffsof finite plays are obtained via the counters, while payoffs of infinite playsare determined via a parity condition. The games are played by a maximizing anda minimizing player, and satisfying the parity condition is good for themaximizing player. We prove that the value of a counter parity game can becomputed, and give an algorithm to do so. The key step in the algorithm is tosolve the unboundedness problem for the value. This is done with the help of agame with imperfect recall, for which we show that finite-memory strategiessuffice for the player suffering from imperfect recall.In mean counter games, the second class of games studied in this thesis, thepayoff of infinite plays is obtained via a mean-payoff condition on a specialcounter. We prove that the unboundedness problem for the value can be solved ingames with only one counter. Furthermore, we show that the exact value can becomputed in one-counter single-player games.The first logic we study is Qμ[#MSO], a counting logic based on the quantitativeμ-calculus. This logic is designed specifically for transition systems where thestates are labeled with finite relational structures. Counting is introduced toQμ with the help of counting terms of monadic second-order logic, which areevaluated on the relational structures the states are labeled with. We prove,via a reduction to counter parity games, that the model-checking problem forQμ[#MSO] is decidable on a generalization of pushdown systems.We also consider a quantitative counting extension of monadic second-order logiccalled qcMSO. In this logic, we adapt the classical interpretations ofdisjunctions as maxima and conjunctions as minima and use counting atoms |X| tocount the sizes of sets. We investigate the connections between qcMSO and twoother extensions of MSO, namely costMSO and MSO+U. We prove that theqcWMSO-theory of the natural numbers with order is decidable via a reduction tothe model-checking problem for an extension of FO+RR on resource-automaticstructures. We also provide decomposition algorithms for qcMSO on the naturalnumbers with order and the infinite binary tree.

OpenAccess:
PDF PDF (PDFA)
(additional files)