In this section, we present our algorithm that translates, in an incremental fashion, a given PTL formula to a label-on-state NGW. The part of our algorithm that deals with the future fragment of PTL (i.e., LTL) is essentially LTL2AUT. This is to be extended with a procedure called backtrace to handle past operators. The extended algorithm will be referred to as Extended LTL2AUT.
Consider the translation of an LTL formula, it is sufficient to recursively compute successors of existing states until no more states can be created. The translation becomes more complex if past operators are involved. Whenever a state s contain-ing past formulae is created, these past formulae impose additional constraints on the predecessors of s. However, when we created those predecessors, the constraints were not taken into account and thus the predecessors and s may be backward incon-sistent. Besides, the predecessors and s may be forward inconsistent if the imposed constraints contain future formulae which in turn impose additional requirements back on s. To resolve backward inconsistency, a backtrace is applied whenever we are trying to add a transition which is backward inconsistent. During the backtrace, states may be created to refine the predecessors. For forward inconsistency on a state, we just recompute its successors.
4.2.1 The Translation Algorithm
Given a PTL formula ϕ in NNF, our goal is to translate ϕ to a label-on-state NGW Aϕ which accepts exactly all the models of ϕ. The core translation algorithm Cre-ateAutomaton is based on create automaton structure except that backtrace is done when adding transitions (line 8) and certain states cannot be initial states anymore (lines 9-11).
There are several global variables: the set U is used to keep unprocessed states, all created states will be added to the set Q, candidates of initial states will be added to the set I, δ is a transition function, κ records the performed backtraces, and γ is a mapping used to track refinement relations.
The algorithm starts by computing the cover of ϕ which serves as the initial states (line 1). Initially, the transition function δ, the backtrace records κ and the refinement function γ are all empty (line 1).
As long as the set U is not empty, a state s in U is removed (line 3). The forward expansion of s is done by computating its successors as the cover of→s (line 4). For each successor t, it is added to the set Q and U for further process if it is a new state (lines 5-7). The transition from s to its successor t is added by the function
AddTransition (line 8) which ensures that backward inconsistency is found and resolved.
After creating all needed states and transitions and resolving all inconsistency, the algorithm fixes the set I by removing states containing −-formulae (lines 9-11) because −-formulae never hold initially.
The resulting generalized B¨uchi automaton Aϕ = (Σ, Q, I, δL, F ) can be defined as follows:
• Σ = 2AP where AP is the set of atomic propositions occuring in the input formula ϕ.
• L(s) = {a ∈ Σ : s+⊆ a and a ∩ s− = ∅}.
• F = {Ff U g : f U g is a subformula of the input formula ϕ} where
Ff U g = {s ∈ Q : SATISFY (s, f U g) implies SATISFY (s, g)}.
4.2.2 The Backtrace Procedure
A backtrace from t to s is needed if we are trying to add a transition from s to t but s and t are not backward consistent. The set κ is used to remember the resolved inconsistency so that the backtrace from a state t to a state s is never performed more than once (lines 1-2).
To resolve potential inconsistency, we cannot simply impose the constraint ←t on s because ←t may contain formulae which are not required by other successors of s. For example, consider the intermediate translation result of 2(p → −(q U r)) by LTL2AUT in Figure 4.1. We are trying to add a transition from s0 to one of its successors, s1. Although state s1 requires that its predecessor must satisfy q U r,
Algorithm 5 BackTrace(s, t)
1:
if (s, t) 6∈ κ then2:
κ = κ ∪ {(s, t)}3:
for r ∈ Cover (←t ∪ s) do4:
γ(s) = γ(s) ∪ {r}5:
if r 6∈ Q then6:
Q = Q ∪ {r}7:
U = U ∪ {r}8:
if s ∈ I then9:
I = I ∪ {r}10:
for u ∈ {u : δ(u, s)} do11:
AddTransition(u, r)s0 = { ✷((¬p ∨ −(q U r))), ¬p} s1 = { ✷((¬p ∨ −(q U r))), −(q U r)}
Figure 4.1: Part of an intermediate result of translating 2(p → −(q U r)).
s0 = { ✷((¬p ∨ −(q U r))), ¬p} s1 = { ✷((¬p ∨ −(q U r))), −(q U r)}
s2 = { ✷((¬p ∨ −(q U r))), (q U r), ¬p, q}
Figure 4.2: Part of an intermediate result of translating 2(p → −(q U r)) after the first backtrace
we can neither add (1) r nor (2) q and (q U r) to s0 because the infinite word (¬p¬q¬r)ω, which is a model of2(p → −(q U r)), would be rejected.
Note that a symbolic state (i.e., an element in a cover) is used to represent a set of states which all satisfy the set of formulae in the symbolic state. A backward inconsistency here does not necessarily mean all states represented by s fail to satisfy the requirement. Thus the solution is to keep the original predecessor s but compute satisfactory predecessors.
The satisfactory predecessors are refined from the original predecessor s by com-puting the cover of ←t ∪ s (line 4). The refinement relation is kept in the function
γ where r ∈ γ(s) indicates that r is a refined state of s (line 5). For each refined predecessor r, we add it to the sets Q and U if it is a new state (lines 6-8). Since r is a refined state of s, r should be an initial state if s is (lines 9-10). Moreover, all predecessors of s should have transitions to r as well (lines 11-12). So far, we get the intermediate result of the example shown in Figure 4.2 by processing the refined predecessor s2 of s0 first.
After building the history of the refined state r, we need to expand its future.
Although r is a refined state of s, we cannot simply add a transition from r to the original successor t of s because this may induce forward inconsistency. For example, if we add a transition from s2 to s1 in Figure 4.2, forward inconsistency occurs because s1 does not satisfy q U r. Thus, new refined states are added to U to be processed later.
4.2.3 The AddTransition Procedure
Given two states s and t, the function AddTransition not only adds transitions from s to t, but also adds other transitions and invokes backtrace if necessary. First, we check if there is a backward inconsistency between s and t (line 1). If there is no backward inconsistency, we add a transition from s to t and try to add a transition from s to every refined state r of t because r satisfies more formulae than t including all constraints from s (lines 2-4). If a backward inconsistency between s and t is found, the backtrace procedure is performed (line 6).