We investigate certain word-construction games with variable turn orders. In these games, Alice and Bob take turns on choosing consecutive letters of a word of fixed length, with Alice winning if the result lies in a predetermined target language. The turn orders that result in a win for Alice form a binary language that is regular whenever the target language is, and we prove some upper and lower bounds for its state complexity based on that of the target language.
We investigate certain word-construction games with variable turn orders. In these games, Alice and Bob take turns on choosing consecutive letters of a word of fixed length, with Alice winning if the result lies in a predetermined target language. The turn orders that result in a win for Alice form a binary language that is regular whenever the target language is, and we prove some upper and lower bounds for its state complexity based on that of the target language. We also consider the computational complexity of membership and intersection problems of winning sets.
Previously, self-verifying symmetric difference automata were defined and a tight bound of 2^n-1-1 was shown for state complexity in the unary case. We now consider the non-unary case and show that, for every n at least 2, there is a regular language L_n accepted by a non-unary self-verifying symmetric difference nondeterministic automaton with n states, such that its equivalent minimal deterministic finite automaton has 2^n-1 states. Also, given any SV-XNFA with n states, it is possible, up to isomorphism, to find at most another |GL(n,Z_2)|-1 equivalent SV-XNFA.
In this paper, we associate the idea of derivation languages with flat splicing systems and compare the families of derivation languages (Szilard and control languages) of these systems with the family of languages in Chomsky hierarchy. We show that the family of Szilard languages of labeled flat finite splicing systems of type $( m, n)$ (i.e., $SZLS_{n, FIN}^{m}$ ) and $REG$, $CF$ and $CS$ are incomparable. Also, it is decidable whether or not $SZ_{n, FIN}^{m}(\mathscr{LS}) \subseteq R$ and $R \subseteq SZ_{n, FIN}^{m}(\mathscr{LS})$ for any regular language $R$ and labeled flat finite splici…
Splicing systems are generative mechanisms introduced by Tom Head in 1987 to model the biological process of DNA recombination. The computational engine of a splicing system is the "splicing operation", a cut-and-paste binary string operation defined by a set of "splicing rules" $r = (α_1, α_2 ; α_3, α_4)$ where $α_1, α_2, α_3, α_4$ are words over an alphabet $Σ$. For two strings $x = x_1 α_1 α_2 x_2$ and $y = y_1 α_3 α_4 y_2$, applying the splicing rule $r$ produces the string $z = x_1 α_1 α_4 y_2$. In this paper we focus on a particular type of splicing systems, called $(i, j)$ semi-simple s…
Context-free games on strings are two-player rewriting games based on a set of production rules and a regular target language. In each round, the first player selects a position of the current string; then the second player replaces the symbol at that position according to one of the production rules. The first player wins as soon as the current string belongs to the target language. In this paper the one-pass setting for context-free games is studied, where the knowledge of the first player is incomplete, she selects positions in a left-to-right fashion and only sees the current symbol and th…
We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh image. For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial time algorithm and prove a completeness result: we construct a s…
We show that it is decidable whether two regular languages of infinite trees are separable by a deterministic language, resp., a game language. We consider two variants of separability, depending on whether the set of priorities of the separator is fixed, or not. In each case, we show that separability can be decided in EXPTIME, and that separating automata of exponential size suffice. We obtain our results by reducing to infinite duration games with ω-regular winning conditions and applying the finite-memory determinacy theorem of Büchi and Landweber.
We study \emph{partial-information} two-player turn-based games on graphs with omega-regular objectives, when the partial-information player has \emph{limited memory}. Such games are a natural formalization for reactive synthesis when the environment player is not genuinely adversarial to the system player. The environment player has goals of its own, but the exact goal of the environment player is unknown to the system player. We prove that the problem of determining the existence of a winning strategy for the system player is PSPACE-hard for reachability, safety, and parity objectives. Moreo…
Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary. Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is c…
We present a general theorem for distributed synthesis problems in coordination games with $ω$-regular objectives of the form: If there exists a winning strategy for the coalition, then there exists an "essential" winning strategy, that is obtained by a retraction of the given one. In general, this does not lead to finite-state winning strategies, but when the knowledge of agents remains bounded, we can solve the synthesis problem. Our study is carried out in a setting where objectives are expressed in terms of events that may \emph{not} be observable. This is natural in games of imperfect inf…
The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a deterministic finite automaton (DFA) needs in order to recognize a given language. Given a language $L$ and a bound $k$, recognizability of $L$ by a DFA with $k$ states is reduced to a game between Prover and Refuter. The interaction along the game then serves as a certificate. Certificates generated by Prover are minimal DFAs. Certificates generated by Refuter are faul…
We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formul…
词上的一阶逻辑片段通常可以用有限幺半群或有限半群来刻画。通常这些代数描述产生的问题的可判定性是否一个给定的正则语言是在一个特定的片段定义。一个有效的代数特征可以从所谓的Ω项的恒等式中得到。为了证明一个给定的片段满足某些Ω项的恒等式，我们可以对Ω项的词实例使用Escherichfeucht-Fraisse游戏。由此产生的证明往往需要大量的簿记有关的常数。在本文中，我们介绍了Escherichfeucht-Fraisse对策的ω-条款。为此，我们为每个omega项分配一个标记的线性顺序。我们的主要定理表明，一个给定的片段满足一些单位的欧米茄条款，当且仅当复制者有一个获胜的策略，为游戏的线性订单。这样可以避免记账。作为我们主要结果的一个应用，我们证明了在指数时间内可以判定所有非周期幺半群是否满足某个给定的Ω项恒等式，从而改进了McCammond（Int. J. Algebra Comput.，2001年）。
