When seeking to coordinate in a game with imperfect information, it is often relevant for a player to know what other players know. Keeping track of the information acquired in a play of infinite duration may, however, lead to infinite hierarchies of higher-order knowledge. We present a construction that makes explicit which higher-order knowledge is relevant in a game and allows us to describe a class of games that admit coordinated winning strategies with finite memory.

We consider games over a finite alphabet with Gurevich-Harrington's winning conditions and restraints as in Yakhnis-Yakhnis . The game tree, the Gurevich-Harrington's kernels of the winning condition and the restraints are defined by finite automata. We give an effective criterion to determine the winning player and an effective presentation of a class of finite automata defined winning strategies.Our approach yields an alternative solution to the games considered by Büchi and Landweber . The BL algorithm is an important tool for solving (...) effectively presented games. The differences between the BL and our algorithms are as follows. Our algorithm is uniformly applicable to winning sets that correspond to boolean combinations of BL winning conditions, while the BL algorithm requires a transformation of such boolean combinations into a single BL condition. Our algorithm directly applies to a larger class of game trees for a given game alphabet than does the BL one. We describe Büchi-Landweber's class of winning conditions in a more transparent way by using finite automata and Gurevich-Harrington's form of winning conditions. Our algorithms that determine the winner of the game and find a winning strategy, are based on a translation of the events in the game in terms of the transition table of the automaton representing the game. This automaton differs from the ones that represent BL winning conditions. Both algorithms need further investigation.The algorithm determining the winner in the game, can be used as a verifier of concurrent programs. This is because programs can be viewed as strategies in Gurevich-Harrington's games and program specifications could be regarded as winning conditions for such games. The algorithm which finds a winning strategy could be used as a basis for automated concurrent program design.The present paper is a sequel to Annals of Pure and Applied Logic 48 277–297. (shrink)

The modal -calculus extends basic modal logic with second-order quantification in terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete. Decision procedures for the modal -calculus are not easy to obtain though since the arbitrary nesting of fixpoint constructs requires some combinatorial arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g., explicitly require formulas to be in guarded normal form. In this paper (...) we present a tableau calculus for deciding satisfiability of arbitrary, i.e., not necessarily guarded -calculus formulas. It is based on a new unfolding rule for greatest fixpoint formulas which allows unguarded formulas to be handled without an explicit transformation into guarded form, thus avoiding a exponential blow-up in formula size. We prove soundness and completeness of the calculus, and compare it empirically to using guarded transformation instead. The new unfolding rule can also be used to handle nested star operators in PDL formulas correctly. (shrink)