Searcharxiv⌕ Search

arXiv subjects

Adrien Pommellet

Publications and source records attributed to Adrien Pommellet.

8 recordsLinked to original sources
arXiv2026

Automata Learning with an Incomplete but Inductive Teacher (Technical Report)

Active automata learning (AAL) under a Minimally Adequate Teacher (MAT) has been successfully used to infer a regular language through membership and equivalence queries. This language might not be fully characterized: we are then interested in finding any solution in a target class of possibly many regular languages. Some problems such as regular language separation or inductive invariant synthesis in the context of regular model checking (RMC) may indeed admit more than one answer. We therefore introduce IdMAT: a new teacher formalism answering queries with respect to any language in the target class, all at once. Such a teacher tailored towards invariant synthesis might provide incomplete "don't know" answers, but also inductive facts of the form "if w1 is accepted, so is w2". We pair IdMAT with a novel AAL algorithm LIndA that 1. encodes all uncertainties as a unique SAT instance and does not fork, 2. leverages incremental SAT solving and UNSAT core analysis, and 3. handles counterexamples of the simple or inductive type in a frugal manner inspired by the Rivest-Schapire refinement technique. We finally evaluate a prototype implementation in the context of regular language separation and RMC.

cs.FL↗
arXiv2025

Active Learning Techniques for Pomset Recognizers

Pomsets are a promising formalism for concurrent programs based on partially ordered sets. Among this class, series-parallel pomsets admit a convenient linear representation and can be recognized by simple algebraic structures known as pomset recognizers. Active learning consists in inferring a formal model of a recognizable language by asking membership and equivalence queries to a minimally adequate teacher (MAT). We improve existing learning algorithms for pomset recognizers by 1. introducing a new counter-example analysis procedure that is in the best case scenario exponentially more efficient than existing methods 2. adapting the state-of-the-art $L^{\lambda}$ algorithm to minimize the impact of exceedingly verbose counter-examples and remove redundant queries 3. designing a suitable finite test suite that ensures general equivalence between two pomset recognizers by extending the well-known W-method.

cs.FL↗
arXiv2024

SAT-based Learning of Computation Tree Logic

The CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bound the size and shape of the desired formula or even ask for its minimality in terms of syntactic size. This synthesis problem is motivated by explanation generation for dissimilar models, e.g. comparing a faulty implementation with the original protocol. We devise a SAT-based encoding for a fixed size CTL formula, then provide an incremental approach that guarantees minimality. We further report on a prototype implementation whose contribution is twofold: first, it allows us to assess the efficiency of various output fragments and optimizations. Secondly, we can experimentally evaluate this tool by randomly mutating Kripke structures or syntactically introducing errors in higher-level models, then learning CTL distinguishing formulas.

cs.LO↗
arXiv2022

Effective Reductions of Mealy Machines

We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel approach derived from simulationbased reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against MeMin on a large collection of test cases made of well-known instances as well as new ones.

cs.FL↗
arXiv2022

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality - that is, the total size in terms of logic and memory elements - of solutions.

cs.LO↗
arXiv2019

Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous

We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called Synchronized Dynamic Pushdown Networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is unfortunately undecidable. Therefore, we tackle this problem by introducing an abstraction framework based on Kleene algebras in order to compute an abstraction of the execution paths between two regular sets of configurations. We combine an automata theoretic saturation procedure with constraint solving in a finite domain. We then apply this framework to an iterative abstraction refinement scheme, using multiple abstractions of increasing complexity and precision.

cs.FL↗
arXiv2018

Reachability Analysis of Pushdown Systems with an Upper Stack

Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to access the part of the memory that is below the current stack or base pointer, hence the need for a model that keeps track of this part of the memory. To this end, we introduce pushdown systems with an upper stack (UPDSs), an extension of PDSs where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors post* and predecessors pre* of a regular set of configurations of such a system are not always regular, but that post* is context-sensitive, so that we can decide whether a single configuration is forward reachable or not. In order to under-approximate pre* in a regular fashion, we consider a bounded-phase analysis of UPDSs, where a phase is a part of a run during which either push or pop rules are forbidden. We then present a method to over-approximate post* that relies on regular abstractions of runs of UPDSs. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent.

cs.FL↗