We give an active learning algorithm for deterministic one-counter automata (DOCA) where the learner can ask the teacher membership and minimal equivalence queries. The algorithm called OL∗learns a DOCA in time polynomial in the size of the smallest DOCA, recognising the target language.All existing algorithms for learning DOCA, even for the subclasses of deterministic real-time one-counter automata (DROCA) and visibly one-counter automata (VOCA), in the worst case, run in exponential time with respect to the size of the DOCA under learning. Furthermore, previous learning algorithms are "grey-box" algorithms relying on an additional query type - counter value query - where the teacher returns the counter value reached on reading a given word. In contrast, our algorithm is a "black-box" algorithm.It is known that the minimisation of VOCA is NP-hard. However, OL∗can be used for approximate minimisation of DOCA. In this case, the output size is at most polynomial in the size of a minimal DOCA.

Abstract In this paper, we introduce a novel method for active learning of deterministic real-time one-counter automata (droca). The existing techniques for learning a droca rely on observing the behaviour of the droca up to exponentially large counter values. Our algorithm eliminates this need and requires only a polynomial number of queries. Additionally, our method differs from existing techniques as we learn a minimal counter-synchronous droca, resulting in much smaller counter-examples on equivalence queries. Learning a minimal counter-synchronous droca cannot be done in polynomial time unless $$\mathsf {P = NP}$$ P = NP , even in the case of visibly one-counter automata. We use a SAT solver to overcome this difficulty. The solver is used to compute a minimal separating DFA from a given set of positive and negative samples. We prove that the equivalence of two counter-synchronous drocas can be checked significantly faster than that of general drocas. For visibly one-counter automata, we have discovered an even faster algorithm for equivalence checking. We implemented the proposed learning algorithm and tested it on randomly generated drocas. Our evaluations show that the proposed method outperforms the existing techniques on the test set.

We introduce weighted one-deterministic-counter automata (odca). These are weighted one-counter automata (oca) with the property of counter-determinacy, meaning that all paths labelled by a given word starting from the initial configuration have the same counter-effect. Weighted odcas are a strict extension of weighted visibly ocas, which are weighted ocas where the input alphabet determines the actions on the counter. We present a novel problem called the co-VS (complement to a vector space) reachability problem for weighted odcas over fields, which seeks to determine if there exists a run from a given configuration of a weighted odca to another configuration whose weight vector lies outside a given vector space. We establish two significant properties of witnesses for co-VS reachability: they satisfy a pseudo-pumping lemma, and the lexicographically minimal witness has a special form. It follows that the co-VS reachability problem is in 𝖯. These reachability problems help us to show that the equivalence problem of weighted odcas over fields is in 𝖯 by adapting the equivalence proof of deterministic real-time ocas [Stanislav Böhm and Stefan Göller, 2011] by Böhm et al. This is a step towards resolving the open question of the equivalence problem of weighted ocas. Finally, we demonstrate that the regularity problem, the problem of checking whether an input weighted odca over a field is equivalent to some weighted automaton, is in 𝖯. We also consider boolean odcas and show that the equivalence problem for (non-deterministic) boolean odcas is in PSPACE, whereas it is undecidable for (non-deterministic) boolean ocas.

We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T_1,T_2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T_1 is contained in R(T_2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open.

We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered the origin semantics, that was introduced by Bojanczyk in 2014. We prove that the equivalence and containment problems for two-way word transducers in the origin semantics are PSPACE-complete. We also consider a variant of the containment problem where two-way transducers are compared under the origin semantics, but in a more relaxed way, by allowing distortions of the origins. The possible distortions are described by means of a resynchronization relation. We propose MSO-definable resynchronizers and show that they preserve the decidability of the containment problem under resynchronizations. {}

Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness. We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.

We study various models of transducers equipped with origin information. We consider the semantics of these models as particular graphs, called origin graphs, and we characterise the families of such graphs recognised by streaming string transducers.

Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the model-checking problem for monadic second order logic (respectively first order logic with a reachability predicate) is decidable on such graphs. We unify both models by introducing the notion of stack trees, trees whose nodes are labelled by higher-order stacks, and define the corresponding class of higher-order ground tree rewriting systems. We show that these graphs retain the decidability properties of ground tree rewriting graphs while generalising the pushdown hierarchy of graphs.

Petri nets, or equivalently vector addition systems (VAS), are widely recognized as a central model for concurrent systems. Many interesting properties are decidable for this class, such as boundedness, reachability, regularity, as well as context-freeness, which is the focus of this paper. The context-freeness problem asks whether the trace language of a given VAS is context-free. This problem was shown to be decidable by Schwer in 1992, but the proof is very complex and intricate. The resulting decision procedure relies on five technical conditions over a customized coverability graph. These five conditions are shown to be necessary, but the proof that they are sufficient is only sketched. In this paper, we revisit the context-freeness problem for VAS, and give a simpler proof of decidability. Our approach is based on witnesses of non-context-freeness, that are bounded regular languages satisfying a nesting condition. As a corollary, we obtain that the trace language of a VAS is context-free if, and only if, it has a context-free intersection with every bounded regular language.