19 citations · 25 across the 10 of their papers we have counts for
11 papers
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…
Teaching LTL and ω-automata with Spot
Alexandre Duret-Lutz
Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and -automata manipulation. While Spot is routinely used as a research and verificat…
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…
On-the-fly LTLf Synthesis under Partial Observability
Nadav Alon, Supratik Chakraborty, Alexandre Duret-Lutz +4
LTLf synthesis under partial observability requires reasoning about unobservable environment variables, which is typically handled by constructing a belief-state DFA via subset con…
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…