Pure-Past Linear Temporal and Dynamic Logic on Finite Traces

1 Introduction

Several research areas in AI have been attracted by the clarity and ease of Linear-time Temporal Logic (LTL) [Pnueli, 1977]. Specifically, LTL has been employed in reasoning about actions and planning: as a specification mechanism for temporally extended goals [Bacchus and Kabanza, 1998; De Giacomo and Vardi, 1999; Calvanese et al., 2002; Camacho et al., 2017], for constraints on plans [Bacchus and Kabanza, 2000], to express preferences and soft constraints [Bienvenu et al., 2006], for specifying multi-agent systems [Fagin et al., 1995], and for specifying norms [Fisher and Wooldridge, 2005].

Recently, a variant of LTL on finite traces, LTLf , and its extension LDLf , inspired by the Propositional Dynamic Logic (PDL) [Harel et al., 2000], have been investigated [De Giacomo and Vardi, 2013], and have found application in several contexts. The main reason for this interest is due to the possibility of transforming LTLf /LDLf formulas into Deterministic Finite-state Automaton (DFA), which can then be suitably employed in different contexts, as mentioned above.

LTLf /LDLf , like LTL originally, expresses temporal properties in a "pure-future fashion", i.e., referring only to the present and to the future. However, it has been observed that sometimes specifications are easier and more natural to express referring to the past [Lichtenstein et al., 1985]. For instance, to say that we have accomplished our task and that since we were decontaminated we have been in clean areas, we write: TaskDone ∧ (InCleanArea S Decontaminated). The use of past temporal logics has been advocated for nonMarkovian models in reasoning about actions [Gabaldon, 2011], for non-Markovian rewards in MDPs [Bacchus et al., 1996], and for normative properties in multi-agent systems [Fisher and Wooldridge, 2005; Knobbout et al., 2016; Alechina et al., 2018].

In this paper, we review the pure-past versions of LTLf and LDLf , respectively PLTLf and PLDLf . Due to the finite nature of traces, PLTLf and PLDLf have a very natural interpretation: they specify formulas that must be true at the end of the trace and evaluate the trace backwards. In fact, PLTLf has been introduced in the literature as a technical means to get results for LTL and LTLf [Maler and Pnueli, 1990; Zhu et al., 2019]. Here, instead, we consider PLTLf , and its extension PLDLf , as first class citizens.

Working with PLTLf /PLDLf gives us an exponential (worstcase) computational advantage with respect to LTLf /LDLf . Such an advantage stems from the fact that, like LTLf /LDLf , also PLTLf /PLDLf can be translated into an Alternating Finitestate Automaton (AFA) in polynomial time, but, in the case of PLTLf /PLDLf , we can exploit a well-known result on regular languages, which states that an AFA can be transformed, in single exponential time, into a DFA that recognizes the reverse language [Chandra et al., 1981]. This should be contrasted with the fact that the DFA for the language itself (not its reverse) can be double-exponentially larger than the AFA.

This language theoretic property has a deep impact on the conversion of PLTLf /PLDLf formulas to their corresponding DFAs. Indeed, PLTLf /PLDLf formulas can be transformed into DFAs in only single exponential time (vs. double exponential time for LTLf /LDLf formulas).

This exponential improvement affects the computational complexity of problems involving temporal logics on finite traces in several contexts, including planning in nondeterministic domains (FOND) [Camacho et al., 2017; De Giacomo and Rubin, 2018], reactive synthesis [De Giacomo and Vardi, 2015; Camacho et al., 2018], MDPs with nonMarkovian rewards [Bacchus et al., 1996; Brafman et al.,

2018], reinforcement learning [De Giacomo et al., 2019; Camacho et al., 2019], and non-Markovian planning and decision problems [Brafman and De Giacomo, 2019a; Brafman and De Giacomo, 2019b].

Interestingly, PLTLf (resp., PLDLf ) and LTLf (resp., LDLf ) have the same expressive power. Indeed, we provide an algorithm to transform a PLTLf (resp., PLDLf ) formula into an LTLf (resp., LDLf ) formula. However, the transformation can be triple-exponentially (resp., double-exponentially) larger in the worst-case, and these are the best-known bounds.

Hence, it is not computationally sensible to start from LTLf /LDLf formulas and transform them into the equivalent PLTLf /PLDLf formulas to take advantage of the exponential improvement. To get such an advantage, the property of interest should be succinctly expressible in PLTLf /PLTLf , as is often the case when the property naturally talks about the past.

2 Preliminaries

AFA, NFA, and DFA. An alternating finite-state automaton (AFA) is a tuple A = ⟨Σ,Q, q0, δ,F⟩, where (i) Σ = 2P is a finite input alphabet; (ii) Q is a finite set of states; (iii) q0 ∈ Q is the initial state; (iv) F ∈ 2Q is the set of accepting states; (v) δ ∶ Q × Σ → B+ (Q) is the transition function, where B+ (Q) is the set of positive Boolean formulas over Q (i.e., built from the states using ∧, ∨ and the constants true and false). For instance, δ(q1, a) = q2 ∨ (q3 ∧ q4) means that for the automaton to accept the input aτ, from state q1, it should either accept the input τ from q2 or from both q3 and q4. For V ⊆ Q and ϕ ∈ B+ (Q), we write V ⊧ ϕ if the assignment that maps states in V to true and states in Q∖V to false satisfies the formula ϕ.

A nondeterministic finite-state automaton (NFA) is an AFA in which no transition uses ∧. For instance, the transition δ(q, a) = (q1 ∨ q2 ∨ q3) is allowed. A deterministic finite-state automaton (DFA) is an NFA in which no transition uses ∨. For instance, the transition δ(q, a) = q1 is allowed.

The size of A, denoted ∣A∣, is the number of bits required to represent the transition function, i.e., ∑q∈Q∑a∈Σ ∣δ(q, a)∣ which is bounded by ∣Q∣∣Σ∣K where K is an upper bound on the lengths of the formulas in the transition function.

An accepting run of an AFA A is defined by introducing the function Acc ∶ Σ∗ → 2Q, where q ∈ Acc(τ) is read "input τ is accepted from state q", inductively given as follows:

1. Acc(ϵ) = F,
2. q ∈ Acc(aτ) iff V ⊧ δ(q, a) for some V ⊆ Acc(τ).

A run τ is accepted by A if q0 ∈ Acc(τ). Note that in the special case that δ(q, a) = true, we have that q ∈ Acc(aτ) for all τ (since ∅ ⊧ true). One way to visualize this definition is via run-trees 1 , see [Vardi, 1996].

1 A run-tree of A on input τ is a tree labeled by states such that i) all nodes at depth ∣τ ∣ are labeled by final states, and ii) if an internal node x is labeled by q, and X is the set of labels of the children of x, then X ⊧ δ(q, x). Note that not all branches need to reach depth ∣τ ∣ since an internal node at depth i may be labeled q where δ(q, τi) = true. Thus, a branch in a run-tree either reaches a final state after reading the word, or hits the transition true.

An easy induction shows that q ∈ Acc(τ) iff there is a run-tree on input τ whose root is labeled by q.

Given an AFA it is possible to obtain (in single exponential time) an NFA that accepts the same language and whose size is at most single exponential in the size of the AFA [Chandra et al., 1981], and hence a DFA that accepts the same language whose size is at most double exponential in the AFA.

We make use of regular expressions, collectively denoted RE [Hopcroft and Ullman, 1979]. In particular, Kleene's Theorem says that one can translate a DFA to a RE in exponential time (and thus to a RE that is at most exponentially-larger than the DFA). We can use RE as temporal specifications on finite traces, see, e.g., [De Giacomo and Vardi, 2013].

LTLf and LDLf . LTLf is a variant of Linear-time Temporal Logic (LTL) interpreted over finite, instead of infinite, traces [De Giacomo and Vardi, 2013]. Given a set P of atomic propositions, LTLf formulas ϕ are defined by:

where a denotes an atomic proposition in P, ◯ is the next operator, and U is the until operator. We use abbreviations for other Boolean connectives, as well as the following: eventually as ◇ϕ ≡ true U ϕ; always as ◻ϕ ≡ ¬ ◇ ¬ϕ; weak next ●ϕ ≡ ¬◯¬ϕ (note that, on finite traces, ¬◯ϕ is not equivalent to ◯¬ϕ); and last (time point of the trace) last ≡ ●false.

Formulas of LTLf are interpreted on finite traces τ = τ0τ1⋯τn-1 where τi at instant i is a propositional interpretation over the alphabet 2P . We denote by length(τ) the length n of τ . Given τ , an LTLf formula ϕ and an instant i, we define when ϕ holds at i, written τ, i ⊧ ϕ, by induction, as follows:

• τ, i ⊧ a iff a ∈ τi (for a ∈ P);
• τ, i ⊧ ¬ϕ iff τ, i /⊧ ϕ;
• τ, i ⊧ ϕ1 ∧ϕ2 iff τ, i ⊧ ϕ1 and τ, i ⊧ ϕ2;
• τ, i ⊧ ◯ϕ iff i < length(τ) - 1 and τ, i + 1 ⊧ ϕ;
• τ, i ⊧ ϕ1 U ϕ2 iff for some j, i ≤ j < length(τ) τ, j ⊧ ϕ2, and for all k, i ≤ k < j τ, k ⊧ ϕ1.

We write τ ⊧ ϕ, if τ, 0 ⊧ ϕ and say that τ satisfies ϕ.

LDLf is a proper extension of LTLf that is able to capture regular expressions over traces. Here, following [Brafman et al., 2018], we consider a notational variant of LDLf . The syntax of LDLf is defined by:

where φ denotes propositional formulas over P (we use the usual abbreviations, e.g., the Boolean constant true is defined as a ∨¬a, for some fixed a ∈ P) and tt stands for logical true (not to be confused with the Boolean constant true). Expressions of the form ϱ are regular expressions (RE) over propositional formulas φ and the test construct ϕ? typical of PDL. We abbreviate [ϱ]ϕ ≡ ¬⟨ϱ⟩¬ϕ as in PDL, ff ≡ ¬tt for false, and φ ≡ ⟨φ⟩tt to denote the occurrence of the propositional formula φ. We also use end ≡ [true]ff to express that the trace has ended.

Intuitively, ⟨ϱ⟩ϕ states that, from the current instant in the trace, there exists an execution satisfying the RE ϱ such that its last instant satisfies ϕ, while [ϱ]ϕ states that, from the current instant, all executions satisfying the RE ϱ are such that their last instant satisfies ϕ. Test constructs put into the execution path checks for satisfaction of additional LDLf formulas.

Given a trace τ = τ0τ1⋯τn-1 we denote by τi,j the sub-trace τi . . . τj if j < length(τ), τi . . . τn-1 if j ≥ length(τ). Note that if i ≥ length(τ) then τi,j denotes the empty trace. Given a finite trace τ , an LDLf formula ϕ, and an instant i, we define when ϕ holds at i, written τ, i ⊧ ϕ, by (mutual) induction, as follows:

• τ, i ⊧ tt;
• τ, i ⊧ ¬ϕ iff τ, i /⊧ ϕ;
• τ, i ⊧ ϕ1 ∧ϕ2 iff τ, i ⊧ ϕ1 and τ, i ⊧ ϕ2;
• τ, i ⊧ ⟨ϱ⟩ϕ iff there is a j such that i ≤ j and τi,j ∈ R(ϱ) and τ, j ⊧ ϕ,

where the relation τi,j ∈ R(ϱ) is inductively defined as:

• τi,j ∈ R(φ) if j = i + 1, i < length(τ), and τi ⊧ φ;
• τi,j ∈ R(ϕ?) if j = i and τ, i ⊧ ϕ;
• τi,j ∈ R(ϱ1+ϱ2) if τi,j ∈ R(ϱ1) or τi,j ∈ R(ϱ2);
• τi,j ∈ R(ϱ1; ϱ2) if there exists i ≤ k ≤ j such that τi,k ∈ R(ϱ1) and τk,j ∈ R(ϱ2);
• τi,j ∈ R(ϱ∗ ) if j = i or there exists k such that τi,k ∈ R(ϱ) and τk,j ∈ R(ϱ∗ ).

Note that if i ≥ length(τ), the above definitions still apply. Again, we say that a trace τ satisfies an LDLf formula ϕ, written τ ⊧ ϕ, if τ, 0 ⊧ ϕ.

LTLf /LDLf to AFA and DFA. For every LTLf /LDLf formula ϕ there is an equivalent AFA Aϕ accepting exactly the traces satisfying ϕ, which is linear in the size of ϕ [De Giacomo and Vardi, 2013]. Moreover, every AFA can be translated into an equivalent DFA, i.e., a DFA recognizing the same language, whose size is at most double-exponential, which can be computed in 2EXPTIME in the size of the AFA [Chandra et al., 1981]. Hence, we have a 2EXPTIME algorithm for translating an LTLf /LDLf formula into an equivalent DFA [De Giacomo and Vardi, 2013].

Algorithm 1: Translating LTLf /LDLf to DFA

Given an LTLf /LDLf formula ϕ

• 1: Compute an AFA equivalent to ϕ (lin)
• 2: Compute an NFA equivalent to the AFA (1exp)
• 3: Determinize the NFA obtaining an equivalent DFA (1exp)

3 PLTLf and PLDLf

We study the pure-past version of LTLf , denoted as PLTLf , and the pure-past version of LDLf , denoted as PLDLf . These are logics on finite traces that refer only to the past. PLTLf and PLDLf have a natural interpretation on finite traces: they are satisfied if they hold in the last instant of the trace.

PLTLf . Given a set P of propositional symbols, PLTLf is defined by:

where a ∈ P, ⊖ is the before operator and S is the since operator. Similarly to LTLf and LDLf , we define the following common abbreviations: the once operator diamondminusϕ ≡ true S ϕ and the historically operator ⊟ϕ ≡ ¬diamondminus¬ϕ.

We define the satisfaction relation τ, i ⊧ ϕ, stating that ϕ holds at instant i, as follows. For atomic propositions and Boolean operators it is as for LTLf . For past operators:

• τ, i ⊧ ⊖ϕ iff i ≥ 1 and τ, i - 1 ⊧ ϕ;
• τ, i ⊧ ϕ1 S ϕ2 iff there exists k, with 0 ≤ k ≤ i such that τ, k ⊧ ϕ2 and for all j, with k < j ≤ i, we have that τ, j ⊧ ϕ1.

A PLTLf formula ϕ is true in τ, denoted τ ⊧ ϕ, if τ, length(τ ) - 1 ⊧ ϕ.

Example 1. The property "we are now at location p23 and we have passed through location p12" can be expressed in PLTLf as p23 ∧diamondminusp12 . It is also expressible in LTLf , although with a more complex formula, i.e., ◇(p12 ∧◇(p23 ∧ last)).

Example 2. The property "every time you took the bus, you bought a new ticket beforehand" can be expressed in PLTLf as ⊟(takeB ⇒ ⊖(¬takeBS buyT)), while it can be expressed in LTLf as (buyT RtakeB) ∧ ◻ (takeB ⇒ (buyT ∨ ◯(buyT R¬takeB))) [Cimatti et al., 2004].

PLDLf . PLDLf is the extension of PLTLf with regular expressions in the eventualities. The syntax of PLDLf is similar to the syntax of LDLf except that we use a backward diamond operator. Intuitively, ⟪ϱ⟫ϕ states that there exists a point in the past, reachable (going backwards) through the regular expression ϱ from the current instant, where ϕ holds. Formally, the syntax of PLDLf is defined by:

Define the satisfaction relation as for LDLf , except that:

• τ, i ⊧ ⟪ϱ⟫ϕ iff there exists j, 0 ≤ j ≤ i such that τj,i ∈ Rpast(ϱ) and τ, j ⊧ ϕ,

where the relation τj,i ∈ Rpast(ϱ) is inductively defined as:

• τj,i ∈ Rpast(φ) if j = i - 1, i ≥ 1, and τi ⊧ φ ;
• τj,i ∈ Rpast(ϕ?) if j = i and τ, i ⊧ ϕ;
• τj,i ∈ Rpast(ϱ1+ϱ2) if τj,i ∈ Rpast(ϱ1) or τj,i ∈ Rpast(ϱ2);
• τj,i ∈ Rpast(ϱ1; ϱ2) if there exists j ≤ k ≤ i such that τk,i ∈ Rpast(ϱ1) and τj,k ∈ Rpast(ϱ2);
• τj,i ∈ Rpast(ϱ∗ ) if j = i or there exists j ≤ k ≤ i such that τk,i ∈ Rpast(ϱ) and τj,k ∈ Rpast(ϱ∗ ).

We say that τ satisfies a PLDLf formula ϕ, written τ ⊧ ϕ, if τ, length(τ) - 1 ⊧ ϕ. As before, we use the abbreviation JϱKϕ ≡ ¬⟪ϱ⟫¬ϕ. Moreover, we define start ≡ JtrueKff to express the fact that the trace has just started.

Example 3. The property "every time, if the cargo-ship departed (cs), then beforehand there was an alternation of grab and unload (unl) of containers" can be expressed in PLDLf as Jtrue ∗ K(⟪cs⟫tt ⇒ ⟪(unl; grab)∗ ; (unl; grab)⟫start), whereas it can be expressed in LDLf as ⟨(¬cs + (grab ∧ ¬cs); (unl; (grab ∧ ¬cs))∗ ; (cs ∧ unl)); ¬cs∗ ⟩end .

As we will see later, all PLTLf /PLDLf formulas are translatable into LTLf /LDLf and vice versa, however the translation can be quite involved.

Just as for LTLf /LDLf , one can build a DFA accepting the traces satisfying ϕ. The same is true for PLTLf /PLDLf formulas ϕ. However, since PLTLf /PLDLf formulas are evaluated from the end of the trace towards the beginning, we can build a DFA whose size is single exponential in the size of the formula (vs. double-exponential, as for LTLf /LDLf ). The crux of this result lays on the possibility of obtaining from an AFA a DFA for the reverse language in single exponential time.

4 Reverse Languages and AFA

The reverse of a string τ = τ0τ1 . . . τn-1 is the string τ R = τn-1 . . . τ1τ0, and the reverse of a language L is the language LR = {τ R ∶ τ ∈ L}. Notably, while the minimal DFA equivalent to an AFA can be double-exponentially larger, the minimal DFA for the reverse language is at most singleexponentially larger [Chandra et al., 1981], and can be easily built as shown below. For an AFA A = (Σ, Q, q0, δ, F), define the DFA AR = (Σ, S, sinit, T, F ′ ) that recognizes the reverse language where:

• S = 2Q, sinit = F;
• for v ∈ S, a ∈ Σ, define T(V, a) to be the set of all q such that V ⊧ δ(q, a);
• let V ∈ F ′ iff q0 ∈ V .

Note that the size of AR is 2O(∣A∣) . Moreover, AR can be computed in exponential time.

Theorem 1. [Chandra et al., 1981] The DFA AR recognizes the reverse of the language of the AFA A.

Proof. Introduce a generalization of Acc defined in Section 2: q ∈ Fwd(τ,X) which is intuitively read as "the automaton reads τ forward from state q and results in a state in the set X". Formally, define Fwd ∶ Σ∗ × 2Q → 2Q inductively:

• (i) Fwd(ϵ,X) = X,
• (ii) Fwd(aτ,X) = {q ∶ Fwd(τ,X) ⊧ δ(q, a)}.

Note that Acc is definable in terms of Fwd, i.e., q ∈ Acc(τ) iff q ∈ Fwd(τ,F). Intuitively, Fwd processes the input word in the forward direction. Also, for processing the input τ in the backward direction, define Bck ∶ Σ∗ × 2Q → 2Q inductively:

• (iii) Bck(ϵ,X) = X,
• (iv) Bck(τa,X) = Bck(τ, {s ∶ X ⊧ δ(s, a)}).

By (ii) and (iv) we get the following property corresponding to the shift from (τa)τ ′ to τ(aτ ′ ): Bck(τa,Fwd(τ ′ ,X)) = Bck(τ,Fwd(aτ ′ ,X)). Then, an induction on the length of τ shows Bck(τ,Fwd(τ ′ ,X)) = Fwd(ττ ′ ,X) for all τ ′ . Indeed, for the base case τ = ϵ, note that Bck(ϵ, Fwd(τ ′ ,X)) = Fwd(τ ′ ,X) by (iii), and for the general case, say τ = τ ′′a, note that Bck(τ ′′a,Fwd(τ ′ ,X)) = Bck(τ ′′ ,Fwd(aτ ′ ,X)) by the shifting property above, which equals Fwd(τ ′′ (aτ ′ ), X) by the inductive hypothesis, which equals Fwd((τ ′′a)τ ′ , X) as required.

We return to the proof of Theorem 1. We prove, by induction on τ , that q0 ∈ Fwd(τ, V ) iff AR accepts τ R from state V . If τ = ϵ then both sides are equivalent to q0 ∈ V . Consider τ = τ ′a. Then Fwd(τ ′a,V ) = Bck(τ ′a,V ) = Bck(τ ′ , {s ∶ V ⊧ δ(s, a)}) = Bck(τ ′ ,T(V, a)) = Fwd(τ ′ ,T(V, a)).

Thus, q0 ∈ Fwd(τ ′a,V ) = Fwd(τ ′ ,T(V, a)) iff AR accepts (τ ′ )R from state T(V, a) (by induction), iff AR accepts a(τ ′ )R = (τ ′a)R from state V , as required. So, A accepts τ iff AR accepts τ R.

5 From PLTLf /PLDLf to DFA

We take advantage of the single exponential reduction of an AFA to a DFA for the reverse language to get a DFA for PLTLf /PLDLf formulas, which is single exponential in the size of the formula. To do so, we introduce the syntactic notion of swap, which, given a PLTLf /PLDLf formula, produces an LTLf /LDLf formula by syntactically replacing each past operator with its corresponding future operator. Intuitively, ⊖ corresponds to ◯, S corresponds U, ⟪ϱ⟫ corresponds to ⟨ϱsw ⟩, and JϱK corresponds to [ϱsw ], where ϱsw is the regular expression ϱ, with all formulas in test constructs replaced by the corresponding swapped formulas. Formally, we define ϕsw by induction: (i) asw = a (for all a ∈ P) and tt sw = tt ; (ii) (¬ϕ)sw = ¬ϕsw and (ϕ1∧ϕ2)sw = ϕsw 1 ∧ϕsw 2 ; (iii) (⊖ϕ)sw = ◯ϕsw , (iv) (ϕ1 S ϕ2)sw = ϕsw 1 U ϕsw 2 ; (v) (⟪ϱ⟫ϕ)sw = ⟨ϱsw ⟩ϕsw and (JϱKϕ)sw = [ϱsw ]ϕsw ; (vi) φsw = φ, and (ϕ?)sw = (ϕsw )?, and (ρ1 + ρ2)sw = ρsw 1 +ρsw 2 ; (vii) (ρ1; ρ2)sw = (ρsw 1 ; ρsw 2 ), and (ρ∗ )sw = (ρsw )∗ . Similarly, we can swap an LTLf /LDLf formula ϕ into a PLTLf /PLDLf formula ϕsw .

The following lemma summarizes the relation between formulas and their swaps.

Lemma 1. If ϕ is a PLTLf /PLDLf (resp., LTLf /LDLf ) formula, its swap ϕsw is an LTLf /LDLf (resp., PLTLf /PLDLf ) formula of size ∣ϕ∣ such that τ ⊧ ϕ iff τ R ⊧ ϕsw , i.e., LR(ϕ) = L(ϕsw ).

We present two examples that illustrate the syntactic (vs. semantic) relationship between a formula and its swap.

Example 4. Consider the PLTLf formula "inRoom ∧ roomDecontaminated ∧ diamondminus(getPermit)" - a variant of the example in the introduction. Its swapped LTLf formula is "inRoom ∧ roomDecontaminated ∧ ◇(getPermit)". Although the two formulas are syntactically similar, they have different meanings. The former says that the robot is in a decontaminated room and it acquired the permit to enter the room beforehand. The latter says that the robot is in a decontaminated room and later (!) it will get the permit to enter.

Example 5. Consider the LTLf formula "batteryCharged∧ ◇(useNotebook)" and its swapped PLTLf formula "batteryCharged ∧diamondminus(useNotebook)". While the first says that the battery is now charged and you can eventually use the notebook, the PLTLf formula says that you used the notebook in the past, but the battery is charged now.

Now, we are ready to show that transforming PLTLf /PLDLf formulas into DFA can be done in exponential time (vs. double exponential time for LTLf /LDLf formulas):

Theorem 2. For every PLTLf /PLDLf formula ϕ there is an equivalent DFA Aϕ whose size is at most 2O(∣ϕ∣) in the size of ϕ, and which is computable in at most exponential time.

Proof. Swap the PLTLf /PLDLf formula ϕ getting the LTLf /LDLf ϕsw , then construct the AFA Aϕsw , and, finally, build the DFA Aϕ = ARϕsw . By Lemma 1 and Theorem 1 we get that Aϕ has size 2O∣ϕ∣ and L(ϕ) = L(Aϕ).

Hence, we can define the analogue of Algorithm 1 to translate PLTLf /PLDLf formulas into DFA based on Theorem 2.

Algorithm 2: Translating PLTLf /PLDLf to DFA

Given a PLTLf /PLDLf formula ϕ

• 1: Swap ϕ into the corresponding LTLf /LDLf ϕsw (lin)
• 2: Compute AFA for ϕsw (lin)
• 3: Compute DFA from AFA for the reverse language (1exp)

Note that Algorithm 2 returns the DFA corresponding to a PLTLf /PLDLf formula in single EXPTIME (worst-case complexity) vs. 2EXPTIME of Algorithm 1 for the LTLf /LDLf case. This implies that using past temporal formulas reduces the complexity of several problems, as we will see later.

6 PLTLf /PLDLf and LTLf /LDLf

PLTLf /PLDLf offers an exponential advantage over LTLf /LDLf when building the corresponding DFA. However, here we show that they have the same expressive power, and, indeed, they can be translated one into the other. Unfortunately, the translations are quite expensive.

Expressive power of PLTLf . We start by establishing that PLTLf and LTLf have the same expressive power by using first-order logic (FOL) as an intermediate logic. In this setting, FOL formulas are interpreted on finite traces viewed as labeled linear orders, i.e., formulas can use: variables x that vary over instants and that can be quantified existentially and universally; the binary predicate < denoting the order of instants; equality = between instants; and unary (sometimes called monadic) predicates P for the labels; see, e.g., [De Giacomo and Vardi, 2013] for formal definitions).

We start by observing that LTLf and PLTLf can be translated into FOL on finite traces by mimicking the semantics of these logics as FOL formulas, and can be done in linear-time:

Theorem 3. [De Giacomo and Vardi, 2013; Zhu et al., 2019] Both PLTLf and LTLf can be translated into FOL on finite traces in linear-time.

For the converse, it is known that FOL (on finite traces) can be translated into LTLf [Gabbay et al., 1980]. Here, we use this fact to show that FOL can also be translated into PLTLf :

Theorem 4 (cf. [Kamp, 1968]). FOL (on finite traces) can be translated into both LTLf and PLTLf .

Proof. Given an FOL formula ϕ replace x < y by y < x to get an FOL ϕsw for the reverse language, i.e., w ⊧ ϕ iff wR ⊧ ϕsw . Then, translate the FOL formula ϕsw into an equivalent LTLf formula ψ [Gabbay et al., 1980]. Then, the PLTLf formula ψsw is equivalent to the original FOL formula ϕ.

Putting these together, we immediately get:

Theorem5. PLTLf and LTLf have the same expressive power.

Considering the results on LTLf in [De Giacomo and Vardi, 2013], we can now characterize the expressive power of PLTLf .

Theorem 6. PLTLf has exactly the same expressive power as FOL on finite traces, i.e., star-free regular expressions.

Expressive power of PLDLf . Next, we investigate the expressive power of PLDLf .

Theorem 7. RE is as least as expressive as PLDLf .

Proof. Apply Theorem 2 to get a DFA, and then apply Kleene's Theorem to get an equivalent regular expression.

The reverse direction also holds:

Theorem 8. PLDLf is as least as expressive as RE.

Proof. Given a regular expression ϱ compute the reverse regular expression ϱ and return ⟪ϱ⟫start.

Since RE has the same expressive power as Monadic Secondorder Logic (MSO) over finite traces (cf., [De Giacomo and Vardi, 2013]), we get the following characterizations.

Theorem9. PLDLf has the same expressive power as RE, and as MSO on finite traces.

Theorem 10. PLDLf has the same expressive power as LDLf .

Translating between PLTLf and LTLf . The above results give us a way to translate LTLf (resp., PLTLf ) into PLTLf (resp., LTLf ): first, translate LTLf into FOL; then, translate FOL into PLTLf . However, we remark that the transformation of an FOL formula into an LTLf formula, in general, can be non-elementary (i.e., not bounded by any finite tower of exponentials) in the size of the FOL formula [Gabbay, 1987]. Hence, the above translation of LTLf (resp., PLTLf ) into PLTLf (resp., LTLf ) is not trivial. In fact, we can do better by making use of the following result from the literature:

Theorem 11. [Maler and Pnueli, 1990] DFA accepting starfree regular languages can be translated into PLTLf formulas of size at most exponentially larger.

Now, we are ready to provide our translation, which gives us the best known upper bound for the translation, though it remains open whether the bound is tight.

Theorem 12. For every PLTLf (resp., LTLf ) formula ϕ there exists an equivalent LTLf (resp., PLTLf ) formula whose size is at most triply exponential in the size of ϕ, and which is computable in at most triply exponential time.

Proof. Given a PLTLf formula ϕ, build an equivalent DFA Aϕ by Theorem 2. Note that the DFA may be exponentially larger than ϕ. Reverse all transitions to get an NFA ARϕ that accepts the reverse of the language of Aϕ, then determinize this NFA to get an equivalent DFA A′R ϕ . Note that A′R ϕ may be exponentially larger than ARϕ . Now, apply Theorem 11 to transform this DFA into an equivalent PLTLf formula ψ. Finally, form the swap ψsw for the reverse language of ψ. Then, ψsw is the LTLf formula equivalent to the PLTLf formula ϕ. Note that we reversed the language twice, and we incurred in three exponential blowups.

Similarly, we can obtain a PLTLf formula from an LTLf one. From an LTLf formula ϕ, build an equivalent DFA Aϕ that may be double-exponentially larger than ϕ, and, then, apply Theorem 11 to get an equivalent PLTLf formula which may be single-exponentially larger.

Translating between PLDLf and LDLf . Next, we turn to PLDLf and LDLf . Again, the bound (and algorithm) in the theorem below is the best known upper bound for the translation. It is open whether the bound is tight.

Theorem 13. For every PLDLf (resp., LDLf ) formula ϕ there exists an equivalent LDLf (resp., PLDLf ) formula whose size is at most doubly exponential in the size of ϕ, and which is computable in doubly exponential time.

Proof. From a PLDLf formula ϕ build, an equivalent DFA that may be exponentially larger (Theorem 2), then, using Kleene's Theorem, convert this to a regular expression that may be exponentially larger, and, finally, convert this to an LDLf formula with constant blow-up [De Giacomo and Vardi, 2013]. The other case (from LDLf to PLDLf ) follows by considering the swapped formulas.

In light of the discussion in this section, we observe that while PLTLf /PLDLf allows for exponentially smaller equivalent DFA compared to LTLf /LDLf , we cannot try to translate LTLf /LDLf into PLTLf /PLDLf to take advantage of this result, since the translation itself is too expensive. Hence, the properties of interest should be naturally expressible directly in PLTLf /PLDLf to get the exponential improvement.

7 Impact of Adopting PLTLf /PLDLf

The exponential gain in transforming PLTLf /PLDLf formulas into DFAs, with respect to LTLf /LDLf , is reflected in an exponential gain in solving a variety of forms of sequential decision making problems involving temporal specifications. We start by focusing on Planning.

Planning in fully observable nondeterministic planning domains (FOND) for LTLf /LDLf goals has been studied in [Camacho et al., 2017; De Giacomo and Rubin, 2018; Camacho et al., 2018]. A (rooted) fully observable nondeterministic domain is a tuple D = ⟨P,A, S, s0, tr⟩ where: (i) P is a set of fluents (atomic propositions); (ii) A is a set of actions (atomic symbols); (iii) S = 2P is the set of domain states; (iv) s0 is the initial state (initial assignment to fluents); (v) (s, a, s′ ) ∈ tr represents action effects (including frame assumptions), and implicitly also actions preconditions. Since a domain is assumed to be represented compactly (e.g. in PDDL), we consider the size of the domain as the cardinality of P, i.e., logarithmic in the number of states (see e.g., [Geffner and Bonet, 2013]). We are interested in the case where the goal is given as a PLTLf /PLDLf goal formula ϕg over fluents P . A plan f is a strong solution to D for goal ϕg if every trace following the plan f of D is finite and satisfies ϕg. To find such a plan we use the automata-based technique in [De Giacomo and Rubin, 2018], but exploit the fact that PLTLf /PLDLf goals give us a single exponential DFA.

Theorem 14. Solving FOND for PLTLf /PLDLf goals is EXPTIME-complete in the domain and EXPTIME-complete in the PLTLf /PLDLf goals.

Contrast this result with the LTLf /LDLf case, where FOND planning is EXPTIME-complete in the domain (compactly represented) and 2EXPTIME-complete in the goal [De Giacomo and Rubin, 2018]. As mentioned in Section 6, the exponential gain is only achieved for properties expressed directly in PLTLf /PLDLf . If we first express the specification in LTLf /LDLf and then translate it into PLTLf /PLDLf , we lose the advantage due to a blow-up in the translation. Thus, our approach yields an improvement for problems that can natively be specified in PLTLf /PLDLf , without resorting to LTLf /LDLf at all. The above construction can be adapted to handle (stochastically) fair domains [De Giacomo and Rubin, 2018; Aminof et al., 2020] with the same exponential advantage.

Note that if the domain is deterministic the difference between LTLf /LDLf and PLTLf /PLDLf disappears because in the former case we can directly work with an NFA, since it is sufficient to solve simple reachability, i.e., nonemptiness (cf. [De Giacomo and Rubin, 2018]). Hence, in both cases, the complexity becomes PSPACE in the domain and in the goal. The crux of the above construction is that starting from the PLTLf /PLDLf formula we build an exponential DFA, which is then combined through a polynomial operation (the product) with the planning domain. An analogous line of reasoning can be exploited to show an exponential improvement in several other contexts as we will show in what follows.

Solving MDPs with non-Markovian rewards [Bacchus et al., 1996; Thi´ebaux et al., 2006; Brafman et al., 2018] with PLTLf /PLDLf rewards is EXPTIME-complete in the domain and EXPTIME in PLTLf /PLDLf rewards, while the latter is 2EXPTIME-complete for LTLf /LDLf rewards [Brafman et al., 2018].

Reinforcement Learning where rewards are based on traces [De Giacomo et al., 2019; Camacho et al., 2019] with PLTLf /PLDLf rewards also gain the exponential improvement.

Planning in non-Markovian domains [Brafman and De Giacomo, 2019a], with both the non-Markovian domain and the goal expressed in PLTLf /PLDLf is EXPTIME-complete in the domain and in the goal, vs. 2EXPTIME-complete in the domain and in the goal in the case these are expressed in LTLf /LDLf .

Solving non-Markovian decision processes [Brafman and De Giacomo, 2019b], with both the system dynamics and the rewards expressed using PLTLf /PLDLf , is EXPTIMEcomplete in the domain and in the rewards specification. Again, this is an exponential improvement both in the domain and the rewards wrt the case of LTLf /LDLf .

8 Conclusion

We reviewed PLTLf and its extension PLDLf , which have an exponential advantage over LTLf /LDLf when computing the corresponding DFA, which, in turn, positively impacts several problems in AI. However, to take advantage of this exponential improvement, the properties of interest must be directly expressed in PLTLf /PLDLf because the translation between LTLf /LDLf and PLTLf /PLDLf dominates the exponential advantage of working with PLTLf /PLDLf .

Acknowledgments

Work partially supported by the European Research Council under the European Union's Horizon 2020 Programme through the ERC Advanced Grant WhiteMech (No. 834228).