5 papers
Multi-Property Synthesis
Christoph Weinhuber, Yannik Schnitzer, Alessandro Abate +3
We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point com…
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…
LTLf Synthesis Under Unreliable Input
Christian Hagemeier, Giuseppe de Giacomo, Moshe Y. Vardi
We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certa…
LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin +1
We introduce LTLf+ and PPLTL+, two logics to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+…
On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts
Shengping Xiao, Yongkang Li, Shufang Zhu +4
We present an on-the-fly synthesis framework for Linear Temporal Logic over finite traces (LTLf) based on top-down deterministic automata construction. Existing approaches rely on…