19 citations · 25 across the 10 of their papers we have counts for
6 papers · 1 filter
A note on the reduction from LTLf to LTL
Alexandre Duret-Lutz
LTLf, a finite word variant of LTL, can be reduced to LTL by introducing a new atomic proposition indicating the prefix of the infinite words that correspond to the finite words th…
Fast Obligation Translation and Synthesis
Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski +3
Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak -automata (DWA). We show that syntactic obligations can be very efficiently converted t…
Engineering an LTLf Synthesis Tool
Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman +2
The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolut…
Simplifying LTL Model Checking Given Prior Knowledge
Alexandre Duret-Lutz, Denis Poitrenaud, Yann Thierry-Mieg
We consider the problem of the verification of an LTL specification on a system given some prior knowledge , an LTL formula that is known to satisfy. The automata-th…
Effective Reductions of Mealy Machines
Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz +1
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 so…
Improvements to ltlsynt
Florian Renkin, Philipp Schlehuber, Alexandre Duret-Lutz +1
ltlsynt is a tool for LTL reactive synthesis. We summarize its evolution since 2018.