We consider the transformation of propositional linear time temporal logic formulae into a clause normal form, called Separated Normal Form, suitable for resolution calculi. In particular, we investigate the e ect of applying various pre-processing techniques on characteristics of the normal form and determine the best combination of techniques on a large collection of benchmark formulae.
Clause normal forms are the foundation of most resolution-based calculi and
such calculi exist for a wide range of logics, including propositional, rst-order,
modal and temporal logics. Given a formula ', the clause normal form of '
is typically computed using a combination of equivalence or satis ability
preserving rewrite steps, including simpli cation as a special case, and renaming,
which replaces complex subformulae by new propositional variables and adds
de nitional clauses for the new propositional variables. Variations in the normal
form can greatly in uence the performance of resolution-based reasoning systems
and transformation procedures that compute clause normal forms typically aim
to produce fewer and/or shorter clauses for a given formula. For propositional
and rst-order logic the computation of such `small' clause normal forms is
wellstudied [
In this paper we consider a clausal normal form for propositional linear time
temporal logic (PLTL), called Separated Normal Form (SNF). This normal form
was originally devised as the basis of a clausal resolution calculus and decision
? The second and third authors were partially supported by the EPSRC funded RAI
Hub FAIR-SPACE (EP/R026092/1) and the EPSRC funded programme grant S4
(EP/N007565/1). The third author was also partially supported by the EPSRC
funded RAI Hub RAIN (EP/R026084/1).
procedure for PLTL [
In following we revisit the problem of computing the SNF of a given PLTL formula. In particular, we determine the e ect of applying various pre-processing techniques during the computation.
The paper is organised as follows. We present the language of PLTL in Section 2. The Separated Normal Form is given in Section 3, where the techniques used for producing the normal form are also presented. Experimental evaluation is discussed in Section 4. 2
We consider a particular variety of temporal logic, which is based on a linear,
discrete model of time with nite past and in nite future [
The temporal operators supplied in the language operate over a sequence of
distinct `moments' in time. In this version, only future-time operators are used.
It is possible to include past-time operators in the de nition of the logic, as in
[
Formulae are constructed from a denumerable set P = fp; q; p0; q0; p1; q1; : : :g of propositional variables and a set of connectives3. In addition to the standard propositional connectives (:; _; ^; !; $) we use a set of temporal operators consisting of `3' (sometime in the future), `2' (always in the future), `#' (in the next moment in the future), `U ' (until ), and `W' (unless or weak until ). The set of well-formed formulae of PLTL, denoted by WFFPLTL , is inductively de ned as the smallest set satisfying: { the propositional variables are in WFFPLTL ; { > and ? are in WFFPLTL ; { if ' and are in WFFPLTL , then so are :', (' !
# ', (' U ), (' W ); { if '1, . . . , 'n, n 1, are in WFFPLTL , then so are ('1 ^ ('1 _ _ 'n). ), (' $ ), 3 ', 2 ', ^ 'n) and
A literal is a propositional variable or its negation. An eventuality is a formula of the form 3 ', for a well-formed formula '. An elementary formula is one of the logical constants >, ?, a propositional literal or a formula of the form # ', for an arbitrary formula '. A position is a word over the natural numbers. For a formula ', the set pos(') of positions of ' is de ned as follows: 3 We consider the connectives that re ect the input language of our tool ltl2snf and that occur in `real-world' or benchmark formulae, instead of restricting ourselves to a minimal, expressively complete set of connectives. { the empty word 2 pos('); { if ' is of the form :'1, # '1, 2 '1, or 3 '1 for some formula '1 and 2 pos('1) then 1: 2 pos('); { if ' is of the form ('1 ! '2), ('1 $ '2), ('1 U '2), or ('1 W '2) and 2 pos('i) for i 2 f1; 2g, then i: 2 pos('); and { if ' is of the form ('1 ^ ^ 'n) or ('1 _ _ 'n) and 2 pos('i) for i 2 f1; : : : ; ng, then i: 2 pos(').
For a formula ' and position at position as follows:
2 pos('), we de ne the subformula 'j of ' { 'j = '; { if ' is of the form :'1, # '1, 2 '1, or 3 '1 for some formula '1 and = 1: , then 'j = '1j ; { if ' is of the form ('1 ! '2), ('1 $ '2), ('1 U '2), or ('1 W '1) and = i: for i 2 f1; 2g, then 'j = 'ij ; and { if ' is of the form ('1^ ^'n) or ('1_ _'n) and = i: for i 2 f1; : : : ; ng, then 'j = 'ij .
The polarity pol('; ) of a subformula occurring at position ' is de ned as follows: in a formula { pol('; ) = 1; { if = :1 and 'j is of the form # '1, 2 '1, or 3 '1, then pol('; ) = pol('; ); { if = :1 and 'j is of the form :'1 or ('1 ! '2), then pol('; ) = pol('; ); { if = :2 and 'j is of the form ('1 ! '2), then pol('; ) = pol('; ); { if = :i with i 2 f1; 2g and 'j is of the form ('1 U '2) or ('1 W '2) then pol('; ) = pol('; ); { if = :i with i 2 f1; : : : ; ng and 'j is of the form ('1 ^ ^ 'n) or ('1 ^ ^ 'n), then pol('; ) = pol('; ); { if = :i with i 2 f1; 2g and 'j is of the form ('1 $ '2) then pol('; ) = 0.
A formula ' at position is of positive polarity (resp. negative polarity ) if pol('; ) = 1 (resp. pol('; ) = 1). A formula ' is pure if, for all positions and 0, pol('; ) = pol('; 0) 6= 0.
PLTL-formulae are interpreted over in nite sequences of states = (si)i2N such that each si, 0 i, is a set of propositional variables. The notation ( ; i) j= ' denotes the truth of a formula ' in the model at the state index i, i 2 N. For any formula ', model , and state index i, i 2 N, then either ( ; i) j= ' holds or ( ; i) j= ' does not hold, where the latter is denoted by ( ; i) 6j= '. The semantics of WFFPLTL can now be given as follows: De nition 1. Let ' and index of a state in .
{ ( ; i) j= > be formulae in WFFPLTL ,
a model, and i 2 N the { ( ; i) 6j= ? { ( ; i) j= p if, and only if, p 2 si, where p 2 P { ( ; i) j= :' if, and only if, ( ; i) 6j= ' { ( ; i) j= ('1 ^ ^ 'n) if, and only if, for every i, 1 i { ( ; i) j= ('1 _ _ 'n) if, and only if, for some i, 1 i { ( ; i) j= (' ! ) if, and only if, ( ; i) j= :' or ( ; i) j= { ( ; i) j= (' $ ) if, and only if, ( ; i) j= (' ! ) and ( ; i) j= ( { ( ; i) j= # ' if, and only if, ( ; i + 1) j= ' { ( ; i) j= 3 ' if, and only if, 9k; k 2 N; k { ( ; i) j= 2 ' if, and only if, 8k; k 2 N, if k { ( ; i) j= (' U ) if, and only if, 9k; k 2 N; k
i j < k, then ( ; j) j= '. { ( ; i) j= (' W ) if, and only if, either ( ; i) j= ' U i; ( ; k) j= ' i, then ( ; k) j= ' i; ( ; k) j= and 8j; j 2 N, if or ( ; i) j= 2 ': n, ( ; i) j= ' n, ( ; i) j= 'i ! ')
A formula ' is satis able if there is a model such that ( ; 0) j= '. If ( ; 0) j= ' for all models , then ' is said to be valid, denoted by j= '. Two PLTL-formulae ' and are equi-satis able if, and only if, ' is satis able if, and only if, is satis able. Two PLTL-formulae ' and are equivalent if, and only if, for every model and every state index i, i 2 N, ( ; i) j= ' if and only if ( ; i) j= 3
Formulae in the language of PLTL can be transformed into a normal form called
Separated Normal Form (SNF) [
n, n 2 N, is in one of the following three forms. where n; m literals.
0 and for every i, 1 m, and j, 1 j
n, li and lj0 are m _ li i=1 m n 2( _ li _ _ # lj0 ) i=1 j=1 m 2( _ li _ 3 l10) i=1
^ 1 i n
Ci i (global clause) (eventuality clause)
Note that SNF clauses do not contain occurrences of the operators U and W, the operator 2 only occurs as principal operator of a clause, and nesting temporal operators is limited to the combinations 2 and #; and 2 and 3.
Every PLTL-formula ' can be transformed into an equi-satis able formula
in SNF. Fisher, Dixon and Peim [
It is easy to see that 1 will not always produce a normal form with the smallest number of clauses. For example,
'1 = 2(:q _ : # :p) is equivalent to 2(:q _ # p) which is in normal form, but, according to Equation (8) in Figure 1, 1('1) would produce a conjunction of two clauses. This could be avoided by converting formulae to negation normal form (NNF) before applying 1, using the rewrite rules for temporal formulae given in Figure 2 and the usual equivalences for classical formulae. The formula
'2 = 2(:q _ (p U p)) is equivalent to 2(:q _ p) which again is in normal form, but, according to Equation (16) in Figure 1, 1('2) would produce a conjunction of ve clauses. This could be avoided by simpli cation using well-known equivalences among temporal formulae, which are given in Figure 3, together with the well-known corresponding equivalences among Boolean formulae.
Using such equivalences we can also extend or reduce the scope of
temporal operators. Prenexing corresponds to moving modal operators outwards a
formula. Analogously, anti-prenexing corresponds to moving modal operators
inwards a formula. For example, anti-prenexing would replace 3(p _ q) by the
equivalent (3 p _ 3 q) while prenexing would do the opposite. Here we only
discuss the anti-prenexing technique. In rst-order logic, it has been shown [
if is not a disjunction of literals 1(2(:q _ (' ! ))) = 1(2(:q _ :' _ )) 1(2(:q _ :(' ! ))) = 1(2(:q _ ')) ^ 1(2(:q _ : )) 1(2(:q _ :#')) = 1(2(:q _ #q0)) ^ 1(2(:q0 _ :')) 1(2(:q _ 2')) = 1(2(:q _ 2q0)) ^ 1(2(:q0 _ '))
if ' is neither a literal nor a constant 1(2(:q _ 2l)) = 2(:q _ l) ^ 2(:q _ q0)
^2(:q0 _ #l) ^ 2(:q0 _ #q0) 1(2(:q _ :2')) = 1(2(:q _ 3:')) 1(2(:q _ 3')) = 1(2(:q _ 3q0)) ^ 1(2(:q0 _ '))
if ' is neither a literal nor a constant 1(2(:q _ :3')) = 1(2(:q _ 2:')) 1(2(:q _ (' U ))) = 1(2(:q _ (q0 U ))) ^ 1(2(:q0 _ '))
if ' is neither a literal nor a constant 1(2(:q _ (' U ))) = 1(2(:q _ (' U q0))) ^ 1(2(:q0 _ ))
if is neither a literal nor a constant 1(2(:q _ (l1 U l2))) = 2(:q _ 3l2) ^ 2(:q _ l1 _ l2) ^2(:q _ q0 _ l2) ^ 2(:q0 _ #l1 _ #l2) ^2(:q0 _ #q0 _ #l2) 1(2(:q _ :(' U ))) = 1(2(:q _ (q0 W q00))) ^2(:q00 _ q0) ^ 2(:q00 _ q000) ^ 1(2(:q0 _ : )) ^ 1(2(:q000 _ :')) 1(2(:q _ (' W ))) = 1(2(:q _ (q0 W ))) ^ 1(2(:q0 _ '))
if ' is neither a literal nor a constant 1(2(:q _ (' W ))) = 1(2(:q _ (' W q0))) ^ 1(2(:q0 _ ))
if is neither a literal nor a constant 1(2(:q _ (l1 W l2))) = 2(:q _ l1 _ l2) ^ 2(:q _ q0 _ l2) ^2(:q0 _ #l1 _ #l2) ^2(:q0 _ #q0 _ #l2) 1(2(:q _ :(' W ))) = 1(2(:q _ (q0 U q00))) ^2(:q00 _ q0) ^ 2(:q00 _ q000) ^ 1(2(:q0 _ : )) ^ 1(2(:q000 _ :')) 1(') = '; if no other rule applies (2) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18) (19) (20) (21) (22) nnf(: # ') = # nnf(:') (23) nnf(:(' U )) = (nnf(: ) W nnf(:' ^ : )) (29) nnf(: 3 ') = 2 nnf(:') (25)
nnf(# ') = # nnf(') (26) As 2 2 is equivalent to 2 , for any formula , after simpli cation, we obtain the formula 2 p. Figure 4 shows the equivalences that can be used to either extend or reduce the scope of temporal operators. For anti-prenexing the equivalences are used as rewrite-rules from left to right. For instance, the anti-prenex normal form of the formula # 2 # 2 # 2 p is 2 2 2 # # # p, which can then be simpli ed to 2 # # # p.
Since 1 only preserves satis ability, we can go even further for the formulae '1, '2 and '3, given before. In all these formulae the propositional variable p only occurs with positive polarity. In analogy to propositional logic, we can apply pure literal elimination, that is, we replace variables that only occur positively (resp. negatively) by > (resp. ?), and then simplify. For '1, '2, and '3 we obtain > as result.
Finally, a peculiarity of the normal form transformation by 0 and 1 is that for a formula ' in normal form, 0(') will not be the same as '. Say, '4 is (q2 ^2(:q2 _p)). Then 0('4) = (q1 ^ 1(2(:q1 _((q2 ^2(:q2 _p))))). Computing 1 will involve Equation (10) in Figure 1, creating four additional clauses. We can ameliorate this problem by modifying 1 so that it treats 2(:q1 _ 2 ') like 2(:q1 _ ') for the speci c propositional variable q1 used by 0. The next lemma 3('1 _ (62) (63) (64) (65) (66) (67) (68) (69) (70) (71) (72) shows that this simpli cation step in the transformation is correct, that is, that satis ability is preserved.
Lemma 1. Let ' be a PLTL-formula and q1 a propositional variable not
occurring in '. Then, 2 ' is satis able if, and only if, q1 ^ 1(2 ') is satis able.
Proof. ()) By the results in [
(() If q1 ^ 1(2 ') is satis able, then there is a model such that ( ; 0) j=
q1 ^ 1(2 '). We construct a model 0 such that s00 = s0 [ fq1g and, for all
i > 0, s0i = si n fq1g. It follows, by construction, that (3) ( 0; 0) j= q1. As
( ; 0) j= 1(2 ') and the evaluation of 1(2 ') does not depend on the evaluation
of q1, we have that ( 0; 0) j= 1(2 ') and, from the de nition of satis ability of
disjunctions, (4) ( 0; 0) j= :q1 _ 1(2 '). Also, by construction, for all i > 0,
( 0; i) j= :q1. Thus, for all i, i 2 N, (5) ( 0; i) j= :q1 _ 1(2 '). From (4) and
(5), it follows that, for all i 0, ( 0; i) j= :q1 _ 1(2 '). From the de nition of
satis ability of the 2 operator, we obtain that (6) ( 0; 0) j= 2(:q1 _ 1(2 ')).
From (3) and (6), we have that ( 0; 0) j= q1 ^ 2(:q1 _ 1(2 ')). By the results
in [
We have implemented 0, 1 and the techniques described in Section 3. The tool
ltl2snf is a transformer written in C, which takes a formula in the language of
PLTL and produces a set of SNF clauses in the syntax used by TRP++ [
The techniques for pre-processing the input are coded as independently as
possible in order to allow for the easy addition and testing of new features. By
default, for a given PLTL-formula ', ltl2snf just computes 0(nnf(')). The
resulting formula is in simpli ed form: repeated literals, the constant ?, and
the formulae # ? and 3 ? within a clause are deleted; and clauses containing
the constant >, l and :l, # l and # :l, for some literal l, and the formulae
# > or 3 > are removed. Once such a set of SNF clauses has been computed, no
further simpli cation is performed. In particular, clause subsumption or variable
elimination techniques such as those described in [
The main loop of ltl2snf is schematically presented in Figure 5, where the input simplication function returns the number of transformation steps given by the optional techniques enable by the user, namely: { -ple for pure literal elimination together with constant propagation, and { -simp for simpli cation.
Two more processing techniques can be enabled by the options: { -aprenex for the anti-prenexing transformation, which is performed by the function aprenex transformation in Figure 5; and { -isnf for the modi ed version of 1, which is implemented as part of the transformation into the normal form (snf transformation). Both the simpli cation procedure and the transformation into anti-prenex normal form are performed until a xed-point is reached, that is, no further transformation/simpli cation is possible. We also note that simpli cation and pure literal elimination are performed before the transformation into Negation Normal Form, as this allows for better memory use and performance. For instance, the NNF of
:(p1 U (p2 U p3)) results in
((:p3 W (:p2 ^ :p3) W (:p1 ^ (:p3 W (:p2 ^ :p3)))) where all literals are pure. It is easy to see that for formulae with similar structure, the result of the translation into NNF is exponential in the size of the original formula. Applying pure literal elimination together with constant propagation to the original formula avoids this problem. For this particular example, the resulting formula is >.
To evaluate the e ectiveness of each technique and their combinations we
have used a set of PLTL-formulae collected by Schuppan and Darwiche [
Table 1 shows syntactic properties of these categories. The random category contains more formulae than all other categories combined. However, the combined size of its formulae is smaller than that of the application and semi-random #Temporal Avg #Boolean #For- Operators Temporal Operator Boolean Total Avg Category mulae Occurrences Operators Occurrences Variables Size Size application 542 65733 121.3 194029 6772 381525 703.9 pattern 407 30703 75.4 15051 24068 72739 178.7 random 4000 87734 21.9 141048 11542 311636 77.9 semi-random 1187 128146 108.0 234298 19163 523890 441.4 total 6136 312316 50.9 584426 61545 1289790 210.2 categories. The pattern category is the smallest, both in terms of number of formulae and their combined size. It is the only category in which the number of temporal operator occurrences is larger, and signi cantly so, than the number of occurrences of Boolean operators. On the other hand, the average number of temporal operators per formula is considerably higher for the application and semi-random categories than the others. The application category is the only one where formulae contain the Boolean constants > and ?, on average 13 occurrences in each formula.
Besides considering the e ect of various pre-processing techniques
implemented in ltl2snf on the normal form, we have also compared ltl2snf with the
latest version of translate [
Figure 6 shows for particular combinations of ltl2snf and translate options for each category (a) the average number of fresh propositional variables introduced in the transformation, (b) the average number of clauses produced, (c) the average size of the normal form and (d) the average computation time. Note that ltl2snf always computes the NNF of the input formula. We therefore cannot investigate whether this in itself has a positive or negative e ect.
Table 1 together with Figures 6(a) and 6(b) show that on average the number
of fresh propositional variables introduced in the SNF transformation as well as
the number of clauses produced is much lower than the worst case upper bound
established in [
application pattern random semi-random overall (a) Average number of fresh variables introduced for each problem during transformation application pattern random semi-random (b) Average number of SNF clauses for each problem overall application
pattern random semi-random (c) Average size of SNF for each problem overall ltl2snf ltl2snf -isnf -simp ltl2snf -isnf -ple -simp ltl2snf -aprenex -isnf -ple -simp translate translate -r -s application pattern random semi-random overall (d) Average time for transformation of each problem (in CPU seconds)
Overall, the combination of -isnf, -simp, and -ple o ers the best result.
The option -isnf o er the greatest improvement on the semi-random category,
as half its formulae are already in normal form. The option -ple, pure literal
elimination, shows the greatest improvements on the pattern and random
categories. For the pattern category this is the case because most formulae only
contain positive propositional literals. It seems to have been overlooked in their
construction that the formulae consequently have trivial models. For the random
category, again a lot of them contain pure literals as an artefact of the particular
way they were randomly generated. On the other hand, on the application and
semi-random categories, pure literal elimination has almost no e ect. For the
application category, one can take this as an indication that in the formalisation
of `real world' applications, pure literals are rare. For the semi-random category,
the lack of pure literals is an artefact of their construction. Option -aprenex,
anti-prenexing, appears to have a detrimental e ect. This is in contrast to the
results in [
Regarding the time it takes to compute the normal form, we can see in Figure 6(d) that ltl2snf typically takes less than 1ms to compute the SNF of a formula, independent of the pre-processing techniques that are applied. In contrast, for translate the use of simpli cation increases the computation time dramatically, in particular, for the application category where it increases from an average of 0.01 CPU seconds to 12.61 CPU seconds. Also remember that we have already excluded over 1300 formulae for which translate does not complete the transformation within 1000 CPU seconds, in particular, it does not do so with simpli cation enabled. One possible explanation for the gap between the time spent by translate and that spent by ltl2snf is that the former does not atten conjunctions and disjunctions, but a polynomial, thus non-optimal, sorting algorithm is applied to conjuncts and disjuncts before applying simpli cation.
We have also started to evaluate how the provers LS4 and TRP++ perform on the various sets of SNF clauses that ltl2snf can produce for each of the benchmark formulae. Initial results suggest that at least on average, the smallest normal form indeed leads to the best performance by the two provers. 5
Overall, the results show that the application of pre-processing techniques
signi cantly reduced the size of the normal form and that, if implemented well, as
in ltl2snf, this application comes at negligible computational cost. We are
currently implementing the prenex transformations given in Figure 4 and di erent
techniques for renaming in order to reduce further the size of the generated set
of clauses. Finally, although 'small' normal forms seem to be a good measure for
determining the quality of the translation into the normal form, we are planning
for a more systematic evaluation of the impact they have in the e ciency of
the provers. As part of our investigation, we are planning to implement di erent
variants of the separated normal form, for instance a variant introduced in [