# Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications

Authors: Salamah Salamah; Ann Q. Gates; Steve Roach; Matthew  Engskow
Journal: Advances in Software Engineering
 (2011)

---

## Abstract

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work
presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Büchi automaton generated for the formula. Minimizing the size of the Büchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.


---

## Body

## 1. Introduction

The process of model checking a system consists of developing a model of the system to be verified and writing specifications in a temporal logic such as Linear Temporal Logic (LTL) [1] or Computational Tree Logic (CTL) [2]. In automata-based model checking, both the model M and the complement of the temporal specification S are represented by a special type of state machine called a Büchi Automaton (BA) [3]. To check the consistency of M with S, the model checker calculates the intersection of M and S′ where S′ is the complement of S. If the intersection is empty, then M is consistent with S. In other words, if M and S′ each represent a set of specifications and if M∩S′=∅, then the system satisfies the specification; otherwise, the system is inconsistent with the specification and a counter-example is returned.The process of writing formal specifications is not easy because of the required mathematical sophistication and depth of knowledge in the specification language. For this reason, tools that simplify the creation of formal specifications in logics such as LTL are of interest to the model checking community and others. In the case of automata-based model checkers such as Spin [4], it is important that these tools generate efficient formulas, since the model checker complements the formulas, translates the result into a BA, and intersects the BA with the automaton of the system. The size of the automaton that results from the intersection of two automata has as its upper bound the product of the number of states in each of the two. One way to avoid the classical problem of state space explosion is to minimize the number of states generated by the negation of the specification. This will reduce the number of states generated by the automaton of the intersection, and as a result, it will reduce the time required to model check a software system.The Property Specification (Prospec) [5–7] builds on the Property Specification Patterns system (SPS) [8, 9], and it uses property pattern and scope to assist in the specification of formal properties in LTL as well as other languages. Patterns are high-level abstractions that provide descriptions of common properties, and scopes describe the extent of program execution over which the property holds. Prospec also introduces the notion of composite propositions to allow for the definition of more complex behavior to represent the behaviors for patterns and scopes.This paper introduces more efficient LTL formulas for patterns and scopes than those originally generated by Prospec. In defining the new formulas, we tried to limit the number of temporal operators in a formula because we believe this reduces the number of states in the never-claim. The formulas are compared in terms of the number of states in the never-claim generated by the negation of these formulas since it is actually the complement of a formula that the model checker uses. To generate Büchi automata, we used the model checker SPIN, and the LTL to BA translators: LTL2BA [10], the Temporal Message Parlor [11], and LTL2NBA [12], all of which efficiently convert LTL specifications into BAs. Notice that some of these tools produce a BA in the form of a never-claim, which is a specific representation of BA used by the model checker Spin. In this article we use the terms Büchi automata and never-claims interchangeably. This paper also shows an approach for proving the equivalence of different LTL formulas. Finally, this paper describes the impact that more efficient formulas have when using composite propositions [6] to define pattern and scope limits.The paper first presents a background on LTL and Büchi automata (BA), including the semantics of the languages. The Prospec tool is introduced in Section3. Section 4 describes the new formulas and the process used to verify the semantic equivalence of the two sets of formulas. Section 4 also provides the results of the comparisons of the formulas. Finally, the impact of the work on composite propositions is presented in Section 5 followed by brief discussion and references.


## 2. Background

### 2.1. Linear Temporal Logic

This section briefly describes Linear Temporal Logic (LTL) and its semantics. A more detailed description of LTL can be found in Manna [13].Temporal Logic has been used to verify concurrent systems. There are three well used types of temporal Logic: Linear Temporal Logic (LTL), Computational Tree Logic (CTL), and CTL* [3]. Both LTL and CTL are subsets of CTL*. While CTL allows for branching type of behavior (i.e., semantically, formulas are defined both using the universal and existential quantifiers), LTL formulas describe specific path behavior (i.e., semantically, formulas are defined only using the universal quantifier). Formulas in this paper deal only with LTL.LTL is used in various model checkers such as SPIN [4], NUSMV [14], and Java Path-Finder [15] and is also used in runtime verification of Java programs [16].In LTL, a temporal formula is constructed inductively from a set of propositionsP by applying Boolean connectives ¬ and ∨ and temporal operators next (X) and until (U) as follows.  (i)
A proposition is a temporal formula.(ii)
Ifp and q are temporal formulas, then the followings are also temporal formulas:
(i)
¬p,(ii)
p∨q,(iii)
Xp,(iv)
pUq.A temporal formula that makes use only of Boolean connectives¬ and ∨ is called a state formula, whereas a formula that makes use of temporal operators X and U is called a temporal formula.LetP be a set of propositions; let σ be an infinite sequence of states or computation, denoted by σ: s0,s1,…, let ∑ be a set of states; let I(s) be an interpretation such that for all s∈∑, I(s)⊆P specifies the propositions that are true in state s. For a state formula, the satisfaction relation ⊨ is defined as follows: for a state s∈∑ and a proposition p in P, s satisfies p, denoted s⊨p, if and only if p∈I(s). In addition, an inductive definition for the notion that a computation σ satisfies formula p at i>0, denoted (σ,i)⊨p, follows [1, 13]:  (i)
(σ,i)⊨p if and only if si⊨p, where p is a state formula,(ii)
(σ,i)⊨¬p if and only if (σ,i)⊭p,(iii)
(σ,i)⊨p∨q if and only if (σ,i)⊨p or (σ,i)⊨q,(iv)
(σ,i)⊨Xp if and only if (σ,i+1)⊨p,(vi)
(σ,i)⊨pUq if and only if (σ,k)⊨q for some k≥i, and (σ,j)⊨p for all j,i≤j<k.Additionally, the temporal operators (eventually, always, and weak-until) are derived as follows:(i)
⋄p≡trueUp,(ii)
[]p≡¬⋄¬p,(iii)
pWq≡[]p∨(pUq).


### 2.2. Büchi Automata

Classical LTL model checking is based on a variation of the classic theory of finite automata [4]. While a finite automaton accepts only terminating executions, model checking requires a different type of machines that can handle executions that might not terminate. Such machines are necessary to model nonterminating systems such as operating systems, traffic lights, or ATMs. One such machine is a Büchi automaton. A Büchi automaton (BA) is a tuple (Q, ∑,  δ, Q0, F), where  (i)
Q is a finite set of states,(ii)
Q0⊆Q is a set of initial states,(iii)
∑ is an alphabet,(iv)
δ:Q×∑→2Q is a transition function,(v)
F⊆Q is a set of accepting states.An execution is a sequences0,s1,…, where for all isi∈Q and for all i≥0, (si,si+1)∈δ. A finite execution is an accepting execution if it terminates in a final state sf∈F. An infinite execution, also called an w-execution or w-run, is accepting if it passes through a state sf∈F infinitely often. An empty BA (accepts no words) is one that either terminates in a state that is not an accepting state or has no accepting state that is reachable from the initial state and that is visited infinitely often. The set of executions accepted by a BA is called the language of the BA.Languages of BAs represent a superset of those of LTL; every LTL formula can be represented by a BA. When a BA is generated from an LTL formula, the language of the BA represents only the traces accepted by the LTL formula. For example, the BA in Figure1 represents the language accepted by the LTL formula (a∪b). This formula specifies that b holds in the initial state of the computation, or a holds until b holds. The language of the BA in Figure 1 accepts the set of traces {b…, ab…, aab…, …, aaab}. Notice that each of these traces passes through the accepting state Final. This state is both reachable from the initial state and is visited infinitely often (by virtue of the self-transition marked 1).Figure 1
BA for “a∪b”.Various work has been done on the translation of LTL to BA to reduce the number of states in the resulting BA and to speed up the process of the BA generation. This paper compares three LTL to BA translators (along with the SPIN model checker) in the number of states in the BA generated from those LTL formulas for patterns and scopes.(i)
Temporal Message Parlor (TMP) [11] is the work of Kousha Etessami at Lucent Technologies.(ii)
LTL2BA [10] is the work of Denis Oddoux and Paul Gastin at the University of Paris 7, France.(iii)
LTL2NBA [12] is the work of Carsten Fritz of the Department of Computer Science at Christian-Albrechts University.


## 2.1. Linear Temporal Logic

This section briefly describes Linear Temporal Logic (LTL) and its semantics. A more detailed description of LTL can be found in Manna [13].Temporal Logic has been used to verify concurrent systems. There are three well used types of temporal Logic: Linear Temporal Logic (LTL), Computational Tree Logic (CTL), and CTL* [3]. Both LTL and CTL are subsets of CTL*. While CTL allows for branching type of behavior (i.e., semantically, formulas are defined both using the universal and existential quantifiers), LTL formulas describe specific path behavior (i.e., semantically, formulas are defined only using the universal quantifier). Formulas in this paper deal only with LTL.LTL is used in various model checkers such as SPIN [4], NUSMV [14], and Java Path-Finder [15] and is also used in runtime verification of Java programs [16].In LTL, a temporal formula is constructed inductively from a set of propositionsP by applying Boolean connectives ¬ and ∨ and temporal operators next (X) and until (U) as follows.  (i)
A proposition is a temporal formula.(ii)
Ifp and q are temporal formulas, then the followings are also temporal formulas:
(i)
¬p,(ii)
p∨q,(iii)
Xp,(iv)
pUq.A temporal formula that makes use only of Boolean connectives¬ and ∨ is called a state formula, whereas a formula that makes use of temporal operators X and U is called a temporal formula.LetP be a set of propositions; let σ be an infinite sequence of states or computation, denoted by σ: s0,s1,…, let ∑ be a set of states; let I(s) be an interpretation such that for all s∈∑, I(s)⊆P specifies the propositions that are true in state s. For a state formula, the satisfaction relation ⊨ is defined as follows: for a state s∈∑ and a proposition p in P, s satisfies p, denoted s⊨p, if and only if p∈I(s). In addition, an inductive definition for the notion that a computation σ satisfies formula p at i>0, denoted (σ,i)⊨p, follows [1, 13]:  (i)
(σ,i)⊨p if and only if si⊨p, where p is a state formula,(ii)
(σ,i)⊨¬p if and only if (σ,i)⊭p,(iii)
(σ,i)⊨p∨q if and only if (σ,i)⊨p or (σ,i)⊨q,(iv)
(σ,i)⊨Xp if and only if (σ,i+1)⊨p,(vi)
(σ,i)⊨pUq if and only if (σ,k)⊨q for some k≥i, and (σ,j)⊨p for all j,i≤j<k.Additionally, the temporal operators (eventually, always, and weak-until) are derived as follows:(i)
⋄p≡trueUp,(ii)
[]p≡¬⋄¬p,(iii)
pWq≡[]p∨(pUq).


## 2.2. Büchi Automata

Classical LTL model checking is based on a variation of the classic theory of finite automata [4]. While a finite automaton accepts only terminating executions, model checking requires a different type of machines that can handle executions that might not terminate. Such machines are necessary to model nonterminating systems such as operating systems, traffic lights, or ATMs. One such machine is a Büchi automaton. A Büchi automaton (BA) is a tuple (Q, ∑,  δ, Q0, F), where  (i)
Q is a finite set of states,(ii)
Q0⊆Q is a set of initial states,(iii)
∑ is an alphabet,(iv)
δ:Q×∑→2Q is a transition function,(v)
F⊆Q is a set of accepting states.An execution is a sequences0,s1,…, where for all isi∈Q and for all i≥0, (si,si+1)∈δ. A finite execution is an accepting execution if it terminates in a final state sf∈F. An infinite execution, also called an w-execution or w-run, is accepting if it passes through a state sf∈F infinitely often. An empty BA (accepts no words) is one that either terminates in a state that is not an accepting state or has no accepting state that is reachable from the initial state and that is visited infinitely often. The set of executions accepted by a BA is called the language of the BA.Languages of BAs represent a superset of those of LTL; every LTL formula can be represented by a BA. When a BA is generated from an LTL formula, the language of the BA represents only the traces accepted by the LTL formula. For example, the BA in Figure1 represents the language accepted by the LTL formula (a∪b). This formula specifies that b holds in the initial state of the computation, or a holds until b holds. The language of the BA in Figure 1 accepts the set of traces {b…, ab…, aab…, …, aaab}. Notice that each of these traces passes through the accepting state Final. This state is both reachable from the initial state and is visited infinitely often (by virtue of the self-transition marked 1).Figure 1
BA for “a∪b”.Various work has been done on the translation of LTL to BA to reduce the number of states in the resulting BA and to speed up the process of the BA generation. This paper compares three LTL to BA translators (along with the SPIN model checker) in the number of states in the BA generated from those LTL formulas for patterns and scopes.(i)
Temporal Message Parlor (TMP) [11] is the work of Kousha Etessami at Lucent Technologies.(ii)
LTL2BA [10] is the work of Denis Oddoux and Paul Gastin at the University of Paris 7, France.(iii)
LTL2NBA [12] is the work of Carsten Fritz of the Department of Computer Science at Christian-Albrechts University.


## 3. Prospec

The Property Specification tool (Prospec) [5–7] builds on the Specification Patterns System (SPS) [8, 9] by facilitating the identification of SPS patterns and scopes as well as validation of specifications. SPS defines patterns and scopes to assist the practitioner in formally specifying software properties. Patterns capture the expertise of developers by describing solutions to recurrent problems [17]. Each pattern describes the structure of specific behavior, defines the pattern's relationship with other patterns, and defines the scope over which the property holds.The main patterns defined by SPS are universality, absence, existence, precedence, and response.UniversalityP states that property P is true at every point of the execution; absenceP states that P is never true during the execution; existenceP states that P is true at some point in the execution; precedence(T,P) states that P holds before T holds;  response(P,T) states that if P holds, then T must hold at a future state. Response properties represent a temporal relation called cause-effect between two propositions. Prospec displays traces of computation to illustrate the subtle issues that exist within the different patterns and scopes, and it displays a decision tree to guide the user through a series of decisions in selecting the appropriate pattern and/or scope. Given a computation represented as a sequence of states, and a finite set of events E, a trace of computation is a list indicating, for each moment of time t, which events from the set E occur at t. Figure 2 shows the Prospec window for selecting a pattern and the traces of computation that are given to elucidate each pattern. Prospec enhances the definition of patterns and scope characteristics provided in the SPS website [18] by explicitly defining the relationships among the proposition that define a pattern and/or a scope and the boundaries defined by each scope. Tables 1 and 2 give those characteristics for pattern and scope, respectively, as they appear in the Prospec tool. These are the characteristics that were used by Salamah et al. [19] to verify the correctness of the LTL formulas for patterns and scopes. Prospec extends SPS by introducing a classification for defining sequential and concurrent behavior. This is accomplished by including composite propositions (CPs) as shown in Figure 3. Section 4 discusses composite propositions in more detail. While Prospec builds on SPS in defining the mapping of patterns and scopes into LTL, it makes some changes to those LTL formulas for patterns and scopes defined in SPS. (Comparing the new formulas in Section 4 with the original SPS formulas showed that the new formulas were at least as efficient in all cases with the exception of the case of the Response pattern within the AfterLUntilR scope in which SPS formula produced one fewer state in the never-claim as produced by LTL2BA, LTL2NBA, and TMP).  Salamah et al. [19] provide a listing of those modifications and the justification behind the changes. Table 3 presents Prospec's LTL mappings for each pattern and scope combination. These formulas along with the ones defined in Section 3 are the ones being compared in this paper.Table 1
Summary of characteristics for patterns in Prospec.
PatternCharacteristics(1) Event or conditionP does not hold within the states defined by the scope of interest(2) Theabsence property is also known as alarmExistence of (P)(1) Event or conditionP holds at least once within the states defined by the scope of interest(2) Theexistence property is also known as eventually.Universality of (P)(1) Event or conditionP holds in every state of the scope of interest(2) Theuniversality property is also known as safety or invariant(T) Precedes (P)(1)T holds before P holds, where T and P are events or conditions(2)T may hold several times before P holds(3)P does not hold before T holds(4)P may hold at the same state as T(5) IfT holds, then P may or may not hold(6) IfT holds, then T may or may not hold when P holds(7) Theprecedence property represents a cause-effect relation, where T denotes a cause and P denotes an effect(8) There is no effectP without a cause T(9)T precedes P is also known as T before P(T) Strictly Precedes (P)(1)T holds before P holds, where T and P are events or conditions(2)T may hold several times before P holds(3)P does not hold before T holds(4)P does not hold at the same state at which T holds(5) IfT holds, then P may or may not hold(6) IfT holds, then T does not hold when P holds(7) Theprecedence property represents a cause-effect relation, where T denotes a cause and P denotes an effect(8) There is no effectP without a cause T(9)T precedes P is also known as T before P(T) Responds to (P)(1)P must be followed by T, where P and T are events or conditions(2) SomeT follows each time that P holds(3) The same state at whichT holds may follow two or more states at which P holds(4)T may hold at the same state as P holds(5) IfT holds, then P may or may not hold at a previous state(6) Theresponse property represents a cause-effect relation, where P denotes a cause and T denotes an effect(7) If causeP holds, then at some future state effect T holds(8)T responds to P is also knows as T follows PTable 2
Summary of characteristics for scopes in Prospec.
ScopeCharacteristicsGlobal(1) The scope denotes the entire computation(2) The scope includes all the states in the computation(3) The interval defined by the scope occurs once in a computationBeforeR(1) The scope denotes a subsequence of states or events (an interval) that begins with the start of computation and ends with the state or event immediately preceding the event or state at whichR holds for first time in the computation(2) The interval does not include the state or event associated withR(3) The interval defined by the scope occurs once in a computation(4) One or more events (conditions) may be associated withR; a condition is a proposition and an event is a change in value of the proposition from one state to the nextAfterL(1) The scope denotes a subsequence of states or events (an interval) that begins with the first event or state at whichL holds and ends with termination of computation(2) The interval includes the state or event associated withL(3) The interval defined by the scope occurs once in a computation(4) One or more events (conditions) may be associated withL; a condition is a proposition and an event is a change in value of the proposition from one state to the nextBetweenL and R(1) The scope denotes a subsequence of states or events (an interval) that begins whenL holds and ends with the state or event immediately preceding the event or state at which R holds(2) Event or conditionL must hold and, at a different event or state in the future, R must hold(3) The interval includes the state or event associated withL(4) The interval does not include the state or event associated withR(5) The interval defined by the scope may occur more than once in a computation(6) Multiple intervals may be defined within an interval whenL holds more than once before R holds(7) One or more events (conditions) may be associated withL and RAfterL Until R(1) The scope denotes a subsequence of states or events (an interval) that begins whenL holds and ends either with the state or event immediately preceding the event or state at which R holds, or begins when L holds and ends with the termination of computation(2) The interval includes the state or event associated withL(3) The interval does not include the state or event associated withR(4) The interval may repeat during a computation(5) IfL holds and R does not hold, the interval ends with termination of a computation(6) The interval defined by the scope may occur more than once in a computation(7) Multiple intervals may be defined within an interval whenL holds more than once before R holds(8) One or more events (conditions) may be associated withL and RTable 3
Prospec's original LTL formulas for pattern and scope.
PatternScopeLTL FormulaAbsenceGlobal¬(⋄P)BeforeR⋄R→¬(¬(R)UP)AfterL¬(L)W(L∧¬(⋄P))BetweenL and R[]((L∧¬(R)∧⋄R)→¬(¬(R)UP))AfterL Until R[](L∧¬(R)→¬(¬(R)UP))ExistenceGlobal(⋄P)BeforeR⋄R→(¬(R)U(P∧¬(R)))AfterL¬(L)W(L∧(⋄P))BetweenL and R[]((L∧¬(R)∧⋄R)→(¬(R)U(P∧¬(R))))AfterL Until R[]((L∧¬(R))→(¬(R)U(P∧¬(R))))UniversalityGlobal[]PBeforeR⋄R→(PUR)AfterL¬(L)W(L∧[]P)BetweenL and R[]((L∧¬(R)∧⋄R)→(PUR))AfterL Until R[]((L∧¬(R))→(PWR))PrecedenceGlobal¬(P)WTBeforeR⋄R→(¬(P)U(T∨R))AfterL¬(L)W(L∧(¬(P)W(T)))BetweenL and R[]((L∧¬(R)∧⋄R)→(¬(P)U((T∨R))))AfterL Until R[](L∧¬(R)→(¬(P)W(T∨R)))ResponseGlobal[](P→⋄T)BeforeR⋄R→((P→(¬(R)U(T∧¬(R))))UR)AfterL(¬L)W(L∧[](P→⋄T))BetweenL and R[]((L∧¬(R)∧⋄R)→(P→(¬(R)U(T∧¬(R))))URAfterL Until R[]((L∧¬(R)→(P→(¬(R)U(T∧¬(R))))WR)Strict PrecedenceGlobal¬(P)W(T∧¬(P))BeforeR⋄R→(¬(P)U((T∧¬(P))∨R))AfterL¬(L)W(L∧(¬(P)W(T∧¬(P))))BetweenL and R[]((L∧¬(R)∧⋄R)→(¬(P)U((T∧¬(P))∨R)))AfterL Until R[](L∧¬(R)→(¬(P)W((T∧¬(P))∨R)))Figure 2
Prospec's pattern screen.Figure 3
Prospec's composite proposition screen.Note that Prospec added the definition ofstrict precedence, which is not available in SPS. This pattern describes the situation where Sstrictly precedesP, where S and P are events or conditions. Unlike the regular precedence pattern, S and P cannot hold at the same state in this pattern. Use of Strict Precedence enforces that S and P cannot hold at the same state.


## 4. New Pattern Formulas

The goal of the work presented by this paper is to improve the efficiency of the LTL specifications generated by Prospec. The efficiency is measured by the number of states in the BA corresponding to the negation of LTL specification. The BAs were produced using the SPIN model checker Version 4.2.7, and the LTL to BA translation tools LTL2BA, LTL2NBA, and the Temporal Message Parlor (TMP), all of which are available at a website maintained by Carsten Fritz [20].In order to reduce the number of states in the BA, our goal is to reduce the number of temporal operators within each formula. We were able to achieve this in 17 out of 30 formulas originally defined by Prospec. Table4 lists the new improved formulas, and Table 5 lists the results of the comparison between Prospec's original formulas and the new ones. In all the cases where we were able to reduce the number of temporal operators, the BAs generated by SPIN contained fewer states. Only in the case of the Response pattern with an AfterLUntilR scope did the new formula generate more states when used by the three BA generators. All the translation tools produced BAs with the same number of states for each new formula except in the case of the strict precedence with the afterLuntilR scope. In this case, the generated BAs by LTL2BA, TMP, and LTL2NBA produced one fewer state than the one generated by SPIN. This is significant, as it allows SPIN users to use the new formulas without having to use the other translators to produce never-claims that have to be inserted into the Promela code.Table 4
Prospec's new LTL formulas.
PatternScopeLTL FormulaAbsenceAfterL¬((¬L)U(L∧⋄P))AfterL Until R[](L∧¬(R)→¬(¬(R)UP))ExistenceBeforeR¬((¬P)UR)AfterL¬((¬L)U(L∧¬⋄P))BetweenL and R[]((L∧¬R)→(¬((¬P)UR)))UniversalityAfterL¬((¬L)U(L∧⋄¬P))AfterL Until R[]((L∧¬R)→(¬((P∧¬R)U((¬P)∧¬R))))PrecedenceGlobal¬((¬T)U(P∧¬T))AfterL¬((¬L)U(L∧((¬T)U(P∧¬T))))AfterL Until R[]((L∧¬R)→(¬(((¬T)∧¬R)U(P∧(¬T)∧¬R)))ResponseBeforeR¬((¬R)U(P∧(¬R)∧((¬T)UR)))AfterL¬((¬L)U(L∧(¬[](P→⋄T))))BetweenL and R[]((L∧¬R)→¬((¬R)U(P∧(¬R)∧((¬T)UR))))AfterL Until R[]((L∧¬R)→¬((¬R)U(P∧(¬R)∧(([]((¬T)∧¬R))∨((¬T)UR))))))Strict PrecedenceGlobal¬((¬(T∧¬P))UP))AfterL¬((¬L)U(L∧((¬(T∧¬P))UP)))BetweenL and R[]((L∧¬R)→(¬(((¬(T∧¬P))∧¬R)U(P∧(¬(T∧¬P))∧(¬R)∧⋄R))))AfterL Until R¬⋄(L∧(¬R)∧(((¬T)∧¬R)U(P∧¬R)))Table 5
Comparison results 1.
Pattern/ScopeSPINLTL2NBATMPLTL2BAOld, NewOld, NewOld, NewOld, NewAbsence AfterL14, 36, 33, 34, 3Existence BeforeR6, 22, 22, 22, 2Existence AfterL7, 23, 23, 23, 2Existence BetweenL and R7, 33, 33, 33, 3Universality AfterL14, 34, 33, 34, 3Universality AfterL Until R6, 33, 33, 33, 3Precedence Global5, 22, 22, 22, 2Precedence AfterL29, 36, 34, 34, 3Precedence AfterL Until R6, 33, 33, 33, 3Response BeforeR7, 33, 33, 33, 3Response AfterL22, 310, 33, 37, 3Response BetweenL and R8, 44, 44, 44, 4Response AfterL Until R9, 54, 54, 54, 5S-Precedence Global6, 32, 22, 22, 2S-Precedence AfterL27, 46, 34, 34, 3S-Precedence BetweenL and R5, 44, 44, 44, 4S-Precedence AfterL Until R7, 33, 33, 33, 3


### 4.1. Equivalence of LTL Formulas

An approach to demonstrating the equivalence of two LTL formulas is to compare the languages of the BAs generated from them. If the languages are identical, then the two LTL formulas are equivalent. To show this, we show that the first language is a subset of the second, and that the second is a subset of the first.Given two LTL formulasF1 andF2, let B1=(Q1,Σ,δ1,Q01,F1) be the BA for F1 and let B2=(Q2,Σ,δ2,Q02,F2) be the BA for F2. Label each transition in δ1 and δ2 with the names of the propositions that are true in the state entered by the transition. Let Σ be the union of all the transition labels in B1 and B2. Let L1 be the language accepted by B1 and let L2 be the language accepted by B2. To show that F1 and F2 are equivalent, we show that L1∩¬L2≡L2∩¬L1≡∅. (Since L1∩¬L2 is empty, ¬L2 must not contain any element of L1. Since L1 and L2 are both subsets of Σ*, L2 must contain every element of L1. Thus, L1⊂L2. Similarly, L2⊂L1. Thus, L2≡L1. B1 and B2 are equivalent if they accept the same language, thus B1≡B2, and F1≡F2.)Given two formulasFP and FN, where FP is the original Prospec formula and FN is the new formula, we used LTL2BA to generate a BA1 for (FP∧¬FN) and a BA2 for (¬FP∧FN). To assert that FP≡FN we have to check that BA1 and BA2 are both empty. To do this we developed a simple computer tool that checks the emptiness of a BA.


#### 4.1.1. Tool for Checking Emptiness

By definition a BA is empty if it does not contain a reachable accepting state that is visited infinitely often [3]. The LTL Validation Tool is designed to ensure that a given LTL formula is valid (i.e., its BA contains at least one reachable accepting state that is visited infinitely often). In this work, the tool is used to prove the equivalence of two formulas. As discussed above we show equivalence of two LTL formulas FP and FN by checking that resulting BAs for (FP∧¬FN) and (¬FP∧FN) are both empty.This validation tool makes use of LTL2BA’s Java interface (JLTL2BA) to translate the formulas (FP∧¬FN) and (¬FP∧FN) into the corresponding BAs. Once the BAs are available, the tool tries to assert that there are no reachable accepting states that are visited infinitely often. This is done by first finding all states reachable from every given state, then by linking these together to form cycles. Should the tool find a single acceptance cycle, that is, an acceptance state which is within a cycle then we declare that the BA is not empty.Figure4 shows the never-claim generated by the LTL Validation tool (through interfacing with LTL2BA) for the LTL formula “[]p→q” and the result generated by the tool to check for the emptiness of the BA (never-claim). Obviously the BA for this formula is not empty, and as a result the tool states that the formula is Valid (i.e., there is a reachable acceptance state that is within a cycle). Figure 5, on the other hand, shows the never-claim and the tool's result for the formula (¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))). This formula is the result of ANDing the negation of Prospec's original LTL formula for Universality of P within the AfterLUntilR scope with the new LTL formula for the same pattern/scope combination. The result returned by the tool specify that there is no reachable acceptance state that is within a cycle (i.e., the BA is empty). Figure 6 shows the graph of the never-claim in Figure 5.Figure 4
LTL validation tool's output for the formula[]p→q.Figure 5
LTL validation tool's output for the formula(¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).Figure 6
LTL2BA generated BA for(¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).Similarly, we used the LTL Validation tool to generate the BA for the LTL formula of ANDing Prospec's original LTL formula for Universality ofP within the AfterLUntilR scope with the negation of new LTL formula for the same pattern/scope combination. Figure 7 shows the graph of the never-claim for the formula (([]((l∧¬r)→(([]p)∨(pUr)))))∧¬([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))). This BA obviously does not contain a cycle that passes through an accepting state. The only accepting state in the BA is accept-S3. Although this state is reachable from the initial state, it is not visited infinitely often (i.e., there is no cycle that contains this state). As expected, the LTL Validation tool returned the message “There’s no reachable acceptance cycle within this BA”. Since both the BAs for ANDing the negation of Prospec's original LTL with the new LTL formula and for ANDing Prospec's original LTL formula with the negation of the new LTL formula are both empty, we conclude that both formulas are equivalent.Figure 7
LTL2BA generated BA for(([]((l∧¬r)→(([]p)∨(pUr)))))∧¬([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).In our work we performed the above mentioned procedure for all the new and original formulas in Tables3 and 4, and the results showed in every case that the new formula is semantically equivalent to the original one.


## 4.1. Equivalence of LTL Formulas

An approach to demonstrating the equivalence of two LTL formulas is to compare the languages of the BAs generated from them. If the languages are identical, then the two LTL formulas are equivalent. To show this, we show that the first language is a subset of the second, and that the second is a subset of the first.Given two LTL formulasF1 andF2, let B1=(Q1,Σ,δ1,Q01,F1) be the BA for F1 and let B2=(Q2,Σ,δ2,Q02,F2) be the BA for F2. Label each transition in δ1 and δ2 with the names of the propositions that are true in the state entered by the transition. Let Σ be the union of all the transition labels in B1 and B2. Let L1 be the language accepted by B1 and let L2 be the language accepted by B2. To show that F1 and F2 are equivalent, we show that L1∩¬L2≡L2∩¬L1≡∅. (Since L1∩¬L2 is empty, ¬L2 must not contain any element of L1. Since L1 and L2 are both subsets of Σ*, L2 must contain every element of L1. Thus, L1⊂L2. Similarly, L2⊂L1. Thus, L2≡L1. B1 and B2 are equivalent if they accept the same language, thus B1≡B2, and F1≡F2.)Given two formulasFP and FN, where FP is the original Prospec formula and FN is the new formula, we used LTL2BA to generate a BA1 for (FP∧¬FN) and a BA2 for (¬FP∧FN). To assert that FP≡FN we have to check that BA1 and BA2 are both empty. To do this we developed a simple computer tool that checks the emptiness of a BA.


### 4.1.1. Tool for Checking Emptiness

By definition a BA is empty if it does not contain a reachable accepting state that is visited infinitely often [3]. The LTL Validation Tool is designed to ensure that a given LTL formula is valid (i.e., its BA contains at least one reachable accepting state that is visited infinitely often). In this work, the tool is used to prove the equivalence of two formulas. As discussed above we show equivalence of two LTL formulas FP and FN by checking that resulting BAs for (FP∧¬FN) and (¬FP∧FN) are both empty.This validation tool makes use of LTL2BA’s Java interface (JLTL2BA) to translate the formulas (FP∧¬FN) and (¬FP∧FN) into the corresponding BAs. Once the BAs are available, the tool tries to assert that there are no reachable accepting states that are visited infinitely often. This is done by first finding all states reachable from every given state, then by linking these together to form cycles. Should the tool find a single acceptance cycle, that is, an acceptance state which is within a cycle then we declare that the BA is not empty.Figure4 shows the never-claim generated by the LTL Validation tool (through interfacing with LTL2BA) for the LTL formula “[]p→q” and the result generated by the tool to check for the emptiness of the BA (never-claim). Obviously the BA for this formula is not empty, and as a result the tool states that the formula is Valid (i.e., there is a reachable acceptance state that is within a cycle). Figure 5, on the other hand, shows the never-claim and the tool's result for the formula (¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))). This formula is the result of ANDing the negation of Prospec's original LTL formula for Universality of P within the AfterLUntilR scope with the new LTL formula for the same pattern/scope combination. The result returned by the tool specify that there is no reachable acceptance state that is within a cycle (i.e., the BA is empty). Figure 6 shows the graph of the never-claim in Figure 5.Figure 4
LTL validation tool's output for the formula[]p→q.Figure 5
LTL validation tool's output for the formula(¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).Figure 6
LTL2BA generated BA for(¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).Similarly, we used the LTL Validation tool to generate the BA for the LTL formula of ANDing Prospec's original LTL formula for Universality ofP within the AfterLUntilR scope with the negation of new LTL formula for the same pattern/scope combination. Figure 7 shows the graph of the never-claim for the formula (([]((l∧¬r)→(([]p)∨(pUr)))))∧¬([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))). This BA obviously does not contain a cycle that passes through an accepting state. The only accepting state in the BA is accept-S3. Although this state is reachable from the initial state, it is not visited infinitely often (i.e., there is no cycle that contains this state). As expected, the LTL Validation tool returned the message “There’s no reachable acceptance cycle within this BA”. Since both the BAs for ANDing the negation of Prospec's original LTL with the new LTL formula and for ANDing Prospec's original LTL formula with the negation of the new LTL formula are both empty, we conclude that both formulas are equivalent.Figure 7
LTL2BA generated BA for(([]((l∧¬r)→(([]p)∨(pUr)))))∧¬([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).In our work we performed the above mentioned procedure for all the new and original formulas in Tables3 and 4, and the results showed in every case that the new formula is semantically equivalent to the original one.


## 4.1.1. Tool for Checking Emptiness

By definition a BA is empty if it does not contain a reachable accepting state that is visited infinitely often [3]. The LTL Validation Tool is designed to ensure that a given LTL formula is valid (i.e., its BA contains at least one reachable accepting state that is visited infinitely often). In this work, the tool is used to prove the equivalence of two formulas. As discussed above we show equivalence of two LTL formulas FP and FN by checking that resulting BAs for (FP∧¬FN) and (¬FP∧FN) are both empty.This validation tool makes use of LTL2BA’s Java interface (JLTL2BA) to translate the formulas (FP∧¬FN) and (¬FP∧FN) into the corresponding BAs. Once the BAs are available, the tool tries to assert that there are no reachable accepting states that are visited infinitely often. This is done by first finding all states reachable from every given state, then by linking these together to form cycles. Should the tool find a single acceptance cycle, that is, an acceptance state which is within a cycle then we declare that the BA is not empty.Figure4 shows the never-claim generated by the LTL Validation tool (through interfacing with LTL2BA) for the LTL formula “[]p→q” and the result generated by the tool to check for the emptiness of the BA (never-claim). Obviously the BA for this formula is not empty, and as a result the tool states that the formula is Valid (i.e., there is a reachable acceptance state that is within a cycle). Figure 5, on the other hand, shows the never-claim and the tool's result for the formula (¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))). This formula is the result of ANDing the negation of Prospec's original LTL formula for Universality of P within the AfterLUntilR scope with the new LTL formula for the same pattern/scope combination. The result returned by the tool specify that there is no reachable acceptance state that is within a cycle (i.e., the BA is empty). Figure 6 shows the graph of the never-claim in Figure 5.Figure 4
LTL validation tool's output for the formula[]p→q.Figure 5
LTL validation tool's output for the formula(¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).Figure 6
LTL2BA generated BA for(¬([]((l∧¬r)→(([]p)∨(pUr)))))∧([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).Similarly, we used the LTL Validation tool to generate the BA for the LTL formula of ANDing Prospec's original LTL formula for Universality ofP within the AfterLUntilR scope with the negation of new LTL formula for the same pattern/scope combination. Figure 7 shows the graph of the never-claim for the formula (([]((l∧¬r)→(([]p)∨(pUr)))))∧¬([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))). This BA obviously does not contain a cycle that passes through an accepting state. The only accepting state in the BA is accept-S3. Although this state is reachable from the initial state, it is not visited infinitely often (i.e., there is no cycle that contains this state). As expected, the LTL Validation tool returned the message “There’s no reachable acceptance cycle within this BA”. Since both the BAs for ANDing the negation of Prospec's original LTL with the new LTL formula and for ANDing Prospec's original LTL formula with the negation of the new LTL formula are both empty, we conclude that both formulas are equivalent.Figure 7
LTL2BA generated BA for(([]((l∧¬r)→(([]p)∨(pUr)))))∧¬([]((l∧¬r)→(¬((p∧¬r)U((¬p)∧¬r))))).In our work we performed the above mentioned procedure for all the new and original formulas in Tables3 and 4, and the results showed in every case that the new formula is semantically equivalent to the original one.


## 5. Impact on the Use of CP

Mondragon et al. [7, 21] introduced composite propositions (CPs) classes to define the structure of multiple propositions to capture sequential and concurrent behavior. The work provided a CP taxonomy that can be used in the property elicitation and specification process. The taxonomy guides practitioners in formally specifying properties, illuminating the subtleties associated with multiple events and conditions. When relations have not been carefully analyzed, CP classes can expose incompleteness or ambiguities.CP classes defined as conditions are used to describe concurrency, and those defined as events are used to describe activation or synchronization of processes or actions. Table6 presents the semantics of the CP classes in LTL.Table 6
CP semantics in LTL (subscriptsC and E stand for condition and event, resp.).
CP ClassSemantics in LTL(1)AtLeastOneCP1∨P2∨⋯∨Pn(2)AtLeastOneE(¬P1∧⋯∧¬Pn)∧((¬P1∧⋯∧¬Pn)U(P1∨⋯∨Pn))(3)ParallelCP1∧P2∧⋯∧Pn(4)ParallelE(¬P1∧¬P2∧⋯∧¬Pn)∧((¬P1∧¬P2∧⋯∧¬Pn)U(P1∧P2∧⋯∧Pn))(5)ConsecutiveCP1∧X(P2∧X(⋯∧X(Pn))⋯)))(6)ConsecutiveE(¬P1∧¬P2∧⋯∧¬Pn)∧((¬P1∧¬P2∧⋯∧¬Pn)U((P1∧¬P2∧¬P3∧⋯∧¬Pn)∧X((P2∧¬P3∧⋯∧¬Pn)∧⋯∧X(Pn)⋯))(7)EventualCP1∧(¬P2U(P2∧⋯∧(¬PnUPn))⋯)(8)EventualE(¬P1∧⋯∧¬Pn)∧((¬P1∧⋯∧¬Pn)U(P1∧((¬P2∧⋯∧¬Pn)U(P2∧(⋯∧(Pn-1∧(¬PnUPn))⋯)))))(9)Strict EventualCP1∧X(¬P2U(P2∧⋯∧X(¬PnUPn))⋯)(10)Strict EventualE(¬P1∧⋯∧¬Pn)∧((¬P1∧⋯∧¬Pn)U(P1∧¬P2∧⋯∧¬Pn∧((¬P2∧⋯∧¬Pn)U(P2∧¬P3∧⋯∧¬Pn∧(⋯∧(Pn-1∧¬Pn∧(¬PnUPn))⋯)))))CP classes can be used to define boundaries of scopes and patterns with multiple propositions. For instance, an ordered sequence can define the left boundary of anafterL scope, and multiple events can define the cause part of a response pattern. The naïve use of CP classes in LTL formulas can result in a state explosion when using a model checker like SPIN. It is important to start with efficient LTL formulas such as the ones presented in Table 4 and to build on them when using these CP classes; otherwise the BAs generated by the LTL formulas would be too large to handle by the model checker. For example, consider the following property of an Automated Teller Machine (ATM): “After a user selects a withdrawal transaction, user's account is updated, money is dispensed, receipt is printed, and ATM card is returned.” Assume the following symbol assignments; “w”: withdrawal transaction is selected, “au”: account is updated, “md”: money is dispensed, “rp”: receipt is printed, and “cr”: card is returned.This property can be described using theExistence of P pattern within the AfterL scope where P is  the CP class EventualC. (P might also be of type Strict EventualC depending on the specification). ((au∧(⋄(md∧(⋄(rp∧(⋄cr))))))), and L is w. Using direct substitution in the original Prospec formula to specify this property the generated formula is ((□¬w)∨((¬w)U(w∧⋄(au∧((¬md)U(md∧((¬rp)U(rp∧((¬cr)Ucr))))))))). The negation of this formula produces a BA with  (i)
40 states using SPIN,(ii)
9 states using LTL2NBA and TMP,(iii)
17 states using LTL2BA.On the other hand, by direct substitution in the new formula, then the generated LTL formula is¬((¬w)U(w∧□¬(au∧((¬md)U(md∧((¬rp)U(rp∧((¬cr)Ucr)))))))). The negation of this formula produces a BA with  (i)
6 states using SPIN,(ii)
5 states using LTL2NBA and TMP,(iii)
9 states using LTL2BA.The previous example shows that although the difference in the number of states generated by the original LTL formulas in Table3 and those in Table 4 might seem negligible, this difference becomes more significant when using the notion of CP classes to specify properties.To further prove this point, Table7 provides a sample comparison of the original and new formulas when some propositions are replaced by certain CP classes. The table shows the number of states generated by SPIN, LTL2NBA, TMP, and LTL2BA for formulas of patterns and scopes using CP. Note that these values were generated running the tools on the negated formulas for the specified pattern and scope. Old indicates Prospec's original formula, and New indicates the new formula. In Table 7 only one of the propositions was replaced by a CP class at a time. In generating this sample, we only used three of the CP classes: ParallelE, EventualC, and Strict EventualC. We used these CP classes in replacing one of the propositions in four of the pattern/scope combinations; Absence of P After L, Existence of P After L, universality of P After L, and Q Responds to P After L. The choice of the CP classes and the pattern/scope combinations was based on the fact that direct substitution of the CP classes into the formulas for these pattern/scope formulas was possible. The CP class replacing a proposition is indicated by the subscript attached to the proposition. The number in the subscript refers to the number of the CP class in Table 6. Each CP class was comprised of two or three propositions. The goal was to include three propositions in each CP class; however in some cases some translation tools (mostly TMP and SPIN) could not generate BAs for the old Prospec formulas with CP classes containing three propositions. Those cases where CP classes were made of only two propositions are indicated with the symbol(*).Table 7
Comparison results 2.
Pattern/ScopeSPINLTL2NBATMPLTL2BAOld, NewOld, NewOld, NewOld, NewAbsence ofP4 After L25, 410, 44, 46, 4Absence ofP7 After L*26, 412, 417, 48, 4Absence ofP9 After L*33, 512, 420, 48, 4Absence ofP After L4*40, 615, 54, 514, 6Absence ofP After L7*45, 614, 49, 410, 6Absence ofP After L9*51, 814, 543, 49, 6Existence ofP4 After L15, 55, 35, 35, 3Existence ofP7 After L29, 97, 47, 49, 5Existence ofP9 After L29, 97, 47, 49, 5Existence ofP After L423, 59, 46, 46, 5Existence ofP After L7*22, 57, 311, 37, 5Existence ofP After L9*27, 76, 39, 37, 5Universality ofP After L440, 613, 54, 514, 6Universality ofP After L7*44, 617, 49, 410, 6Universality ofP After L9*51, 814, 445, 49, 6Q Responds to P4 After L*35, 719, 54, 411, 4Q Responds to P7 After L*20, 79, 614, 98, 6Q Responds to P9 After L*25, 88, 623, 98, 6Q4 Responds to P After L*32, 416, 44, 411, 4Q7 Responds to P After L43, 1015, 55, 520, 6Q9 Responds to P After L65, 1022, 55, 519, 6Q Responds to P After L4*63, 825, 54, 523, 6Q Responds to P After L7*68, 628, 415, 418, 6Q Responds to P After L9*104, 825, 46, 417, 6


## 6. Discussion

Tools that assist in the generation of formal specifications in LTL are important to the model checking community as they relieve the user from the burden of writing specifications in a language that is hard to read and write. Without the help of tools such as Prospec, the user might create faulty specifications. These tools must generate specifications that correspond to the intent of the user. Prospec was demonstrated to provide such support [19]. It is also important that these tools generate efficient formulas, since one of the main challenges of model checking is the state explosion problem. The smaller the size of the automata an LTL formula generates, the less likely that this problem will occur. Although this might not appear significant in the basic pattern-scope formulas as generated originally by Prospec, an example and a sample comparison given in the previous section show the effect on the number of states generated when using less efficient formulas as the base formulas when incorporating CP classes. The sample comparison also shows that in some cases, some translation tools could not generate BAs for the old Prospec formulas in which one of the propositions was replaced with CP classes containing three propositions.The new formulas provided by this work generate BAs with fewer states in almost all pattern/scope combinations regardless of LTL to BA translator used. In addition, the BAs of the new formulas generated by SPIN seem to always be comparable to those generated by the other more efficient translators. This is significant to SPIN users, since those users do not need to use different LTL to BA translators and manually insert the resulting never-claim into the Promela code.Another result of this work is that we are able to provide the user with more than one LTL mapping to the same pattern-scope combination. In some cases we can provide the user with three LTL formulas (considering the formulas provided by SPS) for a specific pattern and scope (Absence ofPBeforeR, e.g.). This, along with the detailed descriptions of patterns and scopes (such as timelines) provided by the Prospec tool, enhances a user's understanding of LTL and can be used as an educational tool. Table 8 shows the formulas generated using the original Prospec formulas while Table 9 provides those generated using the new formulas.Table 8
LTL formulas generated using the original Prospec's formulas.
Formulas(1)((□(¬l))∨((¬l)U(l∧¬⋄(((¬p∧¬pp∧¬ppp)∧((¬p∧¬pp∧¬ppp)U(p∧pp∧ppp)))))))(2)((□(¬l))∨((¬l)U(l∧¬⋄((p∧((¬pp)Upp))))))(3)((□(¬l))∨((¬l)U(l∧¬⋄((p∧X(¬ppUpp))))))(4)((□(¬((¬l∧¬ll)∧((¬l∧¬ll)U(l∧ll)))))∨((¬((¬l∧¬ll)∧((¬l∧¬ll)U(l∧ll))))U((((¬l∧¬ll)∧((¬l∧¬ll)U((l∧ll)∧¬⋄(p))))))))(5)((□(¬(l∧((¬ll)Ull))))∨((¬(l∧((¬ll)Ull)))U(((l∧((¬ll)U(ll∧¬⋄(p))))))))(6)((□(¬(l∧X(¬llUll))))∨((¬(l∧X(¬llUll)))U(((l∧X(¬llU(ll∧¬⋄(p))))))))(7)((□¬l)∨((¬l)U(l∧⋄(((¬p∧¬pp∧¬ppp)∧((¬p∧¬pp∧¬ppp)U(p∧pp∧ppp)))))))(8)((□¬l)∨((¬l)U(l∧⋄((p∧((¬pp)U(pp∧((¬ppp)Uppp))))))))(9)((□¬l)∨((¬l)U(l∧⋄((p∧X(¬ppU(pp∧X(¬pppUppp))))))))(10)((□¬(((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U(l∧ll∧lll)))))∨((¬((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U(l∧ll∧lll))))U((((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U((l∧ll∧lll)∧⋄p)))))))(11)((□¬((l∧((¬ll)Ull))))∨((¬(l∧((¬ll)Ull)))U(((l∧((¬ll)U(ll∧⋄p)))))))(12)((□¬((l∧X(¬llUll))))∨((¬(l∧X(¬llUll)))U(((l∧X(¬llU(ll∧⋄p)))))))(13)((□(¬((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U(l∧ll∧lll)))))∨((¬((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U(l∧ll∧lll))))U((((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U((l∧ll∧lll)∧□p)))))))(14)((□(¬(l∧((¬ll)Ull))))∨((¬(l∧((¬ll)Ull)))U((((l∧((¬ll)U(ll∧Wp))))))))(15)((□(¬(l∧X(¬llUll))))∨((¬(l∧X(¬llUll)))U((((l∧X(¬llU(ll∧Wp))))))))(16)((□(¬l))∨((¬l)U(l∧(□((((¬p)∧(¬pp))∧(((¬p)∧(¬pp))U(p∧pp)))→(((¬p)∧(¬pp))∧(((¬p)∧(¬pp))U(p∧pp∧⋄q))))))))(17)((□(¬l))∨((¬l)U(l∧(□((p∧((¬pp)U(pp))))→(p∧((¬pp)U(pp∧⋄q)))))))(18)((□(¬l))∨((¬l)U(l∧(□((p∧X((¬pp)U(pp))))→(p∧X((¬pp)U(pp∧⋄q)))))))(19)((□(¬l))∨((¬l)U(l∧□(p→⋄(((¬q)∧(¬qq))∧(((¬q)∧(¬qq))U(q∧qq)))))))(20)((□(¬l))∨((¬l)U(l∧□(p→⋄(q∧((¬qq)U(qq∧((¬qqq)Uqqq))))))))(21)((□(¬l))∨((¬l)U(l∧□(p→⋄(q∧X((¬qq)U(qq∧X((¬qqq)Uqqq))))))))(22)((□(¬(((¬l)∧(¬ll))∧(((¬l)∧(¬ll))U(l∧ll)))))∨((¬(((¬l)∧(¬ll))∧(((¬l)∧(¬ll))U(l∧ll))))U((((¬l)∧(¬ll))∧(((¬l)∧(¬ll))U(l∧ll∧□(p→⋄q)))))))(23)((□(¬(l∧((¬ll)U(ll)))))∨((¬(l∧((¬ll)U(ll))))U((l∧((¬ll)U(ll∧□(p→⋄q)))))))(24)((□(¬(l∧X((¬ll)U(ll)))))∨((¬(l∧X((¬ll)U(ll))))U((l∧X((¬ll)U(ll∧□(p→⋄q)))))))Table 9
LTL formulas generated using the New Prospec's formulas.
Formulas(1)(¬((¬l)U(l∧⋄(((¬p∧¬pp∧¬ppp)∧((¬p∧¬pp∧¬ppp)U(p∧pp∧ppp)))))))(2)(¬((¬l)U(l∧⋄((p∧((¬pp)Upp))))))(3)(¬((¬l)U(l∧⋄((p∧X(¬ppUpp))))))(4)(¬((¬((¬l∧¬ll)∧((¬l∧¬ll)U(l∧ll))))U((((¬l∧¬ll)∧((¬l∧¬ll)U((l∧ll)∧⋄p)))))))(5)(¬((¬(l∧((¬ll)Ull)))U(((l∧((¬ll)U(ll∧⋄p)))))))(6)(¬((¬(l∧X(¬llUll)))U(((l∧X(¬llU(ll∧⋄p)))))))(7)(¬((¬l)U(l∧¬⋄(((¬p∧¬pp∧¬ppp)∧((¬p∧¬pp∧¬ppp)U(p∧pp∧ppp)))))))(8)(¬((¬l)U(l∧¬⋄((p∧((¬pp)U(pp∧((¬ppp)Uppp))))))))(9)(¬((¬l)U(l∧¬⋄((p∧X(¬ppU(pp∧X(¬pppUppp))))))))(10)(¬((¬((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U(l∧ll∧lll))))U((((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U((l∧ll∧lll)∧¬⋄p)))))))(11)(¬((¬(l∧((¬ll)Ull)))U(((l∧((¬ll)U(ll∧¬⋄p)))))))(12)(¬((¬(l∧X(¬llUll)))U(((l∧X(¬llU(ll∧¬⋄p)))))))(13)(¬((¬((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U(l∧ll∧lll))))U((((¬l∧¬ll∧¬lll)∧((¬l∧¬ll∧¬lll)U((l∧ll∧lll)∧⋄¬p)))))))(14)(¬((¬(l∧((¬ll)Ull)))U(((l∧((¬ll)U(ll∧⋄¬p)))))))(15)(¬((¬(l∧X(¬llUll)))U(((l∧X(¬llU(ll∧⋄¬p)))))))(16)(¬((¬l)U(l∧¬□((((¬p)∧(¬pp))∧(((¬p)∧(¬pp))U(p∧pp)))→(((¬p)∧(¬pp))∧(((¬p)∧(¬pp))U(p∧pp∧⋄q)))))))(17)(¬((¬l)U(l∧¬□((p∧((¬pp)U(pp))))→(p∧((¬pp)U(pp∧⋄q))))))(18)(¬((¬l)U(l∧¬□((p∧X((¬pp)U(pp))))→(p∧X((¬pp)U(pp∧⋄q))))))(19)(¬((¬l)U(l∧¬□(p→⋄(((¬q)∧(¬qq))∧(((¬q)∧(¬qq))U(q∧qq)))))))(20)(¬((¬l)U(l∧¬□(p→⋄(q∧((¬qq)U(qq∧((¬qqq)Uqqq))))))))(21)(¬((¬l)U(l∧¬□(p→⋄(q∧X((¬qq)U(qq∧X((¬qqq)Uqqq))))))))(22)(¬((¬(((¬l)∧(¬ll))∧(((¬l)∧(¬ll))U(l∧ll)))U((((¬l)∧(¬ll))∧(((¬l)∧(¬ll))U(l∧ll∧¬□(p→⋄q))))))))(23)(¬((¬(l∧((¬ll)U(ll))))U((l∧((¬ll)U(ll∧¬□(p→⋄q)))))))(24)(¬((¬(l∧X((¬ll)U(ll))))U((l∧X((¬ll)U(ll∧¬□(p→⋄q)))))))



---

*Source: 869182-2011-06-22.xml*