Boundedness problems in resource games, logics and automatic structures
Martin Lang, Christof Löding, Erich Grädel, Thomas Colcombet · RWTH Publications (RWTH Aachen) · 2016
We study quantitative extensions of games, logics and automata with the idea ofverification for systems with resources in mind. The resources are discrete and can be consumed step-by-step and replenished all at once. We formally model thisby finitely many non-negative integer counters that can be incremented, reset tozero or left unchanged. This particular formalism is inspired by the model ofB-automata for regular cost functions, which are a quantitative extension ofregular languages with extensive closure properties and rich algorithmic resultsby Colcombet. We consider resource games on resource pushdown systems as formal modelfor interactive, recursive systems with resource consumption. A resource gameis a two-player graph game with a qualitative ω-regular winning condition and an additional quantitative objective of the first player to minimize the used resources throughout a play. The game graph is the configuration graph ofa resource pushdown system, whose transitions are annotated with actions for consuming or replenishing resources.We mainly study the bounded winning problem for these games. This is the question whether there is a uniform upper bound k such that the first player can win the game with an allowed resource-usage of k fromall positions in a given set A of initial configurations. We provide algorithmsto solve this problem if the set A is regular and show that it also has applications in automata theory. The second part of this work is dedicated to study the various formal logicsthat have been considered around boundedness and unboundedness questions recently. There are the quantitative logics costMSO, which extends standardmonadic second-order logic with an atomic formula to count the elements in a set variable, and cost first-order (costFO), which extends standard FO-logic with anuniversal quantifier that allows for a certain number of exceptions. Furthermore, there is first-order+resource relations (FO+RR)-aquantitative variant of first-order logic that is evaluated on structures with quantitative relations. Lastly, wealso consider the qualitative logic MSO+U, which extends MSO with a quantifierto test if there are arbitrarily large finite sets that satisfy some formula. We show that costFO and FO+RR have the same expressive power on the infinite binary tree with equallevel predicate and both define the class of regular cost functions there. Moreover, we establish a general connection between costMSO over arbitraryrelational structures and the two first-order logics on the structure withthe respective powerset as universe. Then, we consider the logic quantitative counting MSO (qcMSO), which combines the aspects of costMSO and MSO+U, and show that it can be translated into an extension of FO+RRwith an infinity test (called FO+RR=∞) on the powerset structure. This allows us toalgorithmically reason about qcMSO with a quantitative extension of automaticstructures called resource automatic structures. We study FO+RR=∞ on resource automatic structures and extensions to the areaof infinite words and finite trees. The logic FO+RR=∞ can be effectively evaluated on resource automatic structures on finite words and trees. Inthe case of infinite words, we can only evaluate the weaker logic FO+RR. Altogether, we obtain algorithmic methods to evaluate weak qcMSO formulas, in which set quantification only ranges over finite sets, on the natural numbers with order and the infinite binary tree.