This version presents a more modular proof of closure under complementation and the PSPACE upper bound, by establishing a link with visibly one-counter automata. The register part has been removed (as it was only loosely related). There is a new section on the relation between one-counter automata and strong automata
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 corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations.
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…
The downward closure of a language $L$ of words is the set of all (not necessarily contiguous) subwords of members of $L$. It is well known that the downward closure of any language is regular. Although the downward closure seems to be a promising abstraction, there are only few language classes for which an automaton for the downward closure is known to be computable. It is shown here that for stacked counter automata, the downward closure is computable. Stacked counter automata are finite automata with a storage mechanism obtained by \emph{adding blind counters} and \emph{building stacks}. H…
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…
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.
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…
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…
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 propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into control states, unlike the naïve approach, and thus produces much smaller deterministic automata. We also develop a simplified and faster version of the general algorithm for the sub-class of so-called monadic CAs (MCAs), i.e., CAs with counting loops on character classes, which are common in practice. Our main motivation is (besides applications in verification and decision procedures of logics) the application of deter…
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…
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.
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the n…
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…
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…
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic $ω$-regular automata to LTL. Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consist…
We consider the complexity of equivalence and learning for multiplicity tree automata, i.e., weighted tree automata over a field. We first show that the equivalence problem is logspace equivalent to polynomial identity testing, the complexity of which is a longstanding open problem. Secondly, we derive lower bounds on the number of queries needed to learn multiplicity tree automata in Angluin's exact learning model, over both arbitrary and fixed fields. Habrard and Oncina (2006) give an exact learning algorithm for multiplicity tree automata, in which the number of queries is proportional to t…
Technion（以色列理工学院）；Bar Ilan University（巴伊兰大学）；Allen Institute for AI（艾伦人工智能研究所）
We present an algorithm for extraction of a probabilistic deterministic finite automaton (PDFA) from a given black-box language model, such as a recurrent neural network (RNN). The algorithm is a variant of the exact-learning algorithm L*, adapted to a probabilistic setting with noise. The key insight is the use of conditional probabilities for observations, and the introduction of a local tolerance when comparing them. When applied to RNNs, our algorithm often achieves better word error rate (WER) and normalised distributed cumulative gain (NDCG) than that achieved by spectral extraction of w…
The question if a deterministic finite automaton admits a software reset in the form of a so-called synchronizing word can be answered in polynomial time. In this paper, we extend this algorithmic question to deterministic automata beyond finite automata. We prove that the question of synchronizability becomes undecidable even when looking at deterministic one-counter automata. This is also true for another classical mild extension of regularity, namely that of deterministic one-turn push-down automata. However, when we combine both restrictions, we arrive at scenarios with a PSPACE-complete (…
We study the reachability problem for networks of timed communicating processes. Each process is a timed automaton communicating with other processes by exchanging messages over unbounded FIFO channels. Messages carry clocks which are checked at the time of transmission and reception with suitable timing constraints. Each automaton can only access its set of local clocks and message clocks of sent/received messages. Time is dense and all clocks evolve at the same rate. Our main contribution is a complete characterisation of decidable and undecidable communication topologies generalising and un…
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…
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…
