No Arabic abstract
We prove that some fairly basic questions on automata reading infinite words depend on the models of the axiomatic system ZFC. It is known that there are only three possibilities for the cardinality of the complement of an omega-language $L(A)$ accepted by a Buchi 1-counter automaton $A$. We prove the following surprising result: there exists a 1-counter Buchi automaton $A$ such that the cardinality of the complement $L(A)^-$ of the omega-language $L(A)$ is not determined by ZFC: (1). There is a model $V_1$ of ZFC in which $L(A)^-$ is countable. (2). There is a model $V_2$ of ZFC in which $L(A)^-$ has cardinal $2^{aleph_0}$. (3). There is a model $V_3$ of ZFC in which $L(A)^-$ has cardinal $aleph_1$ with $aleph_0<aleph_1<2^{aleph_0}$. We prove a very similar result for the complement of an infinitary rational relation accepted by a 2-tape Buchi automaton $B$. As a corollary, this proves that the Continuum Hypothesis may be not satisfied for complements of 1-counter omega-languages and for complements of infinitary rational relations accepted by 2-tape Buchi automata. We infer from the proof of the above results that basic decision problems about 1-counter omega-languages or infinitary rational relations are actually located at the third level of the analytical hierarchy. In particular, the problem to determine whether the complement of a 1-counter omega-language (respectively, infinitary rational relation) is countable is in $Sigma_3^1 setminus (Pi_2^1 cup Sigma_2^1)$. This is rather surprising if compared to the fact that it is decidable whether an infinitary rational relation is countable (respectively, uncountable).
We study the computational complexity of various problems related to synchronization of weakly acyclic automata, a subclass of widely studied aperiodic automata. We provide upper and lower bounds on the length of a shortest word synchronizing a weakly acyclic automaton or, more generally, a subset of its states, and show that the problem of approximating this length is hard. We investigate the complexity of finding a synchronizing set of states of maximum size. We also show inapproximability of the problem of computing the rank of a subset of states in a binary weakly acyclic automaton and prove that several problems related to recognizing a synchronizing subset of states in such automata are NP-complete.
In this note we study automata recognizing birecurrent sets. A set of words is birecurrent if the minimal partial DFA recognizing this set and the minimal partial DFA recognizing the reversal of this set are both strongly connected. This notion was introduced by Perrin, and Dolce et al. provided a characterization of such sets. We prove that deciding whether a partial DFA recognizes a birecurrent set is a PSPACE-complete problem. We show that this problem is PSPACE-complete even in the case of binary partial DFAs with all states accepting and in the case of binary complete DFAs. We also consider a related problem of computing the rank of a partial DFA.
We consider the problem {sc Max Sync Set} of finding a maximum synchronizing set of states in a given automaton. We show that the decision version of this problem is PSPACE-complete and investigate the approximability of {sc Max Sync Set} for binary and weakly acyclic automata (an automaton is called weakly acyclic if it contains no cycles other than self-loops). We prove that, assuming $P e NP$, for any $varepsilon > 0$, the {sc Max Sync Set} problem cannot be approximated in polynomial time within a factor of $O(n^{1 - varepsilon})$ for weakly acyclic $n$-state automata with alphabet of linear size, within a factor of $O(n^{frac{1}{2} - varepsilon})$ for binary $n$-state automata, and within a factor of $O(n^{frac{1}{3} - varepsilon})$ for binary weakly acyclic $n$-state automata. Finally, we prove that for unary automata the problem becomes solvable in polynomial time.
This volume contains the proceedings of the 12th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2021). The aim of GandALF 2021 symposium is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization.
We present an underapproximation for context-free languages by filtering out runs of the underlying pushdown automaton depending on how the stack height evolves over time. In particular, we assign to each run a number quantifying the oscillating behavior of the stack along the run. We study languages accepted by pushdown automata restricted to k-oscillating runs. We relate oscillation on pushdown automata with a counterpart restriction on context-free grammars. We also provide a way to filter all but the k-oscillating runs from a given PDA by annotating stack symbols with information about the oscillation. Finally, we study closure properties of the defined class of languages and the complexity of the k-emptiness problem asking, given a pushdown automaton P and k >= 0, whether P has a k-oscillating run. We show that, when k is not part of the input, the k-emptiness problem is NLOGSPACE-complete.