Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userInfinite Games Specified by 2-Tape Automata
123
0
0.0
(
0
)
Added by
Olivier Finkel
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Authors
Olivier Finkel
Ask ChatGPT about the research
No Arabic abstract
We prove that the determinacy of Gale-Stewart games whose winning sets are infinitary rational relations accepted by 2-tape Buchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. Then we prove that winning strategies, when they exist, can be very complex, i.e. highly non-effective, in these games. We prove the same results for Gale-Stewart games with winning sets accepted by real-time 1-counter Buchi automata, then extending previous results obtained about these games. Then we consider the strenghs of determinacy for these games, and we prove that there is a transfinite sequence of 2-tape Buchi automata (respectively, of real-time 1-counter Buchi automata) $A_alpha$, indexed by recursive ordinals, such that the games $G(L(A_alpha))$ have strictly increasing strenghs of determinacy. Moreover there is a 2-tape Buchi automaton (respectively, a real-time 1-counter Buchi automaton) B such that the determinacy of G(L(B)) is equivalent to the (effective) analytic determinacy and thus has the maximal strength of determinacy. We show also that the determinacy of Wadge games between two players in charge of infinitary rational relations accepted by 2-tape Buchi automata is equivalent to the (effective) analytic determinacy, and thus not provable in ZFC.
rate research
Read More
We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Buchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We show also that the determinacy of Wadge games between two players in charge of omega-languages accepted by 1-counter Buchi automata is equivalent to the (effective) analytic Wadge determinacy. Using some results of set theory we prove that one can effectively construct a 1-counter Buchi automaton A and a Buchi automaton B such that: (1) There exists a model of ZFC in which Player 2 has a winning strategy in the Wadge game W(L(A), L(B)); (2) There exists a model of ZFC in which the Wadge game W(L(A), L(B)) is not determined. Moreover these are the only two possibilities, i.e. there are no models of ZFC in which Player 1 has a winning strategy in the Wadge game W(L(A), L(B)).
Some decidable winning conditions of arbitrarily high finite Borel complexity for games on finite graphs or on pushdown graphs have been recently presented by O. Serre in [ Games with Winning Conditions of High Borel Complexity, in the Proceedings of the International Conference ICALP 2004, LNCS, Volume 3142, p. 1150-1162 ]. We answer in this paper several questions which were raised by Serre in the above cited paper. We first show that, for every positive integer n, the class C_n(A), which arises in the definition of decidable winning conditions, is included in the class of non-ambiguous context free omega languages, and that it is neither closed under union nor under intersection. We prove also that there exists pushdown games, equipped with such decidable winning conditions, where the winning sets are not deterministic context free languages, giving examples of winning sets which are non-deterministic non-ambiguous context free languages, inherently ambiguous context free languages, or even non context free languages.
We solve some decision problems for timed automata which were recently raised by S. Tripakis in [ Folk Theorems on the Determinization and Minimization of Timed Automata, in the Proceedings of the International Workshop FORMATS2003, LNCS, Volume 2791, p. 182-188, 2004 ] and by E. Asarin in [ Challenges in Timed Languages, From Applied Theory to Basic Theory, Bulletin of the EATCS, Volume 83, p. 106-120, 2004 ]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a timed regular language is timed regular. We show that the problem of the minimization of the number of clocks of a timed automaton is undecidable. It is also undecidable whether the shuffle of two timed regular languages is timed regular. We show that in the case of timed Buchi automata accepting infinite timed words some of these problems are Pi^1_1-hard, hence highly undecidable (located beyond the arithmetical hierarchy).
Game semantics provides an interactive point of view on proofs, which enables one to describe precisely their dynamical behavior during cut elimination, by considering formulas as games on which proofs induce strategies. We are specifically interested here in relating two such semantics of linear logic, of very different flavor, which both take in account concurrent features of the proofs: asynchronous games and concurrent games. Interestingly, we show that associating a concurrent strategy to an asynchronous strategy can be seen as a semantical counterpart of the focusing property of linear logic.
We consider parity games on infinite graphs where configurations are represented by control-states and integer vectors. This framework subsumes two classic game problems: parity games on vector addition systems with states (vass) and multidimensional energy parity games. We show that the multidimensional energy parity game problem is inter-reducible with a subclass of single-sided parity games on vass where just one player can modify the integer counters and the opponent can only change control-states. Our main result is that the minimal elements of the upward-closed winning set of these single-sided parity games on vass are computable. This implies that the Pareto frontier of the minimal initial credit needed to win multidimensional energy parity games is also computable, solving an open question from the literature. Moreover, our main result implies the decidability of weak simulation preorder/equivalence between finite-state systems and vass, and the decidability of model checking vass with a large fragment of the modal mu-calculus.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
