7 papers
Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo +1
Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stoc…
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…
The Trembling-Hand Problem for LTLf Planning
Pian Yu, Shufang Zhu, Giuseppe De Giacomo +2
Consider an agent acting to achieve its temporal goal, but with a "trembling hand". In this case, the agent may mistakenly instruct, with a certain (typically small) probability, a…