Besides LTL2AUT, we have also extended two state-based algorithms, namely GPVW and MoDeLLa, and two transitions-based algorithms, namely Couvreur and LTL2BUCHI, to support past operators.
4.5.1 Extended GPVW
The extension to GPVW, resulting in Extended GPVW, is easy as GPVW and LTL2AUT were presented in a uniform way in [17]. GPVW+ is also presented in the uniform way but cannot be similarly extended because the requirement for a state s to satisfy a formula f in GPVW+ is as strict as in GPVW but some useful formulae are discarded in the cover computation. That is, in GPVW+, SATISFY (F, f ) returns true iff f ∈ F
while STORE (f ) returns true iff f is an U -formula or f is the right argument of an U -formula. Consider the translation of 2p by GPVW+. The successor of the− initial state q0 = { 2p} computed by Cover is q− 1 = {p, ∼2p}. Since q− 0 does not satisfy 2p imposed by q− 1, we have to refine q0 by 2p and obtain a refined state− q2 = { 2p, p,− ∼2p}. Then, the successor of q− 2 computed by Cover is q1. In GPVW+, q2 does not satisfy 2p imposed by q− 1 (SATISFY (q2,2p) = false) because− 2p 6∈ q− 2. However, q2 does satisfy 2p semantically. In this case, GPVW+ will construct a label-− on-state NGW that accepts nothing for 2p, which is incorrect.−
4.5.2 Extended MoDeLLa
MoDeLLa basically follows the construction of LTL2AUT but uses a different cover computation procedure and three additional improvements. Since the cover com-putation in MoDeLLa also satisfies Formula 4.1, we can extend MoDeLLa, resulting in Extended MoDeLLa, in the same way with special cares of the additional improve-ments.
The first improvement in MoDeLLa is pruning fair sets, which can be performed after a label-on-state NGW is obtained. Thus, this improvement won’t affect our extension.
The second improvement in MoDeLLa merges states that have the same -formulae and behave the same in the acceptance condition. Thus, a state in MoDeLLa may contains several sub-states. In MoDeLLa, a state is a To make this improvement work with our backtrace procedure, we merge states if they also have the same −- and
∼-formulae. Thus, every sub-state in a state have the same backward requirements.
Moreover, when refining a state, we refine its sub-states separately as they have different satisfied formulae.
The third improvement is branching postponement, which rewrites f ∨ g into (f ∨ g) if it is safe. Therefore, in the cover computation, two states s = F ∪ { f1, f2, . . . , fn} and t = G ∪ { g1, g2, . . . , gm} may be merged to F ∪ { (f1∧ f2∧ · · · ∧ fn∨ g1∧ g2∧ · · · ∧ gm)} (with s and t as the sub-states) if the merge is safe and F = G. This improvement merges only future formulae and produces larger merged states similar in the first improvement. Thus, we require that states to be merged by branching postponement must have the same backward requirements and we refine sub-states separately.
4.5.3 Extended Couvreur
Couvreur relies also on tableau rules to expand a formula into several cases that satisfy the formula, which is similar to the cover computation. Unlike those state-based translation algorithms, Couvreur puts acceptance conditions on transitions instead of states, produces transition-based NGW (NTGW), and uses BDD (Binary Decision Diagram) [7] to encode automata.
A state in Couvreur is a set of formulae to be satisfied by the following transitions and successive states. When computating the successors of a state s, Couvreur first expands the formulae in s to a set C, of which an element in C is a possible way to satisfy all formulae in s. Then, for each c ∈ C, Couvreur creates a successor →c and a transition with literals in c as the label. For example, in translating3p, Couvreur starts with a single initial state q0 = {3p} instead of decomposing 3p immediately.
Since 3p can be expanded by the tableau rules into {{p}, { 3p}} with two cases to satisfy 3p, two transitions t1 and t2 are created, of which t1 has a label p and successor {true} while t2 has label true and successor q0. The NTGW produced by Couvreur is shown in Figure 4.3.
Figure 4.3: The NTGW produced by Couvreur for 3p
A problem appears immediately is that when doing backtrace, we want to put formulae that should be satisfied in a state. Therefore, a state may contain formulae to be satisfied by the following transitions and successors and formulae to be satisfied by itself. We will be hard to distinguish formulae in a state with different intentions.
A solution is to add a operator to every formula to be satisfied next and compute the successors of a state s by decomposing the formulae→s . Besides, after a backtrace, we may add literals to a state. Those literals should be included in all outgoing transitions.
Another problem is that the translation may be incorrect if we backtrace the initial state. For example, consider the translation of ∼p, which is equivalent to true. With the previous solution, the initial state is q0 = { ∼p} and the successor candidate of the initial state is q1 = { ∼p}. Since q0 does not satisfy p imposed by q1, we may need to do a backtrace. If we do, we will refine the initial state and put a p in it. Such p will appear in all outgoing transitions of the refined state. As a result, the constructed NTGW will only accept words start with a p, which is incorrect.
Thus, when adding an outgoing transition from the initial state to a successor, we always skip the backtrace and really add the transition if the successor contains no
−-formula. However, self-loop transitions of the initial states may need backtrace because they may appear several steps after the initial state but the backtrace is omitted anyway now. To avoid this problem, we add ∼false to the initial state and
therefore the initial state will has no predecessor.
4.5.4 Extended LTL2BUCHI
Compared to GPVW, MoDeLLa, and Couvreur, the extension to LTL2BUCHI is the most complicated one because it adapts the Node data structures and recursive procedure in GPVW and GPVW+ [34]. A node in LTL2BUCHI contains formulae to be satisfied. In each iteration of the recursive procedure, a formula in a node is expanded by the tableau rules. If the formula is expanded into two disjunctive cases, the node is split into two nodes. If no formula in a node can be expanded, the node is fully expanded.
Once a node is fully expanded, if there is no duplicate node, a state will be created for it and a new node will be created to satisfy the -formulae of the fully expanded node.
To adapt our backtrace procedure to LTL2BUCHI, we perform backtrace when a node is fully expanded. During the expansion of nodes, the refinement relation are maintained carefully because nodes may not be fully expanded and nodes may be merged into other nodes. When splitting a node n into two nodes n1 and n2, if n refines some node m, n1 and n2 should also refine m. Moreover, LTL2BUCHI merges nodes that have the same -formulae as in MoDeLLa. Unlike MoDeLLa, LTL2BUCHI does not maintain sub-nodes of nodes. Thus, we merge nodes containing past for-mulae if they are exactly the same.
Both LTL2BUCHI and Couvreur produce NTGWs and put the formula to be translated in the initial state. Therefore, some modifications applied in Couvreur are also required in LTL2BUCHI. These modifications are listed below.
• Incoming transitions of the initial state is forbidded.
• Never refine the initial state.
• Any successor of the initial state cannot contain previous formulae.