19 citations · 25 across the 10 of their papers we have counts for
4 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…
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…