Abstract Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin’s $$L^*$$ L ∗ algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems.

Transducers generalise automata by producing output word(s) for each input word, thereby defining a relation over words. A transducer is said to be finite-valued if, for every input word, it produces at most k output words, for some constant k. If k = 1, then the transducer is said to be functional. The edit distance between two transducers is the minimal number of edits required to transform every output of one transducer into some output of the other, for each input word. This notion has been studied for functional transducers, where it is shown to be computable. However, it is uncomputable for transducers in general. In this work, we show the computability of the edit distance of finite-valued transducers, a class that is strictly more expressive than functional transducers.

Python implementation of OCA-L* for active learning of deterministic real-time one-counter automata and Python implementation of OCA-L* and MinOCA for active learning of visibly one-counter automata.

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.