Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics? Ullrich Hustadt1 , Cláudia Nalon2 , and Clare Dixon1 1 Department of Computer Science, University of Liverpool Liverpool, L69 3BX – United Kingdom U.Hustadt, CLDixon@liverpool.ac.uk 2 Department of Computer Science, University of Brası́lia C.P. 4466 – CEP:70.910-090 – Brası́lia – DF – Brazil nalon@unb.br Abstract We consider the transformation of propositional linear time temporal logic formulae into a clause normal form, called Separated Nor- mal Form, suitable for resolution calculi. In particular, we investigate the effect 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. 1 Introduction Clause normal forms are the foundation of most resolution-based calculi and such calculi exist for a wide range of logics, including propositional, first-order, modal and temporal logics. Given a formula ϕ, the clause normal form of ϕ is typically computed using a combination of equivalence or satisfiability pre- serving rewrite steps, including simplification as a special case, and renaming, which replaces complex subformulae by new propositional variables and adds definitional clauses for the new propositional variables. Variations in the normal form can greatly influence 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 first-order logic the computation of such ‘small’ clause normal forms is well- studied [16,1,18]. However, the problem has been not been investigated to the same extent for non-classical logics, one exception being the work by Nalon and Dixon on prenexing versus anti-prenexing for modal logics [14]. 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 [6]. More recently, a decision procedure for PLTL using la- belled superposition has also used SNF as a starting point [22]. There are sev- eral theorem provers for PLTL that use SNF as their input language, including TRP [9], TRP++ [10,11] and LS4 [22,21]. In following we revisit the problem of computing the SNF of a given PLTL formula. In particular, we determine the effect of applying various pre-processing techniques during the computation. The paper is organised as follows. We present the language of PLTL in Sec- tion 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 The Language of PLTL We consider a particular variety of temporal logic, which is based on a linear, discrete model of time with finite past and infinite future [7,13]. This logic can be seen as a multi-modal language with two modalities, one to represent the ‘next’ moment in time, the other representing all future moments in time. 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 definition of the logic, as in [4], but such operators add no extra expressive power [7]. Formulae are constructed from a denumerable set P = {p, q, p0 , q 0 , p1 , q1 , . . .} 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 defined as the smallest set satisfying: – the propositional variables are in WFFPLTL ; – > and ⊥ are in WFFPLTL ; – if ϕ and ψ are in WFFPLTL , then so are ¬ϕ, (ϕ → ψ), (ϕ ↔ ψ), 3 ϕ, 2 ϕ, # ϕ, (ϕ U ψ), (ϕ W ψ); – if ϕ1 , . . . , ϕn , n ≥ 1, are in WFFPLTL , then so are (ϕ1 ∧ · · · ∧ ϕn ) and (ϕ1 ∨ · · · ∨ ϕn ). 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 defined as follows: 3 We consider the connectives that reflect 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. 35 – the empty word  ∈ pos(ϕ); – if ϕ is of the form ¬ϕ1 , # ϕ1 , 2 ϕ1 , or 3 ϕ1 for some formula ϕ1 and π ∈ pos(ϕ1 ) then 1.π ∈ pos(ϕ); – if ϕ is of the form (ϕ1 → ϕ2 ), (ϕ1 ↔ ϕ2 ), (ϕ1 U ϕ2 ), or (ϕ1 W ϕ2 ) and π ∈ pos(ϕi ) for i ∈ {1, 2}, then i.π ∈ pos(ϕ); and – if ϕ is of the form (ϕ1 ∧ · · · ∧ ϕn ) or (ϕ1 ∨ · · · ∨ ϕn ) and π ∈ pos(ϕi ) for i ∈ {1, . . . , n}, then i.π ∈ pos(ϕ). For a formula ϕ and position π ∈ pos(ϕ), we define the subformula ϕ|π of ϕ at position π as follows: – ϕ| = ϕ; – if ϕ is of the form ¬ϕ1 , # ϕ1 , 2 ϕ1 , or 3 ϕ1 for some formula ϕ1 and π = 1.τ , then ϕ|π = ϕ1 |τ ; – if ϕ is of the form (ϕ1 → ϕ2 ), (ϕ1 ↔ ϕ2 ), (ϕ1 U ϕ2 ), or (ϕ1 W ϕ1 ) and π = i.τ for i ∈ {1, 2}, then ϕ|π = ϕi |τ ; and – if ϕ is of the form (ϕ1 ∧· · ·∧ϕn ) or (ϕ1 ∨· · ·∨ϕn ) and π = i.τ for i ∈ {1, . . . , n}, then ϕ|π = ϕi |τ . The polarity pol(ϕ, π) of a subformula occurring at position π in a formula ϕ is defined as follows: – pol(ϕ, ) = 1; – if π = τ.1 and ϕ|τ is of the form # ϕ1 , 2 ϕ1 , or 3 ϕ1 , then pol(ϕ, π) = pol(ϕ, τ ); – if π = τ.1 and ϕ|τ is of the form ¬ϕ1 or (ϕ1 → ϕ2 ), then pol(ϕ, π) = − pol(ϕ, τ ); – if π = τ.2 and ϕ|τ is of the form (ϕ1 → ϕ2 ), then pol(ϕ, π) = pol(ϕ, τ ); – if π = τ.i with i ∈ {1, 2} and ϕ|τ is of the form (ϕ1 U ϕ2 ) or (ϕ1 W ϕ2 ) then pol(ϕ, π) = pol(ϕ, τ ); – if π = τ.i with i ∈ {1, . . . , n} and ϕ|τ is of the form (ϕ1 ∧ · · · ∧ ϕn ) or (ϕ1 ∧ · · · ∧ ϕn ), then pol(ϕ, π) = pol(ϕ, τ ); – if π = τ.i with i ∈ {1, 2} and ϕ|τ 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 infinite sequences of states σ = (si )i∈N such that each si , 0 ≤ i, is a set of propositional variables. The notation (σ, i) |= ϕ denotes the truth of a formula ϕ in the model σ at the state index i, i ∈ N. For any formula ϕ, model σ, and state index i, i ∈ N, then either (σ, i) |= ϕ holds or (σ, i) |= ϕ does not hold, where the latter is denoted by (σ, i) 6|= ϕ. The semantics of WFFPLTL can now be given as follows: Definition 1. Let ϕ and ψ be formulae in WFFPLTL , σ a model, and i ∈ N the index of a state in σ. – (σ, i) |= > 36 – (σ, i) 6|= ⊥ – (σ, i) |= p if, and only if, p ∈ si , where p ∈ P – (σ, i) |= ¬ϕ if, and only if, (σ, i) 6|= ϕ – (σ, i) |= (ϕ1 ∧ · · · ∧ ϕn ) if, and only if, for every i, 1 ≤ i ≤ n, (σ, i) |= ϕ – (σ, i) |= (ϕ1 ∨ · · · ∨ ϕn ) if, and only if, for some i, 1 ≤ i ≤ n, (σ, i) |= ϕi – (σ, i) |= (ϕ → ψ) if, and only if, (σ, i) |= ¬ϕ or (σ, i) |= ψ – (σ, i) |= (ϕ ↔ ψ) if, and only if, (σ, i) |= (ϕ → ψ) and (σ, i) |= (ψ → ϕ) – (σ, i) |= # ϕ if, and only if, (σ, i + 1) |= ϕ – (σ, i) |= 3 ϕ if, and only if, ∃k, k ∈ N, k ≥ i, (σ, k) |= ϕ – (σ, i) |= 2 ϕ if, and only if, ∀k, k ∈ N, if k ≥ i, then (σ, k) |= ϕ – (σ, i) |= (ϕ U ψ) if, and only if, ∃k, k ∈ N, k ≥ i, (σ, k) |= ψ and ∀j, j ∈ N, if i ≤ j < k, then (σ, j) |= ϕ. – (σ, i) |= (ϕ W ψ) if, and only if, either (σ, i) |= ϕ U ψ or (σ, i) |= 2 ϕ. A formula ϕ is satisfiable if there is a model σ such that (σ, 0) |= ϕ. If (σ, 0) |= ϕ for all models σ, then ϕ is said to be valid, denoted by |= ϕ. Two PLTL-formulae ϕ and ψ are equi-satisfiable if, and only if, ϕ is satisfiable if, and only if, ψ is satisfiable. Two PLTL-formulae ϕ and ψ are equivalent if, and only if, for every model σ and every state index i, i ∈ N, (σ, i) |= ϕ if and only if (σ, i) |= ψ 3 Normal Form Formulae in the language of PLTL can be transformed into a normal form called Separated Normal Form (SNF) [5]. This normal form was inspired by (but it is independent of) Gabbay’s separation result [8], which states that temporal formulae can be transformed into their past, present and future-time compon- ents. In the version of SNF that we present here, formulae are represented by a conjunction of clauses, ^ Ci 1≤i≤n where each clause Ci , 1 ≤ i ≤ n, n ∈ N, is in one of the following three forms. m _ li (initial clause) i=1 _m n _ 2( li ∨ # lj0 ) (global clause) i=1 j=1 _m 2( li ∨ 3 l10 ) (eventuality clause) i=1 where n, m ≥ 0 and for every i, 1 ≤ i ≤ m, and j, 1 ≤ j ≤ n, li and lj0 are literals. 37 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-satisfiable formula in SNF. Fisher, Dixon and Peim [6] describe functions τ0 and τ1 with τ0 (ϕ) = (q1 ∧τ1 (2(¬q1 ∨ϕ))), where q1 is a fresh propositional variable not occurring in ϕ, such that τ0 (ϕ) is in SNF and equi-satisfiable to ϕ. The function τ1 proceeds top- down and uses renaming to deal with subformulae that are not yet in normal form [17]. The inductive definition of τ1 is shown in Figure 1, where ϕ, ϕi , 0 ≤ i ≤ n, and ψ are PLTL-formulae, l, l1 , l2 are literals, q is a propositional variable, and q 0 , q 00 , and q 000 are fresh propositional variables. Theorems 7.1.1 and 7.1.2 in [6] show that the computation of τ0 (ϕ) always terminates, that the number of SNF clauses in τ0 (ϕ) is bounded by 1 + 4 × size(ϕ), and that the number of fresh propositional variables in τ0 (ϕ) is bounded by 1 + 11 × size(ϕ), where size(ϕ) is the size of ϕ. 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 Equa- tion (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 five clauses. This could be avoided by simplification 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 tem- poral 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 dis- cuss the anti-prenexing technique. In first-order logic, it has been shown [3] that the transformation of a given problem into anti-prenex normal form may result in a better set of clauses. Similar results for normal modal logics which allow the simplification of nested operators can be found in [14]. For temporal logics, anti- prenexing together with simplification may help reducing the size of a formula and, consequently, the size of the normal form. For instance, the anti-prenex normal form of ϕ3 = 2(p ∧ 2(p ∧ 2 p)) is 2p ∧ 22p ∧ 222p 38 τ1 (2(¬q ∨ (ϕ1 ∧ · · · ∧ ϕn ))) = τ1 (2(¬q ∨ ϕ1 )) ∧ · · · ∧ τ1 (2(¬q ∨ ϕn )) (1) τ1 (2(¬q ∨ ¬(ϕ1 ∧ · · · ∧ ϕn ))) = τ1 (2(¬q ∨ ¬ϕ1 ∨ · · · ∨ ¬ϕn )) (2) τ1 (2(¬q ∨ ϕ1 ∨ · · · ∨ ϕn )) = 2(¬q ∨ ϕ1 ∨ · · · ∨ q 0 ∨ · · · ∨ ϕn ) ∧ 2(¬q 0 ∨ ϕi ) (3) if ϕi , 1 ≤ i ≤ n, is not an elementary formula τ1 (2(¬q ∨ ϕ ∨ #(ϕ1 ∨ · · · ∨ ϕn ))) = τ1 (2(¬q ∨ ϕ ∨ # ϕ1 ∨ · · · ∨ # ϕn )) (4) 0 0 τ1 (2(¬q ∨ ϕ ∨ # ψ)) = τ1 (2(¬q ∨ ϕ ∨ # q )) ∧ τ1 (2(¬q ∨ ψ)) (5) if ψ is not a disjunction of literals τ1 (2(¬q ∨ (ϕ → ψ))) = τ1 (2(¬q ∨ ¬ϕ ∨ ψ)) (6) τ1 (2(¬q ∨ ¬(ϕ → ψ))) = τ1 (2(¬q ∨ ϕ)) ∧ τ1 (2(¬q ∨ ¬ψ)) (7) τ1 (2(¬q ∨ ¬ # ϕ)) = τ1 (2(¬q ∨ # q 0 )) ∧ τ1 (2(¬q 0 ∨ ¬ϕ)) (8) τ1 (2(¬q ∨ 2 ϕ)) = τ1 (2(¬q ∨ 2 q 0 )) ∧ τ1 (2(¬q 0 ∨ ϕ)) (9) if ϕ is neither a literal nor a constant τ1 (2(¬q ∨ 2 l)) = 2(¬q ∨ l) ∧ 2(¬q ∨ q 0 ) (10) ∧ 2(¬q 0 ∨ # l) ∧ 2(¬q 0 ∨ # q 0 ) τ1 (2(¬q ∨ ¬ 2 ϕ)) = τ1 (2(¬q ∨ 3 ¬ϕ)) (11) 0 0 τ1 (2(¬q ∨ 3 ϕ)) = τ1 (2(¬q ∨ 3 q )) ∧ τ1 (2(¬q ∨ ϕ)) (12) if ϕ is neither a literal nor a constant τ1 (2(¬q ∨ ¬ 3 ϕ)) = τ1 (2(¬q ∨ 2 ¬ϕ)) (13) τ1 (2(¬q ∨ (ϕ U ψ))) = τ1 (2(¬q ∨ (q 0 U ψ))) ∧ τ1 (2(¬q 0 ∨ ϕ)) (14) if ϕ is neither a literal nor a constant τ1 (2(¬q ∨ (ϕ U ψ))) = τ1 (2(¬q ∨ (ϕ U q 0 ))) ∧ τ1 (2(¬q 0 ∨ ψ)) (15) if ψ is neither a literal nor a constant τ1 (2(¬q ∨ (l1 U l2 ))) = 2(¬q ∨ 3 l2 ) ∧ 2(¬q ∨ l1 ∨ l2 ) (16) ∧ 2(¬q ∨ q 0 ∨ l2 ) ∧ 2(¬q 0 ∨ # l1 ∨ # l2 ) ∧ 2(¬q 0 ∨ # q 0 ∨ # l2 ) τ1 (2(¬q ∨ ¬(ϕ U ψ))) = τ1 (2(¬q ∨ (q 0 W q 00 ))) (17) ∧ 2(¬q 00 ∨ q 0 ) ∧ 2(¬q 00 ∨ q 000 ) ∧τ1 (2(¬q 0 ∨ ¬ψ)) ∧ τ1 (2(¬q 000 ∨ ¬ϕ)) τ1 (2(¬q ∨ (ϕ W ψ))) = τ1 (2(¬q ∨ (q 0 W ψ))) ∧ τ1 (2(¬q 0 ∨ ϕ)) (18) if ϕ is neither a literal nor a constant τ1 (2(¬q ∨ (ϕ W ψ))) = τ1 (2(¬q ∨ (ϕ W q 0 ))) ∧ τ1 (2(¬q 0 ∨ ψ)) (19) if ψ is neither a literal nor a constant τ1 (2(¬q ∨ (l1 W l2 ))) = 2(¬q ∨ l1 ∨ l2 ) ∧ 2(¬q ∨ q 0 ∨ l2 ) (20) ∧ 2(¬q 0 ∨ # l1 ∨ # l2 ) ∧ 2(¬q 0 ∨ # q 0 ∨ # l2 ) τ1 (2(¬q ∨ ¬(ϕ W ψ))) = τ1 (2(¬q ∨ (q 0 U q 00 ))) (21) ∧ 2(¬q 00 ∨ q 0 ) ∧ 2(¬q 00 ∨ q 000 ) ∧ τ1 (2(¬q 0 ∨ ¬ψ)) ∧ τ1 (2(¬q 000 ∨ ¬ϕ)) τ1 (ϕ) = ϕ, if no other rule applies (22) Figure 1. Definition of Transformation Function τ1 39 nnf(¬ # ϕ) = # nnf(¬ϕ) (23) nnf(¬(ϕ U ψ)) = (nnf(¬ψ) W nnf(¬ϕ ∧ ¬ψ)) (29) nnf(¬ 2 ϕ) = 3 nnf(¬ϕ) (24) nnf(¬(ϕ W ψ)) = (nnf(¬ψ) U nnf(¬ϕ ∧ ¬ψ)) (30) nnf(¬ 3 ϕ) = 2 nnf(¬ϕ) (25) nnf((ϕ U ψ) = (nnf(ϕ) U nnf(ψ)) (31) nnf(# ϕ) = # nnf(ϕ) (26) nnf((ϕ W ψ) = (nnf(ϕ) W nnf(ψ)) (32) nnf(3 ϕ) = 3 nnf(ϕ) (27) nnf(2 ϕ) = 2 nnf(ϕ) (28) Figure 2. Definition of the Negation Normal Form for Temporal Formulae #> ↔ > (33) 3(ϕ U ψ) ↔ 3 ψ (43) (ϕ W ϕ) ↔ ϕ (52) #⊥ ↔ ⊥ (34) 2(ϕ W ψ) ↔ 2(ϕ ∨ ψ) (44) (ϕ U >) ↔ > (53) 3⊥ ↔ ⊥ (35) (ϕ U 3 ψ) ↔ 3 ψ (45) (ϕ U ⊥) ↔ ⊥ (54) 3> ↔ > (36) (ϕ U ¬ϕ) ↔ 3 ¬ϕ (46) (> U ϕ) ↔ 3 ϕ (55) 2⊥ ↔ ⊥ (37) (¬ϕ U ϕ) ↔ 3 ϕ (47) (⊥ U ϕ) ↔ ϕ (56) 2> ↔ > (38) (ϕ U ϕ) ↔ ϕ (48) (ϕ W >) ↔ > (57) 33ϕ ↔ 3ϕ (39) (2 ϕ W ψ) ↔ (2 ϕ ∨ ψ) (49) (ϕ W ⊥) ↔ 2 ϕ (58) 22ϕ ↔ 2ϕ (40) (ϕ W ¬ϕ) ↔ > (50) (> W ϕ) ↔ > (59) 3 2 3 ϕ ↔ 2 3 ϕ (41) (¬ϕ W ϕ) ↔ > (51) (⊥ W ϕ) ↔ ϕ (60) 2 3 2 ϕ ↔ 3 2 ϕ (42) Figure 3. Temporal Equivalences for Simplification As 2 2 ψ is equivalent to 2 ψ, for any formula ψ, after simplification, 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 equi- valences 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 simplified to 2 # # # p. Since τ1 only preserves satisfiability, 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 specific propositional variable q1 used by τ0 . The next lemma 40 #(ϕ1 ∨ · · · ∨ ϕn ) ↔ (# ϕ1 ∨ · · · ∨ # ϕn ) (61) 3(ϕ1 ∨ · · · ∨ ϕn ) ↔ (3 ϕ1 ∨ · · · ∨ 3 ϕn ) (62) #(ϕ1 ∧ · · · ∧ ϕn ) ↔ (# ϕ1 ∧ · · · ∧ # ϕn ) (63) 2(ϕ1 ∧ · · · ∧ ϕn ) ↔ (2 ϕ1 ∧ · · · ∧ 2 ϕn ) (64) #2ϕ ↔ 2#ϕ (65) #3ϕ ↔ 3#ϕ (66) #(ϕ U ψ) ↔ ((# ϕ) U (# ψ)) (67) #(ϕ W ψ) ↔ ((# ϕ) W (# ψ)) (68) ((ϕ ∧ ψ) U ϑ) ↔ ((ϕ U ϑ) ∧ (ψ U ϑ)) (69) (ϕ U (ψ ∨ ϑ)) ↔ ((ϕ U ψ) ∨ (ϕ U ϑ)) (70) ((ϕ ∧ ψ) W ϑ) ↔ ((ϕ W ϑ) ∧ (ψ U ϑ)) (71) (ϕ W (ψ ∨ ϑ)) ↔ ((ϕ W ψ) ∨ (ϕ W ϑ)) (72) Figure 4. Temporal Equivalences for Prenexing and Anti-Prenexing shows that this simplification step in the transformation is correct, that is, that satisfiability is preserved. Lemma 1. Let ϕ be a PLTL-formula and q1 a propositional variable not occur- ring in ϕ. Then, 2 ϕ is satisfiable if, and only if, q1 ∧ τ1 (2 ϕ) is satisfiable. Proof. (⇒) By the results in [6], 2 ϕ is satisfiable if, and only if, q1 ∧ 2(¬q1 ∨ τ1 (2 ϕ)) is satisfiable. From the definition of satisfiability, there is a model σ such that (σ, 0) |= q1 ∧ 2(¬q1 ∨ τ1 (2 ϕ)). It follows that (1) (σ, 0) |= q1 and (σ, 0) |= 2(¬q1 ∨ τ1 (2 ϕ)). From the definition of satisfiability of the temporal operator 2, for all i, i ∈ N, we have that (σ, i) |= ¬q1 ∨ τ1 (2 ϕ). In particular, (σ, 0) |= ¬q1 ∨ τ1 (2 ϕ). As (σ, 0) |= q1 , it follows from the definition of satisfiability of disjunctions that (2) (σ, 0) |= τ1 (2 ϕ). From (1) and (2), q1 ∧τ1 (2 ϕ) is satisfiable. (⇐) If q1 ∧ τ1 (2 ϕ) is satisfiable, then there is a model σ such that (σ, 0) |= q1 ∧ τ1 (2 ϕ). We construct a model σ 0 such that s00 = s0 ∪ {q1 } and, for all i > 0, s0i = si \ {q1 }. It follows, by construction, that (3) (σ 0 , 0) |= q1 . As (σ, 0) |= τ1 (2 ϕ) and the evaluation of τ1 (2 ϕ) does not depend on the evaluation of q1 , we have that (σ 0 , 0) |= τ1 (2 ϕ) and, from the definition of satisfiability of disjunctions, (4) (σ 0 , 0) |= ¬q1 ∨ τ1 (2 ϕ). Also, by construction, for all i > 0, (σ 0 , i) |= ¬q1 . Thus, for all i, i ∈ N, (5) (σ 0 , i) |= ¬q1 ∨ τ1 (2 ϕ). From (4) and (5), it follows that, for all i ≥ 0, (σ 0 , i) |= ¬q1 ∨ τ1 (2 ϕ). From the definition of satisfiability of the 2 operator, we obtain that (6) (σ 0 , 0) |= 2(¬q1 ∨ τ1 (2 ϕ)). From (3) and (6), we have that (σ 0 , 0) |= q1 ∧ 2(¬q1 ∨ τ1 (2 ϕ)). By the results in [6], 2 ϕ is satisfiable. 41 1 Algorithm: ltl2snf(ϕ) 2 repeat 3 hnumsimp, ϕi ← input simplification(ϕ); 4 until (numsimp = 0); 5 ϕ ← nnf transformation(ϕ); 6 repeat 7 hϕ, numaprenexi ← aprenex transformation(ϕ); 8 hnumsimp, ϕi ← input simplification(ϕ); 9 until (numsimp = 0 and numaprenex = 0); 10 return snf transformation(ϕ); Figure 5. Main Loop 4 Implementation and Evaluation 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++ [10] and LS4 [22,21]. The source code of ltl2snf, together with installation and usage instructions, is available in [15]. 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 simplified 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 simplification is performed. In particular, clause subsumption or variable elimination techniques such as those described in [10,20] are not applied. We consider this to be a task for theorem provers that take SNF clauses as input. 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 simplification. 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 modified version of τ1 , which is implemented as part of the transformation into the normal form (snf transformation). 42 Both the simplification procedure and the transformation into anti-prenex nor- mal form are performed until a fixed-point is reached, that is, no further trans- formation/simplification is possible. We also note that simplification and pure literal elimination are performed before the transformation into Negation Nor- mal 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 struc- ture, the result of the translation into NNF is exponential in the size of the ori- ginal formula. Applying pure literal elimination together with constant propaga- tion to the original formula avoids this problem. For this particular example, the resulting formula is >. To evaluate the effectiveness of each technique and their combinations we have used a set of PLTL-formulae collected by Schuppan and Darwiche [19]. The collection consists of 7450 formulae, half of these are taken from the literature or previous collections of benchmark formulae, the other half is obtained by negating these formulae. Since we also compared ltl2snf with an earlier im- plementation of the SNF transformation in the tool translate [12], we have only 6135 of these formulae, on the remaining formulae, translate does not produce a normal form within a time limit of 1000 CPU seconds. The collection is divided into seven classes: acacia, alaska, anzu, forobots, rozier, schuppan, trp. Most classes consist of several families of formulae, sometimes with quite different characteristics (for a detailed description of each class and each family see [19]). We have therefore re-categorised the formulae as follows: – application category: consists of the formulae in the classes acacia, alaska, anzu, and forobots, all of which relate to ‘real world’ applications, as well as the counter family of the rozier class, containing formulae that specify serial counters, and the phltl family of the schuppan class, containing formulae that specify temporalised instances of the pigeon hole problem; – pattern category: consists of the pattern family of the rozier class and the O1formula and O2formula families of the schuppan class; these are series of scalable temporal formulae that follow simple patterns; – random category: consists of the formulas family of the rozier class, containing random temporal formulae; – semi-random category: consists of the trp class, containing formulae that each follow a pattern but also have a random part. Half of the formulae in this category (the unnegated formulae) are already in SNF. Table 1 shows syntactic properties of these categories. The random category con- tains more formulae than all other categories combined. However, the combined size of its formulae is smaller than that of the application and semi-random 43 #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 Table 1. Properties of the benchmark formulae 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 significantly 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 oc- currences in each formula. Besides considering the effect of various pre-processing techniques implemen- ted in ltl2snf on the normal form, we have also compared ltl2snf with the latest version of translate [12], an earlier implementation of the transformation of PLTL to SNF. translate which is written in OCaml, implements the same set of simplification rules used by ltl2snf, the main differences being that conjunc- tions and disjunctions are taken as binary operators and that some prenexing is also applied (specifically, Equations (61) to (64), (67) and (68) in Figure 4). The option -s activates simplification. With the option -r, during the normal form transformation translate will replace (ϕ ∨ ψ) by (p ∨ ψ) together with the definition 2(¬p ∨ ϕ), if both ϕ and ψ are temporal formulae. This is assumed to result in a smaller normal form in most cases, although it not always does. Figure 6 shows for particular combinations of ltl2snf and translate op- tions 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 effect. 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 [6]. Instead of four times the number of clauses and eleven times the number fresh variables in the size of formulae, even without any pre-processing we see that on everage we get a number of clauses linear in the size of a formulae and a number of fresh propositional variables at half the size of a formula. With pre-processing both can further be reduced by half. 44 200 100 0 application pattern random semi-random overall (a) Average number of fresh variables introduced for each problem during transform- ation 400 200 0 application pattern random semi-random overall (b) Average number of SNF clauses for each problem 3,000 2,000 1,000 0 application pattern random semi-random overall (c) Average size of SNF for each problem ltl2snf 10 ltl2snf -isnf -simp ltl2snf -isnf -ple -simp ltl2snf -aprenex -isnf -ple -simp 5 translate translate -r -s 0 application pattern random semi-random overall (d) Average time for transformation of each problem (in CPU seconds) Figure 6. Evaluation of ltl2snf and translate 45 Overall, the combination of -isnf, -simp, and -ple offers the best result. The option -isnf offer 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 cat- egories. 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 effect. 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 effect. This is in contrast to the results in [14] for basic modal logic, where anti-prenexing was found to be bene- ficial. This indicates that the assumption that anti-prenexing leads to chains of temporal operators that can be collapsed, is not true for any of the benchmark categories. 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 simplification 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 simplification enabled. One possible explanation for the gap between the time spent by translate and that spent by ltl2snf is that the former does not flatten conjunctions and disjunctions, but a polynomial, thus non-optimal, sorting algorithm is applied to conjuncts and disjuncts before applying simplification. 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 Conclusion Overall, the results show that the application of pre-processing techniques sig- nificantly reduced the size of the normal form and that, if implemented well, as in ltl2snf, this application comes at negligible computational cost. We are cur- rently implementing the prenex transformations given in Figure 4 and different 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 46 for a more systematic evaluation of the impact they have in the efficiency of the provers. As part of our investigation, we are planning to implement different variants of the separated normal form, for instance a variant introduced in [2] where only a single eventuality clause is allowed. While this leads to a bigger normal form when we need to reduce several eventualities in the input to just one, proof search by existing PLTL decision procedures may become easier and therefore result in better overall performance. References 1. Azmy, N., Weidenbach, C.: Computing tiny clause normal forms. In: Proc. CADE- 24. Lecture Notes in Computer Science, vol. 7898, pp. 109–125. Springer (2013) 2. Degtyarev, A., Fisher, M., Konev, B.: A simplified clausal resolution procedure for propositional linear-time temporal logic. In: Proc. TABLEAUX 2002. Lecture Notes in Computer Science, vol. 2381, pp. 85–99. Springer (2002) 3. Egly, U.: On the value of antiprenexing. In: Proc. LPAR 1994. Lecture Notes in Artificial Intelligence, vol. 822, pp. 69–83. Springer (1994) 4. Fisher, M.: A Resolution Method for Temporal Logic. In: Proc. IJCAI 1991. pp. 99–104. Morgan Kaufman (1991) 5. Fisher, M.: A Normal Form for Temporal Logic and its Application in Theorem- Proving and Execution. Journal of Logic and Computation 7(4), 429–456 (Aug 1997) 6. Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic 2(1), 12–56 (2001) 7. Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: The Temporal Analysis of Fairness. In: Proc. POPL 1980. pp. 163–173. ACM (1980) 8. Gabbay, D.M.: Declarative Past and Imperative Future: Executable Temporal Lo- gic for Interactive Systems. In: Proc. Colloquium on Temporal Logic in Specifica- tion. Lecture Notes in Computer Science, vol. 398, pp. 402–450. Springer (1987) 9. Hustadt, U.: TRP 1.4 [online] (2008), http://cgi.csc.liv.ac.uk/~ullrich/TRP/ 10. Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Baaz, M., Makowsky, J., Voronkov, A. (eds.) Collegium Logicum, pp. 65–79. Kurt Gödel So- ciety (2004), http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf 11. Konev, B.: TRP++ 2.2 [online] (2011), http://cgi.csc.liv.ac.uk/~konev/ software/trp++/ 12. Konev, B.: Translate [online] (2016), http://cgi.csc.liv.ac.uk/~konev/ software/trp++/translator/ 13. Lichtenstein, O., Pnueli, A., Zuck, L.: The Glory of the Past. In: Proc. Logics of Programs 1985, Lecture Notes in Computer Science, vol. 193, pp. 196–218. Springer (1985) 14. Nalon, C., Dixon, C.: Anti-prenexing and prenexing for modal logics. In: Proc. JELIA 2006. Lecture Notes in Computer Science, vol. 4160, pp. 333–345. Springer (2006) 15. Nalon, C., Hustadt, U., Dixon, C.: ltl2snf: a translator for LTL formulae into SNF clauses [online] (2018), http://www.cic.unb.br/~nalon/software/ltl2snf-0.1. 0.tar.gz 16. Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robin- son, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 6, pp. 335– 367. Elsevier (2001) 47 17. Plaisted, D.A., Greenbaum, S.A.: A Structure-Preserving Clause Form Transla- tion. Journal of Logic and Computation 2, 293–304 (1986) 18. Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: Proc. GCAI 2016. EPiC Series in Computing, vol. 41, pp. 11–23. EasyChair (2016) 19. Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Proc. ATVA 2011. Lecture Notes in Computer Science, vol. 6996, pp. 397–413. Springer (2011) 20. Suda, M.: Variable and clause elimination for LTL satisfiability checking. Math- ematics in Computer Science 9(3), 327–344 (2015) 21. Suda, M.: LS4 [online] (2018), https://github.com/quickbeam123/ls4 22. Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Proc. IJCAR 2012. pp. 537–543. Springer (2012) 48