LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
Authors: Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We study two logics, LTLf+ and PPLTL+, to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli s LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of reactive synthesis for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL synthesis. We present optimal DFA-based technique for solving reactive synthesis for LTLf+ and PPLTL+. Additionally, we adapt these algorithms to optimally solve satisfiability and model-checking for these two logics. |
| Researcher Affiliation | Academia | 1University of Rome La Sapienza , Italy 2University of Oxford, United Kingdom 3University of Sydney, Australia 4Rice University, USA EMAIL, EMAIL, EMAIL, EMAIL |
| Pseudocode | Yes | We solve the LTLf+/PPLTL+ synthesis problem with an automata-theoretic approach based on DFAs, in a 4-step Synthesis Algorithm, as follows. For convenience, we begin with a formula Γ in positive normal-form. The formula Γ can be thought of as a Boolean formula bΓ without negations over a set of the form [k] = {1, 2, . . . , k} (for some k); thus Γ can be formed from bΓ by replacing, for every i [k], every occurrence of i in bΓ by a certain infinite-trace formula of the form QiΓi, where Qi { , , , }. Elements of [k] are called component numbers. Step (1). For each i [k], convert the finite-trace formula Γi into an equivalent DFA Ai = (Di, Fi). Say Di = (Γ, Qi, Ιi, δi). We assume, without loss of generality, that the initial state has no incoming transitions. Note that one only has to do this conversion once for each finite-trace formula, even if it appears in multiple infinite-trace formulas. Step (2). For each i [k], build a transition system D i = (Γ, Qi, Ιi, δ i), a set F i Qi, and an objective Oi over Qi: 1. Say Qi = . Let δ i = δi, F i = Fi, and Oi = { ρ : inf(ρ) F i = }. 2. Say Qi = . Let δ i = δi, F i = Fi, and Oi = { ρ : inf(ρ) (Q \ F i) = }. 3. Say Qi = . If Ιi is not a final state, make it into a final state, i.e., define F i = Fi {Ιi}. Let δ i be like δi except that every non-final state is a sink, i.e., define δ i(q, a) to be q if q F i, and otherwise to be δi(q, a). Let Oi = { ρ : inf(ρ) F i = }. 4. Say Qi = . If Ιi is a final state, make it into a nonfinal state, i.e., define F i = Fi \ {Ιi}. Let δ i be like δi except that every final state q is a sink, i.e., define δ i(q, a) to be q if q F i, and otherwise to be δi(q, a). Let Oi = { ρ : inf(ρ) F i = }. Step (3). Build the product transition system D = Q i [k] D i. Let Q be the state set of D. Define an EL condition (Γ, λ, B) over Q as follows: Γ = [k] (i.e., the labels are the component numbers), λ(q) = {i [k] : qi is marked} (i.e., a state is labeled by the numbers of those components that are in marked states), and the Boolean formula B is formed from the Boolean formula bΓ by simultaneously replacing, for every i with Qi = , every occurrence of i by i. Define the deterministic EL-automaton AΓ = (D, (Γ, λ, B)). Step (4). Solve the EL game AΓ. By Theorem 1, this can be done in time polynomial in the size of the arena and exponential in the number of labels. |
| Open Source Code | No | The paper does not provide any statement about releasing source code or a link to a code repository. It mentions existing tools/solvers like Oink [van Dijk, 2018] but not its own implementation. |
| Open Datasets | No | The paper is theoretical and does not conduct experiments using specific datasets. Therefore, it does not mention any open datasets or their access information. |
| Dataset Splits | No | The paper is theoretical and does not conduct experiments using specific datasets. Therefore, it does not provide information about dataset splits. |
| Hardware Specification | No | The paper is theoretical and focuses on logical formalisms and algorithms. It does not describe any specific hardware used for experiments. |
| Software Dependencies | No | The paper is theoretical and focuses on logical formalisms and algorithms. It mentions existing tools/solvers (e.g., Oink for parity games), but does not specify software dependencies with version numbers for its own implementation or experiments. |
| Experiment Setup | No | The paper is theoretical and describes algorithms and logics. It does not present experimental results or an experimental setup with hyperparameters or training configurations. |