Partielle Information in Logik und Spielen
Zusammenfassung der Projektergebnisse
The main objectives of this project concerned the analysis of partial information in logic in games, often in connection with game structures of low structural complexity. Specifically we have provided a detailed analysis of structural complexity measure of directed graphs and its connection with algorithmic issues in games and properties of winning strategies. We provide a general construction for eliminating imperfect information from games with several players who coordinate against nature, and to transform them into two-player games with perfect information while preserving winning strategy profiles. The construction yields an infinite game tree with epistemic models associated to nodes. To obtain a more succinct representation, we have defined an abstraction based on homomorphic equivalence, which is proved to be sound for games with observable winning conditions. The abstraction generates finite game graphs in several relevant cases, and leads to a new semi-decision procedure for multi-player games with imperfect information. The problem whether winning regions and wining strategies for parity games can be computed in polynomial time is a major open problem in the field of infinite games, which is relevant for many applications in logic and formal verification. For some time the discrete strategy improvement algorithm had been considered to be a candidate for solving parity games in polynomial time. However, it has recently been proved that this algorithm requires super-polynomially many iteration steps, for all popular local improvements rules. We have analysed the counter-examples in terms of complexity measures for directed graphs such as tree width, DAG-width, entanglement and Kelly-width. It turned out that with respect to all of these measures, the complexity of the counterexamples is bounded, and indeed in most cases by very small numbers. This analysis shows that the discrete strategy improvement algorithm even has super-polynomial lower time bounds on natural classes of parity games on which efficient algorithms are known. Entanglement is a parameter for the complexity of finite directed graphs that measures to which extent the cycles of the graph are intertwined. It is defined by way of a game similar in spirit to the cops and robber games used to describe tree width, directed tree width, and hypertree width. Entanglement is intimately related with the computational and descriptive complexity of the modal µ-calculus. We have studied complexity issues for entanglement and have compared it to other structural parameters of directed graphs. One of our main results is that parity games of bounded entanglement can be solved in polynomial time. Furthermore, we have discussed the case of graphs of entanglement two. While graphs of entanglement zero and one are very simple, graphs of entanglement two allow arbitrary nesting of cycles, and they form a sufficiently rich class for modelling relevant classes of structured systems. We have provided characterisations of this class, and propose decomposition notions similar to the ones for tree width, DAG-width, and Kelly-width. Finally we have constructed model-checking games for logics of dependence and independence whose semantics, called team semantics, is not based on single assignments (mapping variables to elements of a structure) but on sets of assignments (teams). We have designed model-checking games for logics with team semantics in a general and systematic way. The construction works for any extension of first-order logic by atomic formulae on teams, as long as certain natural conditions are observed, which are satisified by all team properties considered so far in the literature, including dependence, independence, constancy, inclusion, and exclusion. The secondorder features of team semantics are reflected by the notion of a consistent winning strategy which is also a second-order notion in the sense that it depends not on single plays but on the space of all plays that are compatible with the strategy. Based on our games, we also have provided a complexity analysis of logics with teams semantics.
Projektbezogene Publikationen (Auswahl)
- A Perfect-Information Construction for Coordination in Games. Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS ’11, pp. 387-398. Schloss Dagstuhl - Leibniz-Zentrum u f¨r Informatik, 2011
D. Berwanger, L. Kaiser, and B. Puchala
- Entanglement and the Complexity of Directed Graphs. Theoretical Computer Science, vol. 463 (2012), pp. 2–25
D. Berwanger, E. Grädel, L. Kaiser, and R. Rabinovich
- Model-Checking Games for Logics of Incomplete Information. Theoretical Computer Science, vol. 493 (2013), pp. 2–14
E. Grädel
- The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs. Theoretical Computer Science, vol. 560 (2014) pp. 235 - 250
F. Canavoi, E. Gr¨del, and R. Rabinovich
(Siehe online unter https://doi.org/10.1016/j.tcs.2013.12.021)
