Adrien Pommellet

In Proceedings of the 12th international joint conference (IJCAR’24), nancy, france, july 3–6, 2024

Abstract 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.

Dissecting ltlsynt

By Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet

2023-08-30

In Formal Methods in System Design

Abstract ltlsynt is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. ltlsynt generally follows a textbook approach: the LTL specification is translated into a parity game whose winning strategy can be seen as a Mealy machine modeling a valid controller. This article details each step of this approach, and presents various refinements integrated over the years. Some of these refinements are unique to ltlsynt: for instance, ltlsynt supports multiple ways to encode a Mealy machine as an AIG circuit, features multiple simplification algorithms for the intermediate Mealy machine, and bypasses the usual game-theoretic approach for some subclasses of LTL formulas in favor of more direct constructions.

The Mealy-machine reduction functions of Spot

By Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet

2023-07-04

In Science of Computer Programming

Abstract We present functions for reducing Mealy machines, initially detailed in our FORTE’22 article. These functions are now integrated into Spot 2.11.2, where they are used as part of the ltlsynt tool for reactive synthesis. Of course, since Spot is a library, these functions can also be used on their own, and we provide Python bindings for easy experiments. The reproducible capsule benchmarks these functions on Mealy machines from various sources, and compare them to the MeMin tool.

The reactive synthesis competition (SYNTCOMP): 2018-2021

By Swen Jacobs, Guillermo Alberto Perez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara J. Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clément Tamines, Leander Tentrup, Adam Walker

2022-06-01

In

Abstract

Effective reductions of Mealy machines

By Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet

2022-04-26

In Proceedings of the 42nd international conference on formal techniques for distributed objects, components, and systems (FORTE’22)

Abstract 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 simulation-based 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.

A portable, simple, embeddable type system

By Jim Newton, Adrien Pommellet

2021-04-26

In ELS 2021, the 14th european lisp symposium

Abstract We present a simple type system inspired by that of Common Lisp. The type system is intended to be embedded into a host language and accepts certain fundamental types from that language as axiomatically given. The type calculus provided in the type system is capable of expressing union, intersection, and complement types, as well as membership, subtype, disjoint, and habitation (non-emptiness) checks. We present a theoretical foundation and two sample implementations, one in Clojure and one in Scala.

Practical “paritizing” of Emerson–Lei automata

By Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet

2020-07-07

In Proceedings of the 18th international symposium on automated technology for verification and analysis (ATVA’20)

Abstract We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an $\omega$-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization.

LTL model checking for communicating concurrent programs

By Adrien Pommellet, Tayssir Touili

2020-05-15

In Innovations in Systems and Software Engineering: a NASA journal (ISSE)

Abstract We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs).The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed.

SAT-based learning of computation tree logic

Dissecting ltlsynt

The Mealy-machine reduction functions of Spot

The reactive synthesis competition (SYNTCOMP): 2018-2021

Effective reductions of Mealy machines

A portable, simple, embeddable type system

Practical “paritizing” of Emerson–Lei automata

LTL model checking for communicating concurrent programs

Search

Tags