The regular separability problem asks, for two given languages, if there exists a regular language including one of them but disjoint from the other. Our main result is decidability, and PSpace-completeness, of the regular separability problem for languages of one counter automata without zero tests (also known as one counter nets). This contrasts with undecidability of the regularity problem for one counter nets, and with undecidability of the regular separability problem for one counter automata, which is our second result.
We investigate a subclass of languages recognized by vector addition systems, namely languages of nondeterministic Parikh automata. While the regularity problem (is the language of a given automaton regular?) is undecidable for this model, we show surprising decidability of the regular separability problem: given two Parikh automata, is there a regular language that contains one of them and is disjoint from the other?
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 a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on …
We present a method for approximating context-free languages with one-counter automata. This approximation allows the reconstruction of parse trees of the original grammar. We identify a decidable superset of regular languages whose elements, i.e. languages, are recognized by one-counter automata.
This paper contains results related to synthesis and presentation of abstract automata by fragments of behaviour and investigates the structure of the classes of finite connected initial output-less automata specified by systems of defining relations considered as fragments, co-fragments, counter-fragments and co-counter-fragments of automata.
Deterministic one-way time-bounded multi-counter automata are studied with respect to their ability to perform reversible computations, which means that the automata are also backward deterministic and, thus, are able to uniquely step the computation back and forth. We study the computational capacity of such devices and obtain separation results between irreversible and reversible k-counter automata for superpolynomial time. For exponential time we obtain moreover an infinite and tight hierarchy with respect to the number of counters. This hierarchy is shown with Kolmogorov complexity and inc…
Parikh automata on finite words were first introduced by Klaedtke and Rueß [Automata, Languages and Programming, 2003]. In this paper, we introduce several variants of Parikh automata on infinite words and study their expressiveness. We show that one of our new models is equivalent to synchronous blind counter machines introduced by Fernau and Stiebe [Fundamenta Informaticae, 2008]. All our models admit ε-elimination, which to the best of our knowledge is an open question for blind counter automata. We then study the classical decision problems of the new automata models.
Many different deletion operations are investigated applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines, deterministic pushdown automata, and finite automata. Operations studied include the prefix, suffix, infix and outfix operations, as well as left and right quotient with languages from different families. It is often expected that language families defined from deterministic machines will not be closed under deletion operations. However, here, it is shown that one-way deterministic reversal-bounded multicounter languages are closed under…
We introduce an affine generalization of counter automata, and analyze their ability as well as affine finite automata. Our contributions are as follows. We show that there is a language that can be recognized by exact realtime affine counter automata but by neither 1-way deterministic pushdown automata nor realtime deterministic k-counter automata. We also show that a certain promise problem, which is conjectured not to be solved by two-way quantum finite automata in polynomial time, can be solved by Las Vegas affine finite automata. Lastly, we show that how a counter helps for affine finite …
We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hie…
We prove the equivalence of two classes of counter machines and one class of distributed automata. Our counter machines operate on finite words, which they read from left to right while incrementing or decrementing a fixed number of counters. The two classes differ in the extra features they offer: one allows to copy counter values, whereas the other allows to compute copyless sums of counters. Our distributed automata, on the other hand, operate on directed path graphs that represent words. All nodes of a path synchronously execute the same finite-state machine, whose state diagram must be ac…
We study the (parameter) synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-regular property. Lechner showed that (th…
In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the correspondin…
We study the ($ω$-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages $L_1$ and $L_2$, check whether there is a regular language that fully contains $L_1$ while remaining disjoint from $L_2$. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from $L_2$. Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of $L_1$. Finally, we sh…
We consider one of the weakest variants of cost register automata over a tropical semiring, namely copyless cost register automata over $\mathbb{N}$ with updates using $\min$ and increments. We show that this model can simulate, in some sense, the runs of counter machines with zero-tests. We deduce that a number of problems pertaining to that model are undecidable, in particular equivalence, disproving a conjecture of Alur et al. from 2012. To emphasize how weak these machines are, we also show that they can be expressed as a restricted form of linearly-ambiguous weighted automata.
We consider a general class of decision problems concerning formal languages, called ``(one-dimensional) unboundedness predicates'', for automata that feature reversal-bounded counters (RBCA). We show that each problem in this class reduces -- non-deterministically in polynomial time -- to the same problem for just finite automata. We also show an analogous reduction for automata that have access to both a pushdown stack and reversal-bounded counters (PRBCA). This allows us to answer several open questions: For example, we show that it is coNP-complete to decide whether a given (P)RBCA languag…
A language $L$ is said to be dense if every word in the universe is an infix of some word in $L$. This notion has been generalized from the infix operation to arbitrary word operations $\varrho$ in place of the infix operation ($\varrho$-dense, with infix-dense being the standard notion of dense). It is shown here that it is decidable, for a language $L$ accepted by a one-way nondeterministic reversal-bounded pushdown automaton, whether $L$ is infix-dense. However, it becomes undecidable for both deterministic pushdown automata (with no reversal-bound), and for nondeterministic one-counter aut…
Parikh automata extend automata with counters whose values can only be tested at the end of the computation, with respect to membership into a semi-linear set. Parikh automata have found several applications, for instance in transducer theory, as they enjoy decidable emptiness problem. In this paper, we study two-way Parikh automata. We show that emptiness becomes undecidable in the non-deterministic case. However, it is PSpace-C when the number of visits to any input position is bounded and the semi-linear set is given as an existential Presburger formula. We also give tight complexity bounds…
A new discontinuous model of computation called one-way jumping finite automata was defined by H. Chigahara et. al. This model was a restricted version of the model jumping finite automata. These automata read an input symbol-by-symbol and jump only in one direction. A generalized linear one-way jumping finite automaton makes jumps after deleting a substring of an input string and then changes its state. These automata can make sequence of jumps in only one direction on an input string either from left to right or from right to left. We show that newly defined model is powerful than its origin…
We look at nondeterministic finite automata augmented with multiple reversal-bounded counters where, during an accepting computation, the behavior of the counters is specified by some fixed pattern. These patterns can serve as a useful "bridge" to other important automata and grammar models in the theoretical computer science literature, thereby helping in their study. Various pattern behaviors are considered, together with characterizations and comparisons. For example, one such pattern defines exactly the smallest full trio containing all the bounded semilinear languages. Another pattern def…
In the last years, various extensions of ω-regular languages have been proposed in the literature, including ωB-regular (ω-regular languages extended with boundedness), ωS-regular (ω-regular languages extended with strict unboundedness), and ωBS-regular languages (the combination of ωB- and ωS-regular ones). While the first two classes satisfy a generalized closure property, namely, the complement of an ωB-regular (resp., ωS-regular) language is an ωS-regular (resp., ωB-regular) one, the last class is not closed under complementation. The existence of non-ωBS-regular languages that are the com…
One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems. The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN ad…
Counter machines have achieved a newfound relevance to the field of natural language processing (NLP): recent work suggests some strong-performing recurrent neural networks utilize their memory as counters. Thus, one potential way to understand the success of these networks is to revisit the theory of counter computation. Therefore, we study the abilities of real-time counter machines as formal grammars, focusing on formal properties that are relevant for NLP models. We first show that several variants of the counter machine converge to express the same class of formal languages. We also prove…
The Eilenberg correspondence relates varieties of regular languages to pseudovarieties of finite monoids. Various modifications of this correspondence have been found with more general classes of regular languages on one hand and classes of more complex algebraic structures on the other hand. It is also possible to consider classes of automata instead of algebraic structures as a natural counterpart of classes of languages. Here we deal with the correspondence relating positive $\mathcal C$-varieties of languages to positive $\mathcal C$-varieties of ordered automata and we present various spe…
