Counting logics and games with counters

• Zähllogiken und Spiele mit Zählern

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

Aachen : Publikationsserver der RWTH Aachen University (2015)
Doktorarbeit

Aachen, Techn. Hochsch., Diss., 2015

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.