# Degeneralization Algorithm for Generation of Büchi Automata Based on Contented Situation

Authors: Laixiang Shan; Jun Qin; Mingshi Chen; Zheng Qin
Journal: Journal of Applied Mathematics
 (2015)

---

## Abstract

We present on-the-fly degeneralization algorithm used to transform generalized Büchi automata (GBA) into Büchi Automata (BA) different from the standard degeneralization algorithm. Contented situation, which is used to record what acceptance conditions are satisfiable during expanding LTL formulae, is attached to the states and transitions in the BA. In order to get the deterministic BA, the Shannon expansion is used recursively when we expand LTL formulae by applying the tableau rules. On-the-fly degeneralization algorithm is carried out in each step of the expansion of LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae. The temporary automata are stored as syntax directed acyclic graph in order to save storage space. These ideas are implemented in a conversion algorithm used to build a property automaton corresponding to the given LTL formulae. We compare our method to previous work and show that it is more efficient for four sets of random formulae generated by LBTT.


---

## Body

## 1. Introduction

Model checking [1] is a formal verification technique used to check whether a model of the system verifies some desired properties for software or hardware systems. In order to verify whether the system satisfies some properties, a common method is to use linear temporal logic (LTL) model checking. When the given property is expressed in an LTL formula, the model checker usually transforms the negation of the LTL formula into a Büchi automaton (BA), builds the product of this BA with the system described as an automaton, and checks the emptiness of the product automaton. The size of the product automaton is usually exponential in the size of the system automaton and property automaton, because it is a Cartesian product of the system automaton and property automaton. If there are too many states and transitions, the product automaton will get too big to be verified in the available time. Generating a smaller and more deterministic property automaton in less time contributes to improving the efficiency of model checking.There are many outstanding conversion tools that implement the translation from an LTL formula to a BA effectively. Babiak et al. [2] proposed a series of improvement measures to improve performance of the conversion algorithm presented by Gastin and Oddoux [3] and implemented a new conversion tool, LTL3BA, which translates an LTL formula into a very weak alternating automaton (VWAA) with a co-Büchi accepting condition. VWAA is then translated into a transition based generalized Büchi automata (TGBA). Finally, TGBA is degeneralized into a BA. The time complexity of the alternation removal is O(n2n), which is the same magnitude as alternation removal of tableau-based algorithm [4]. Duret-Lutz [5] introduced many improvements to improve performance of the algorithm proposed by Couvreur [6]. These improvements have been applied in Spot, which is a C++ library for model checking. Spot uses TGBA to express LTL formulae into automata. Gerth et al. [7] proposed a classic algorithm that translates an LTL formula into a generalized Büchi automaton (GBA). This algorithm is a tableau-based translation method in on-the-fly fashion and has been applied in Spin [8].In order to obtain a BA from the given LTL formula, [2, 3, 5, 7] involve the intermediate automata (GBA or TGBA), perform simplification on the intermediate automata, and transform the intermediate automata into BA finally. Clarke et al. presented a standard degeneralization algorithm used to transform GBA into BA in Section 9.2.2 of [1]. This standard degeneralization algorithm is also adapted to transform a TGBA into a BA [3, 9]. Furthermore, Duret-Lutz proposed a better degeneralization algorithm based on the standard degeneralization algorithm in Section 4.2.2 of [5], which is related to the order in which the corresponding BDD variables were declared. Babiak et al. [10] presented the SCC-based degeneralization including many improvements to the standard degeneralization algorithm used to transform a TGBA into an equivalent BA. Chatterjee et al. [11] proposed the definition of the degeneralization index applied to transform the automaton with generalized Rabin pairs into a Rabin automaton.However, the standard degeneralization algorithm is used to transform a GBA or a TGBA into a BA, only when the expansion of LTL formulae is finished. We say that the standard degeneralization algorithm is a kind of postdegeneralization algorithm. The intermediate automata are needed to record the expansion of LTL formulae in the use of standard degeneralization algorithm. The standard degeneralization algorithm can transform a TGBA withn states and m acceptance conditions into an equivalent BA with one acceptance condition and at most nm states [12]. We have to search m!(m+1) possible degeneralizations.In this paper, we present on-the-fly degeneralization algorithm that is used to transform a GBA or a TGBA into an equivalent BA during expanding LTL formulae. We circumvent the intermediate automata and translate an LTL formula to a BA directly. Our method differs from the previous translation algorithms [2, 3, 5, 7] in two ways.(1)
Thecontented situation, which is a set of acceptance conditions, is attached to the states and transitions in the BA. According to the contented situation, we can determine which acceptance conditions are satisfied in the current state or transition.(2)
The process of degeneralization is carried out in each step of the expansion of LTL formulae. LTL formulae can be translated to the BA directly. The intermediate automata are no longer needed.Our research focuses on an efficient conversion algorithm producing a BA corresponding to an LTL formula directly. The contented situation is attached to the states and transitions in the BA in order to track whether the acceptance condition is satisfiable. The BA is described by ordered binary decision diagrams (OBDDs) and stored as syntax directed acyclic diagram (DAG). On-the-fly degeneralization algorithm is used in order to degeneralize GBA into BA during the expansion. The BA simplification is adopted in the algorithm in order to gain reduction on the size of the result automaton. In order to get the deterministic BA, the Shannon expansion is used recursively when we expand LTL formulae by applying the tableau rules. These measures cause a lot of improvement on the efficiency of the algorithm, especially when expanding the formulae containing a large amount of{U,R,F,G}-subformulae.The rest of this paper is organized as follows. In Section2, we provide preliminary notions used in this paper. Then, we describe the main ideas of our approach in Section 3. Overview of the algorithm is introduced in Section 4. In Section 5, a comparison between our method and previous works is presented. Finally, Section 6 closes the paper with conclusions.


## 2. Preliminaries

LTL is usually used to describe system constraints in formal method, which is a modal temporal logic with modalities referring to time. LetAP represent a finite set of atomic propositions. Let 2AP represent the set of subsets of AP. Let 22AP represent the set of propositional formulae induced by AP.Definition 1 (syntax of LTL formulae).
An LTL formula is usually composed of atomic propositions (p∈AP), proposition constants (⊤ (True) and ⊥ (False)), the logical operators (¬ (not), ∧ (and), and ∨ (or)), and the temporal modal operators (X (Next), U (Until), R (Release), G (Always), and F (Eventually)). Formally, the syntax of LTL formulae is defined inductively as follows:(i)
p, ⊤, and ⊥ are LTL formulae, respectively;(ii)
¬φ, φ∧ψ, φ∨ψ, Xφ, Fφ, Gφ, φUψ, and φRψ are LTL formulae, if φ and ψ are LTL formulae, respectively.
R-formula is the dual of U-formula. {R, F, G}-formula can be translated to U-formula by the following identities:(i)
φRψ≡¬(¬φU¬ψ);(ii)
Fφ≡⊤Uφ;(iii)
Gφ≡⊥Rφ≡¬F(¬φ)≡¬(⊤U¬φ).Definition 2 (Kripke structure).
A Kripke structure is a tupleM=(Q,δ,L) where Q is a finite set of states. δ is δ⊆Q×Q, a transition relation between states. L is Q→AP, labeling of the states.Definition 3 (semantics of LTL formulae).
LetM be a Kripke structure, and let ξ=ξ0ξ1ξ2⋯∈(2AP)ω be an infinite word in M. ξi=ξ[i]ξ[i+1]ξ[i+2]⋯ denotes the suffix starting at letter ξ[i]. The semantics of LTL formulae is defined inductively as follows:(i)
M,ξ⊨⊤;(ii)
M,ξ⊨p iff p∈ξ[0], for p∈AP;(iii)
M,ξ⊨¬φ iff ¬(ξ⊨φ);(iv)
M,ξ⊨φ∧ψ iff ξ⊨φ and ξ⊨ψ;(v)
M,ξ⊨φ∨ψ iff ξ⊨φ or ξ⊨ψ;(vi)
M,ξ⊨Xφ iff ξ1⊨φ;(vii)
M,ξ⊨Fφ iff ∃i≥0, ξi⊨φ;(viii)
M,ξ⊨Gφ iff ∀i≥0, ξi⊨φ;(ix)
M,ξ⊨φUψ iff ∃j≥0, ξj⊨ψ and ∀0≤i<j, ξi⊨φ;(x)
M,ξ⊨φRψ iff ∃j≥0, ξj⊨φ and ∀0≤i<j, ξi⊨φ and ξi⊨ψ.Remark 4.
Every LTL formula can be rewritten as an equivalent LTL formula in negation normal form (NNF), where operator¬ occurs only immediately in front of atomic propositions and ¬, ∧, and ∨ are the only allowed Boolean connectives. In this paper, we consider only such formulae. The NNF formula can be translated to an equivalent LTL formula by the following identities:
(1)¬φ∧ψ≡¬φ∨¬ψ,¬φ∨ψ≡¬φ∧¬ψ,¬¬φ≡φ,¬Xφ≡X¬φ,¬Fφ≡G¬φ,¬φUψ≡¬φR¬ψ,¬φRψ≡¬φU¬ψ,¬Gφ≡F¬φ.Definition 5 (Büchi automata).
Büchi automaton is a kind ofω-automata in which acceptance conditions are carried by the states. It is also called state-based Büchi automata that is a tuple A=〈Q,Σ,δ,I,F〉, where Q is a finite set of states. Σ is a finite input alphabet, Σ=2AP. δ:Q×Σ→2Q is a transition function. I⊆Q is a set of initial states. F⊆Q is a set of acceptance states. Let ξ=ξ0ξ1ξ2⋯∈Σω be an infinite word of A. An infinite sequence π=(q0,ξ[0],q1)(q1,ξ[1],q2)⋯∈δω is a run of A, where q0∈I is an initial state and qi+1∈δ(qi,ξ[i]) for all i≥0. Run(A) denotes the set of all runs of A. Let InfQ(π) denote the set of states that appear infinitely often in π. The run π is accepted by A, if and only if ∃π∈Run(A) with InfQ(π)∩F≠∅. An infinite word ξ is accepted by A, if some run of A over ξ is accepted.Definition 6 (transition based generalized Büchi automata).
Transition based generalized Büchi automaton (TGBA) is a Büchi automaton in which the set of subsets of acceptance conditions are carried by the transitions. It can be defined as a tupleT=〈Q,AP,δ,I,F〉, where Q is a finite set of states. AP is a finite set of atomic propositions. δ⊆Q×22AP×2F×Q is a transition relation, where each transition is labeled by a Boolean formula and a set of acceptance conditions. I⊆Q is a set of initial states. F={f1,f2,…,fm} is a finite set of acceptance conditions, m is the number of acceptance conditions, and 2F is the set of the subsets of acceptance conditions. An infinite sequence π=q0,l0,F0,q1⋯(qi,li,Fi,qi+1)⋯∈δω is a run of T, where q0∈I, li∈22AP, Fi∈2F, and qi+1∈δ(qi,li,Fi) for all i≥0. Run(T) denotes the set of all runs of T. Let Infδ(π) denote the set of transitions that appear infinitely often in π. The run π is accepted by T, if and only if ∀Z∈F, ∃π∈Run(T) with Infδ(π)∩Z≠∅. The accepting runs of T visit each acceptance set infinitely often.


## 3. Details of Our Approach

In this section, we introduce our ideas and the details of our approach. The next section gives an overview of the algorithm implementation.


### 3.1. Tableau Rules

Tableau rules [7] are often used to translate an LTL formula into a BA. The process of translation is as follows. First, an LTL formula φ, which is rewritten as NNF, is defined as the labeling of the initial state. Then, φ is expanded by applying the tableau rules recursively until no {U,R,F,G}-subformulae occur at the top level. The expansion of the formula is rewritten as acover by computing its disjunctive normal form (DNF). Each disjunct of thecover represents a state of the automaton. All propositional literals represent the label of the states, which are the acceptance conditions satisfied in this state. The X-formulae represent the label of the next state and determine the transitions outcoming from the current state. The transition is given by connecting each state to its successors. The tableau rules for LTL formulae are listed in Table 1. The automata constructed by the tableau rules are state-based Büchi automata.Table 1
Tableau rules for LTL formulae.
Formula
1st subformula
2nd subformula
φ
∧
ψ
{
φ
,
ψ
}
φ
∨
ψ
{
φ
}
{
ψ
}
X
φ
{
X
φ
}
φ
U
ψ
{
ψ
}
{
φ
,
X
(
φ
U
ψ
)
}
φ
R
ψ
{
φ
,
ψ
}
{
ψ
,
X
(
φ
R
ψ
)
}
F
φ
{
φ
}
{
X
F
φ
}
G
φ
{
φ
,
X
G
φ
}For instance, the expansions ofαUβ and αRβ are showed as (2). In thecover of αUβ, there are two propositional literals and one X-formula. Consider
(2)αUβ⟹β∨α∧XαUβ,αRβ⟹α∧β∨β∧XαRβ.
By observing the expansion of αUβ, we find that either (i) β holds and αUβ is satisfied or (ii) α holds and αUβ should be verified next, until αUβ has to be satisfied. Obviously, (ii) is infinite path probably. The expansion of αRβ is similar to αUβ. Intuitively, Fα⇒α∨XFα and Gα⇒α∧XGα product infinite path also.Although the method based on tableau rules can work well, the only challenging problem is how to avoid the unwanted infinite path. Because tableau rules cannot fully characterize{U,R,F,G}-formulae, each infinite path cannot identify models of the formula according to a graph which is constructed by the sole expansion law. In order to cope with the infinite path, thepromise has been presented in [13]. In this paper, a new approach,contented situation, is presented. We attach contented situation to the states and transitions in the automata during expanding LTL formulae. Although a sequence of BA is infinite probably, it is accepted as long as the formula is satisfied infinite often along the sequence. We record the acceptance conditions that are satisfied along the sequence. If all the acceptance conditions are satisfied, then we arrive at the final state. It guarantees the sequence of the {U,R,F,G}-formulae cannot be postponed infinitely.


### 3.2. Contented Situation

Thecontented situation is a set of acceptance conditions that are satisfiable along the path of a BA. Thecontented situation differs from thepromise in two ways: the definition and the purpose. The promise is the opposite of the acceptance conditions [13], while the contented situation is the set of the satisfying acceptance conditions. The promise is attached to the transitions only, while the contented situation is attached to the states or transitions. According to the promise, we can determine which acceptance conditions are not satisfied in the current transition. According to the contented situation, we can determine which acceptance conditions are satisfied in the current state or transition.Definition 7 (contented situation).
A functionS is defined to express the contented situation that is a mapping relationship from the states and transitions to the set of acceptance conditions. The formalized definition of S is as follows:
(3)S:Q∪T⟶2F,
where Q is a finite set of states, F represents a set of the acceptance conditions, and T is a finite set of transitions.
S indicates which acceptance conditions are satisfiable along a run of the automata. S of the initial state q0 is defined as ∅  ((*) of Algorithm 1).qi is the ith state and ti is the ith transition in the automata. The recursive calculation of S(ti) and S(qi) is shown as (**)-(***)  in Algorithm 1, where E(qi) represents the eventualities that should be satisfied along the sequence starting from qi. Let π=q1,lt1,q2q2,lt2,q3⋯ be a run in the automata. If π⊨φ and l(ti)∈π[i], then l(ti)⊨*φ. l(ti) represents the label of the transition ti.
For example, the expansion of(αUβ)Uγ is showed in Figure 1. The contented situations (in the curly braces) are attached to the states and transitions. F={αUβ,(αUβ)Uγ} and S(q0)=∅. S of the transition t0=(q0,α,q1) is ∅, because α cannot satisfy (αUβ)Uγ. S(q1)=∅, because ∄φ∈F∩E(q1)  s.t.φ∈S(t0). The formula is expanded recursively until S(q3)=∅; that is, the final state is reached.Algorithm 1
(1)S(q0)=∅;                (*)
(2)if  ∃φ∈Fwithφ∈Eqiandlti⊨*φ  then
S(ti)=S(qi)∪φ
else
S(ti)=S(qi);
endif                    (**)
(3)if  ∃φ∈Fwithφ∈E(qi+1)andφ∉S(ti)  then
S(qi+1)=S(ti)
else
S(qi+1)=∅;
endif;                  (***)Figure 1
The expansion of(αUβ)Uγ.


### 3.3. Computing Deterministic Covers

As said in Section3.1, the covers of LTL formulae are computed based on the recursive application of the tableau rules and on the subsequent computation of the DNF of the resulting formula. The determinism of the BA can be improved using a trick on the Shannon expansion during the expansion.For example, the cover ofGFφ∧GFψ is showed in (4). The BA corresponding to this cover has four successor states q0, q1, q2, and q3 with labels {φ,ψ}, {φ}, {ψ}, and {⊤}, respectively. The states, q1, q2, and q3, are nondeterministic decision states. Consider
(4)coverGFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧XFψ∧GFφ∧GFψ∨ψ∧XFφ∧GFφ∧GFψ∨⊤∧XFφ∧Fψ∧GFφ∧GFψ.The states,q1, q2, and q3, can be expanded by applying the Shannon expansion. The expansions of q1, q2, and q3 are showed in (5). According to the identical equation GFφ≡(Fφ∧XGFφ), we know (Fψ∧GFφ∧GFψ)≡(GFφ∧GFψ), (Fφ∧GFφ∧GFψ)≡(GFφ∧GFψ), and (Fφ∧Fψ∧GFφ∧GFψ)≡(GFφ∧GFψ):
(5)φ∧XFψ∧GFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧¬ψ∧XGFφ∧GFψ,ψ∧XFφ∧GFφ∧GFψ=ψ∧φ∧XGFφ∧GFψ∨ψ∧¬φ∧XGFφ∧GFψ,⊤∧XFφ∧Fψ∧GFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧¬ψ∧XGFφ∧GFψ∨¬φ∧ψ∧XGFφ∧GFψ∨¬φ∧¬ψ∧XGFφ∧GFψ.By combining the same items according to (5), (4) can be rewritten as (6). The BA corresponding to the cover in (6) has four successor states q0′, q1′, q2′, and q3′ with labels {φ,ψ}, {φ,¬ψ}, {¬φ,ψ}, and {¬φ,¬ψ}, respectively. The states, q0′, q1′, q2′, and q3′, are deterministic decision states. Consequently, deterministic covers give rise to deterministic automata. The TGBA corresponding to GFφ∧GFψ is showed in Figure 2(a):
(6)coverGFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧¬ψ∧XGFφ∧GFψ∨¬φ∧ψ∧XGFφ∧GFψ∨¬φ∧¬ψ∧XGFφ∧GFψ.Degeneralization of a TGBA corresponding toGFφ∧GFψ using the standard degeneralization algorithm.
(a)
TGBA corresponding toGFφ∧GFψ
(b)
Degeneralization of the TGBA
(c)
BA corresponding toGFφ∧GFψThere are2n labels to be considered during the expansion by applying the Shannon expansion over n atomic propositions in a BA. However, we remove the invalid nodes and combine equivalent states during the expansion of LTL formulae. It helps to ignore the useless labels. In the practical application, n is usually small enough so that the slowdown incurred by this method has little effect.


### 3.4. On-the-Fly Degeneralization

The degeneralization is a simple translation from a GBA to a BA. The standard degeneralization algorithm is presented by Clarke et al. [1]. This standard degeneralization algorithm can be used to translate a TGBA into a BA [2, 3, 5]. However, the standard algorithm is a kind of postdegeneralization algorithm; that is to say, it is used to translate a GBA or a TGBA to a BA, only when the expansion of LTL formulae is finished. The intermediate automata (GBA or TGBA) are needed to record the expansion of LTL formulae. For a TGBA, there are m!(m+1) possible degeneralizations by applying this algorithm. It takes a lot of time and storage space to complete the degeneralization.The degeneralization ofGFφ∧GFψ by applying the standard degeneralization algorithm is showed in Figure 2. The details are introduced in Section 4.2.2 of [5]. The TGBA corresponding to GFφ∧GFψ, which is showed in Figure 2(a), has two acceptance conditions {Acc[Fφ],Acc[Fψ]} that are indicated using colored marker (the blue dot and the red dot) per set. In Figure 2(b), in addition to the first level, the states in each level satisfy at least one acceptance condition. The states in the last level satisfy all the acceptance conditions. In Figure 2(b), all states in level 1 satisfy {Acc[Fφ]}; all states in level 2 satisfy {Acc[Fφ],Acc[Fψ]}. For example, q1 in level 1 satisfies {Acc[Fφ]}, and q2 in level 2 satisfies {Acc[Fφ],Acc[Fψ]} in Figure 2(b).All transitions are added to the degeneralized automata according to which acceptance conditions are satisfied in the current state. In order not to lose the transition, the TGBA is cloned inm+1 levels. The number of transitions in the degeneralized automata is three times the ones of TGBA. This setup guarantees that any accepting run in the degeneralized automata will correspond to an infinite run that visits all acceptance conditions infinitely often in the TGBA. The BA corresponding to GFφ∧GFψ is generated by removing the invalid states and transitions from degeneralized automata in Figure 2(c). The standard degeneralization algorithm generates many invalid states and transitions (see Figure 2(b)). It takes a lot of time to generate the degeneralized automata and remove the invalid states and transitions. A lot of storage space has to be used to save the temporal data.In this paper, we present on-the-fly degeneralization algorithm used to translate a GBA or a TGBA to a BA during the expansion of LTL formulae. The degeneralized automata are no longer needed in on-the-fly degeneralization algorithm. Our idea is that the degeneralization is carried out in each step of the expansion. As described in Section3.2, the contented situation is attached to all states in the BA. According to the contented situation, we know which acceptance conditions are satisfiable in each state. We can add the transitions to the BA according to which acceptance conditions are satisfied in the current state; that is to say, the outgoing transitions that carry the acceptance condition fj are redirected to the next state in which fj is satisfiable. The outgoing transitions that carry ∅ are redirected to the initial state. This setup guarantees that any accepting run can see all acceptance conditions infinitely often in the automata.On-the-fly degeneralization is a process in which the degeneralization process is carried out during the expansion of LTL formulae. Therefore, we can translate an LTL formula to a BA directly. The time used to generate the degeneralized automata and remove redundant states and transitions is saved. In Figure3, we translate GFφ∧GFψ to a BA directly by applying on-the-fly degeneralization. The contented situation is attached to the states and transitions. The contented situation of the transition ti is equal to the contented situation of the destination state of this transition. For example, the outgoing transitions that carry the acceptance condition {Acc[Fφ]} are redirected to the next state in which {Acc[Fφ]} is satisfiable. The outgoing transitions that carry the acceptance condition {Acc[Fψ]} are redirected to the next state in which {Acc[Fψ]} is satisfiable. The outgoing transitions that carry the acceptance condition {Acc[Fφ],Acc[Fψ]} are redirected to the next state in which {Acc[Fφ],Acc[Fψ]} is satisfiable. On-the-fly degeneralization is a process in which the standard degeneralization algorithm is carried out in each step of expansion. The BA in Figure 3 is equivalent to the BA in Figure 2(c).Figure 3
Building a BA corresponding toGFφ∧GFψ using on-the-fly degeneralization.Although the BA in Figure3 is different from the BA in Figure 2(c), they both guarantee that any accepting run visits all acceptance conditions infinitely often in the automata with the same number of states and transitions.


### 3.5. Representing a BA by OBDD

The BA can be represented by applying ordered binary decision diagrams (OBDDs) [14]. OBDD is a binary decision diagram that has an ordering for some list of variables. For example, we represent the BA corresponding to (αUβ)Uγ in Figure 1 by applying OBDDs. OBDDs representation is showed in Figure 4.Rewriting Büchi automata into an OBDD.
(a)
The BA corresponding to(αUβ)Uγ
(b)
Representing the BA by applying OBDDOBDDs can be regarded as a compressed representation of sets or relations. The checking equivalence is reduced to checking isomorphism between BDDs, when OBDDs are used to represent the BA. If the two Boolean functions have isomorphic representations in OBDDs, they are logically equivalent and can be merged. OBDD is a more concise representation for the cover by merging isomorphic subtrees.OBDD, which is a rooted, directed acyclic graph, can be stored as a syntax directed acyclic diagram (DAG). The use of a DAG has two advantages. First, less space is needed to store the automata. Second, if the result of computing each subtree is cached, there will be concomitant time savings. Sharing of subformulae also can work across multiple formulae. Because each subformula is unique, a cache is used to record the formula when we are travelling multiple formulae in order to speed up the algorithm. The running time is reduced by applying this kind of data structure.


## 3.1. Tableau Rules

Tableau rules [7] are often used to translate an LTL formula into a BA. The process of translation is as follows. First, an LTL formula φ, which is rewritten as NNF, is defined as the labeling of the initial state. Then, φ is expanded by applying the tableau rules recursively until no {U,R,F,G}-subformulae occur at the top level. The expansion of the formula is rewritten as acover by computing its disjunctive normal form (DNF). Each disjunct of thecover represents a state of the automaton. All propositional literals represent the label of the states, which are the acceptance conditions satisfied in this state. The X-formulae represent the label of the next state and determine the transitions outcoming from the current state. The transition is given by connecting each state to its successors. The tableau rules for LTL formulae are listed in Table 1. The automata constructed by the tableau rules are state-based Büchi automata.Table 1
Tableau rules for LTL formulae.
Formula
1st subformula
2nd subformula
φ
∧
ψ
{
φ
,
ψ
}
φ
∨
ψ
{
φ
}
{
ψ
}
X
φ
{
X
φ
}
φ
U
ψ
{
ψ
}
{
φ
,
X
(
φ
U
ψ
)
}
φ
R
ψ
{
φ
,
ψ
}
{
ψ
,
X
(
φ
R
ψ
)
}
F
φ
{
φ
}
{
X
F
φ
}
G
φ
{
φ
,
X
G
φ
}For instance, the expansions ofαUβ and αRβ are showed as (2). In thecover of αUβ, there are two propositional literals and one X-formula. Consider
(2)αUβ⟹β∨α∧XαUβ,αRβ⟹α∧β∨β∧XαRβ.
By observing the expansion of αUβ, we find that either (i) β holds and αUβ is satisfied or (ii) α holds and αUβ should be verified next, until αUβ has to be satisfied. Obviously, (ii) is infinite path probably. The expansion of αRβ is similar to αUβ. Intuitively, Fα⇒α∨XFα and Gα⇒α∧XGα product infinite path also.Although the method based on tableau rules can work well, the only challenging problem is how to avoid the unwanted infinite path. Because tableau rules cannot fully characterize{U,R,F,G}-formulae, each infinite path cannot identify models of the formula according to a graph which is constructed by the sole expansion law. In order to cope with the infinite path, thepromise has been presented in [13]. In this paper, a new approach,contented situation, is presented. We attach contented situation to the states and transitions in the automata during expanding LTL formulae. Although a sequence of BA is infinite probably, it is accepted as long as the formula is satisfied infinite often along the sequence. We record the acceptance conditions that are satisfied along the sequence. If all the acceptance conditions are satisfied, then we arrive at the final state. It guarantees the sequence of the {U,R,F,G}-formulae cannot be postponed infinitely.


## 3.2. Contented Situation

Thecontented situation is a set of acceptance conditions that are satisfiable along the path of a BA. Thecontented situation differs from thepromise in two ways: the definition and the purpose. The promise is the opposite of the acceptance conditions [13], while the contented situation is the set of the satisfying acceptance conditions. The promise is attached to the transitions only, while the contented situation is attached to the states or transitions. According to the promise, we can determine which acceptance conditions are not satisfied in the current transition. According to the contented situation, we can determine which acceptance conditions are satisfied in the current state or transition.Definition 7 (contented situation).
A functionS is defined to express the contented situation that is a mapping relationship from the states and transitions to the set of acceptance conditions. The formalized definition of S is as follows:
(3)S:Q∪T⟶2F,
where Q is a finite set of states, F represents a set of the acceptance conditions, and T is a finite set of transitions.
S indicates which acceptance conditions are satisfiable along a run of the automata. S of the initial state q0 is defined as ∅  ((*) of Algorithm 1).qi is the ith state and ti is the ith transition in the automata. The recursive calculation of S(ti) and S(qi) is shown as (**)-(***)  in Algorithm 1, where E(qi) represents the eventualities that should be satisfied along the sequence starting from qi. Let π=q1,lt1,q2q2,lt2,q3⋯ be a run in the automata. If π⊨φ and l(ti)∈π[i], then l(ti)⊨*φ. l(ti) represents the label of the transition ti.
For example, the expansion of(αUβ)Uγ is showed in Figure 1. The contented situations (in the curly braces) are attached to the states and transitions. F={αUβ,(αUβ)Uγ} and S(q0)=∅. S of the transition t0=(q0,α,q1) is ∅, because α cannot satisfy (αUβ)Uγ. S(q1)=∅, because ∄φ∈F∩E(q1)  s.t.φ∈S(t0). The formula is expanded recursively until S(q3)=∅; that is, the final state is reached.Algorithm 1
(1)S(q0)=∅;                (*)
(2)if  ∃φ∈Fwithφ∈Eqiandlti⊨*φ  then
S(ti)=S(qi)∪φ
else
S(ti)=S(qi);
endif                    (**)
(3)if  ∃φ∈Fwithφ∈E(qi+1)andφ∉S(ti)  then
S(qi+1)=S(ti)
else
S(qi+1)=∅;
endif;                  (***)Figure 1
The expansion of(αUβ)Uγ.


## 3.3. Computing Deterministic Covers

As said in Section3.1, the covers of LTL formulae are computed based on the recursive application of the tableau rules and on the subsequent computation of the DNF of the resulting formula. The determinism of the BA can be improved using a trick on the Shannon expansion during the expansion.For example, the cover ofGFφ∧GFψ is showed in (4). The BA corresponding to this cover has four successor states q0, q1, q2, and q3 with labels {φ,ψ}, {φ}, {ψ}, and {⊤}, respectively. The states, q1, q2, and q3, are nondeterministic decision states. Consider
(4)coverGFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧XFψ∧GFφ∧GFψ∨ψ∧XFφ∧GFφ∧GFψ∨⊤∧XFφ∧Fψ∧GFφ∧GFψ.The states,q1, q2, and q3, can be expanded by applying the Shannon expansion. The expansions of q1, q2, and q3 are showed in (5). According to the identical equation GFφ≡(Fφ∧XGFφ), we know (Fψ∧GFφ∧GFψ)≡(GFφ∧GFψ), (Fφ∧GFφ∧GFψ)≡(GFφ∧GFψ), and (Fφ∧Fψ∧GFφ∧GFψ)≡(GFφ∧GFψ):
(5)φ∧XFψ∧GFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧¬ψ∧XGFφ∧GFψ,ψ∧XFφ∧GFφ∧GFψ=ψ∧φ∧XGFφ∧GFψ∨ψ∧¬φ∧XGFφ∧GFψ,⊤∧XFφ∧Fψ∧GFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧¬ψ∧XGFφ∧GFψ∨¬φ∧ψ∧XGFφ∧GFψ∨¬φ∧¬ψ∧XGFφ∧GFψ.By combining the same items according to (5), (4) can be rewritten as (6). The BA corresponding to the cover in (6) has four successor states q0′, q1′, q2′, and q3′ with labels {φ,ψ}, {φ,¬ψ}, {¬φ,ψ}, and {¬φ,¬ψ}, respectively. The states, q0′, q1′, q2′, and q3′, are deterministic decision states. Consequently, deterministic covers give rise to deterministic automata. The TGBA corresponding to GFφ∧GFψ is showed in Figure 2(a):
(6)coverGFφ∧GFψ=φ∧ψ∧XGFφ∧GFψ∨φ∧¬ψ∧XGFφ∧GFψ∨¬φ∧ψ∧XGFφ∧GFψ∨¬φ∧¬ψ∧XGFφ∧GFψ.Degeneralization of a TGBA corresponding toGFφ∧GFψ using the standard degeneralization algorithm.
(a)
TGBA corresponding toGFφ∧GFψ
(b)
Degeneralization of the TGBA
(c)
BA corresponding toGFφ∧GFψThere are2n labels to be considered during the expansion by applying the Shannon expansion over n atomic propositions in a BA. However, we remove the invalid nodes and combine equivalent states during the expansion of LTL formulae. It helps to ignore the useless labels. In the practical application, n is usually small enough so that the slowdown incurred by this method has little effect.


## 3.4. On-the-Fly Degeneralization

The degeneralization is a simple translation from a GBA to a BA. The standard degeneralization algorithm is presented by Clarke et al. [1]. This standard degeneralization algorithm can be used to translate a TGBA into a BA [2, 3, 5]. However, the standard algorithm is a kind of postdegeneralization algorithm; that is to say, it is used to translate a GBA or a TGBA to a BA, only when the expansion of LTL formulae is finished. The intermediate automata (GBA or TGBA) are needed to record the expansion of LTL formulae. For a TGBA, there are m!(m+1) possible degeneralizations by applying this algorithm. It takes a lot of time and storage space to complete the degeneralization.The degeneralization ofGFφ∧GFψ by applying the standard degeneralization algorithm is showed in Figure 2. The details are introduced in Section 4.2.2 of [5]. The TGBA corresponding to GFφ∧GFψ, which is showed in Figure 2(a), has two acceptance conditions {Acc[Fφ],Acc[Fψ]} that are indicated using colored marker (the blue dot and the red dot) per set. In Figure 2(b), in addition to the first level, the states in each level satisfy at least one acceptance condition. The states in the last level satisfy all the acceptance conditions. In Figure 2(b), all states in level 1 satisfy {Acc[Fφ]}; all states in level 2 satisfy {Acc[Fφ],Acc[Fψ]}. For example, q1 in level 1 satisfies {Acc[Fφ]}, and q2 in level 2 satisfies {Acc[Fφ],Acc[Fψ]} in Figure 2(b).All transitions are added to the degeneralized automata according to which acceptance conditions are satisfied in the current state. In order not to lose the transition, the TGBA is cloned inm+1 levels. The number of transitions in the degeneralized automata is three times the ones of TGBA. This setup guarantees that any accepting run in the degeneralized automata will correspond to an infinite run that visits all acceptance conditions infinitely often in the TGBA. The BA corresponding to GFφ∧GFψ is generated by removing the invalid states and transitions from degeneralized automata in Figure 2(c). The standard degeneralization algorithm generates many invalid states and transitions (see Figure 2(b)). It takes a lot of time to generate the degeneralized automata and remove the invalid states and transitions. A lot of storage space has to be used to save the temporal data.In this paper, we present on-the-fly degeneralization algorithm used to translate a GBA or a TGBA to a BA during the expansion of LTL formulae. The degeneralized automata are no longer needed in on-the-fly degeneralization algorithm. Our idea is that the degeneralization is carried out in each step of the expansion. As described in Section3.2, the contented situation is attached to all states in the BA. According to the contented situation, we know which acceptance conditions are satisfiable in each state. We can add the transitions to the BA according to which acceptance conditions are satisfied in the current state; that is to say, the outgoing transitions that carry the acceptance condition fj are redirected to the next state in which fj is satisfiable. The outgoing transitions that carry ∅ are redirected to the initial state. This setup guarantees that any accepting run can see all acceptance conditions infinitely often in the automata.On-the-fly degeneralization is a process in which the degeneralization process is carried out during the expansion of LTL formulae. Therefore, we can translate an LTL formula to a BA directly. The time used to generate the degeneralized automata and remove redundant states and transitions is saved. In Figure3, we translate GFφ∧GFψ to a BA directly by applying on-the-fly degeneralization. The contented situation is attached to the states and transitions. The contented situation of the transition ti is equal to the contented situation of the destination state of this transition. For example, the outgoing transitions that carry the acceptance condition {Acc[Fφ]} are redirected to the next state in which {Acc[Fφ]} is satisfiable. The outgoing transitions that carry the acceptance condition {Acc[Fψ]} are redirected to the next state in which {Acc[Fψ]} is satisfiable. The outgoing transitions that carry the acceptance condition {Acc[Fφ],Acc[Fψ]} are redirected to the next state in which {Acc[Fφ],Acc[Fψ]} is satisfiable. On-the-fly degeneralization is a process in which the standard degeneralization algorithm is carried out in each step of expansion. The BA in Figure 3 is equivalent to the BA in Figure 2(c).Figure 3
Building a BA corresponding toGFφ∧GFψ using on-the-fly degeneralization.Although the BA in Figure3 is different from the BA in Figure 2(c), they both guarantee that any accepting run visits all acceptance conditions infinitely often in the automata with the same number of states and transitions.


## 3.5. Representing a BA by OBDD

The BA can be represented by applying ordered binary decision diagrams (OBDDs) [14]. OBDD is a binary decision diagram that has an ordering for some list of variables. For example, we represent the BA corresponding to (αUβ)Uγ in Figure 1 by applying OBDDs. OBDDs representation is showed in Figure 4.Rewriting Büchi automata into an OBDD.
(a)
The BA corresponding to(αUβ)Uγ
(b)
Representing the BA by applying OBDDOBDDs can be regarded as a compressed representation of sets or relations. The checking equivalence is reduced to checking isomorphism between BDDs, when OBDDs are used to represent the BA. If the two Boolean functions have isomorphic representations in OBDDs, they are logically equivalent and can be merged. OBDD is a more concise representation for the cover by merging isomorphic subtrees.OBDD, which is a rooted, directed acyclic graph, can be stored as a syntax directed acyclic diagram (DAG). The use of a DAG has two advantages. First, less space is needed to store the automata. Second, if the result of computing each subtree is cached, there will be concomitant time savings. Sharing of subformulae also can work across multiple formulae. Because each subformula is unique, a cache is used to record the formula when we are travelling multiple formulae in order to speed up the algorithm. The running time is reduced by applying this kind of data structure.


## 4. Overview of Algorithm

In the current, many kinds of state-of-the-art algorithm used to translate an LTL formula to a BA can be divided into four main phases: simplifying the formulae, translating an LTL formula to a BA, the BA simplification, and degeneralization of the BA.In this paper, we focus on phase 2 and phase 3. According to the new approach proposed in the previous section, we have conceived and implemented a new translation tool, calledltltoba, which builds a BA from an LTL formula. The contented situation and on-the-fly degeneralization algorithm are used in these tools. Our method differs from the previous translation algorithms [2, 3, 5, 7] in two steps.(1)
Our algorithm circumvents the intermediate automata and translates an LTL formula to a BA directly.(2)
On-the-fly degeneralization is used in our algorithm. Phase 4 is not needed.


### 4.1. The Data Structure

The basic data structure that the automata graph construction algorithm manipulates is theNode, which contains the following fields:NodeSet, the set of the unprocessed states;DisjunctSet, the set of the disjuncts of the cover; f, the input LTL formulae; q,q′, the state of the automata;t, the transition of the automata;src, source node of a transition;dst, destination node of a transition; l, the label of the state or transition; F, the set of the acceptance conditions.In order to describe the BA, the class is defined as shown in Algorithm2.Algorithm 2
class
T
_
B
A
public:
void initialize_statef∅;  // the initial node is defined as f, the contented situation is ∅.
void add_stateqSq; // adding a state to the BA. If a BA has not the state q, q is added to
the BA directly. If a BA has a stateq′ with l(q)=l(q′), then S(q′)=S(q)∪S(q′) and q is discarded.
void add_transtSt;// adding a transition to the BA. If a BA has not the
transitiont, t is added to the BA directly. If a BA has a transition t′ with src(t)=src(t′),
dst(t)=dst(t′) and S(t)=S(t′), then label(t′)=label(t)∪label(t′) and t is discarded.
string search_stateq  // Searching the state q in the BA.
If∃q′∈BA  s.t.l(q)=l(q′), then q already exists in the BA and return q′.
Otherwise, return∅.
string s.t.(t) // Searching the transition t in the BA. If ∃t′∈BA  s.t.src(t)=src(t′)
anddst(t)=dst(t′), then t already exists in the BA and return t′. Otherwise, return ∅.


### 4.2. The Main Algorithm

The main algorithm of ltltoba, which is described in Algorithm3, is used to transform a given LTL formula f to a BA. The idea is very clear; we expand an LTL formula recursively by applying the tableau rules. A simple depth-first-search strategy is used in the expansion operation. The resulting formula is rewritten into a cover by computing its DNF. For each disjunct of the cover, the contented situation of state or transition is calculated according to the calculation using (**)-(***) of Algorithm 1. If the new states do not exist in the BA, they will be added to BA. The function add_state() tells us how to add a state to the BA. Then, the transitions are added to the BA by applying the on-the-fly degeneralization algorithm (Algorithm 3, lines (24)–(30)). If the S(qi) has been reset to ∅, the state qi is the final state. The details of the main algorithm are shown in Algorithm 3.Algorithm 3:The main algorithm of ltltoba.
(1)Input: an LTL formula f;
(2)Output: a BA corresponding to f;
(3)
(4)procedure LTL_to_BA_translation
(5)NodeSet←{f∣∅};
(6)BA.initialize_state(f∣∅);
(7)while  NodeSet≠∅  do
(8) let q∈NodeSet;
(9) NodeSet←NodeSet∖{q};
(10)φ←apply_tableau_rules(q);
(11)for each  p at the top level in φ  do
(12)φ←(p∧φ[{p}])∨(¬p∧φ[{¬p}]);
(13)  simplify(φ);
(14)end for
(15) DisjunctSet← the DNF of φ;
(16)for each d∈DisjunctSet  do
(17)  letd←l(t)∧X(q′);
(18)S(t)←calculateusing  (**);
(19)S(q′)←calculateusing  (***);
(20)if  BA.search_state(q′)=∅  then
(21)BA.add_state(q′∣S(q′));
(22)   NodeSet← NodeSet  ∪  {q′∣S(q′)};
(23)end if
(24)if  (t′←BA.search_trans(t))=∅  then
(25)BA.add_trans(q,l(t),q′,S(t))
(26)else
(27)   lett′←(q,lt,q′,St);
(28)l(t′)←l(t′)∨l(t);
(29)S(t′)←S(t′)∪S(t);
(30)end if
(31)end for
(32)end while
(33)return BA;
(34)End procedure


### 4.3. Preliminary Analysis on Complexity

The most time-consuming component in ltltoba is the process of calculating thecover of the formulae. In our work, we remove the redundant states and transitions in each step of expansion. The size of the resulting automata is smaller. Representing the cover by OBDDs contributes to merging equivalent formulae. The on-the-fly degeneralization algorithm contributes to reducing the running time. Therefore, the operation of the algorithm is more efficient and the running time becomes faster. The worst time complexity of the expansion algorithm is O(2n) (where n is the number of elements in f), because we have to travel all nodes in worst case. The average time complexity of our algorithm is much lower than O(2n).


## 4.1. The Data Structure

The basic data structure that the automata graph construction algorithm manipulates is theNode, which contains the following fields:NodeSet, the set of the unprocessed states;DisjunctSet, the set of the disjuncts of the cover; f, the input LTL formulae; q,q′, the state of the automata;t, the transition of the automata;src, source node of a transition;dst, destination node of a transition; l, the label of the state or transition; F, the set of the acceptance conditions.In order to describe the BA, the class is defined as shown in Algorithm2.Algorithm 2
class
T
_
B
A
public:
void initialize_statef∅;  // the initial node is defined as f, the contented situation is ∅.
void add_stateqSq; // adding a state to the BA. If a BA has not the state q, q is added to
the BA directly. If a BA has a stateq′ with l(q)=l(q′), then S(q′)=S(q)∪S(q′) and q is discarded.
void add_transtSt;// adding a transition to the BA. If a BA has not the
transitiont, t is added to the BA directly. If a BA has a transition t′ with src(t)=src(t′),
dst(t)=dst(t′) and S(t)=S(t′), then label(t′)=label(t)∪label(t′) and t is discarded.
string search_stateq  // Searching the state q in the BA.
If∃q′∈BA  s.t.l(q)=l(q′), then q already exists in the BA and return q′.
Otherwise, return∅.
string s.t.(t) // Searching the transition t in the BA. If ∃t′∈BA  s.t.src(t)=src(t′)
anddst(t)=dst(t′), then t already exists in the BA and return t′. Otherwise, return ∅.


## 4.2. The Main Algorithm

The main algorithm of ltltoba, which is described in Algorithm3, is used to transform a given LTL formula f to a BA. The idea is very clear; we expand an LTL formula recursively by applying the tableau rules. A simple depth-first-search strategy is used in the expansion operation. The resulting formula is rewritten into a cover by computing its DNF. For each disjunct of the cover, the contented situation of state or transition is calculated according to the calculation using (**)-(***) of Algorithm 1. If the new states do not exist in the BA, they will be added to BA. The function add_state() tells us how to add a state to the BA. Then, the transitions are added to the BA by applying the on-the-fly degeneralization algorithm (Algorithm 3, lines (24)–(30)). If the S(qi) has been reset to ∅, the state qi is the final state. The details of the main algorithm are shown in Algorithm 3.Algorithm 3:The main algorithm of ltltoba.
(1)Input: an LTL formula f;
(2)Output: a BA corresponding to f;
(3)
(4)procedure LTL_to_BA_translation
(5)NodeSet←{f∣∅};
(6)BA.initialize_state(f∣∅);
(7)while  NodeSet≠∅  do
(8) let q∈NodeSet;
(9) NodeSet←NodeSet∖{q};
(10)φ←apply_tableau_rules(q);
(11)for each  p at the top level in φ  do
(12)φ←(p∧φ[{p}])∨(¬p∧φ[{¬p}]);
(13)  simplify(φ);
(14)end for
(15) DisjunctSet← the DNF of φ;
(16)for each d∈DisjunctSet  do
(17)  letd←l(t)∧X(q′);
(18)S(t)←calculateusing  (**);
(19)S(q′)←calculateusing  (***);
(20)if  BA.search_state(q′)=∅  then
(21)BA.add_state(q′∣S(q′));
(22)   NodeSet← NodeSet  ∪  {q′∣S(q′)};
(23)end if
(24)if  (t′←BA.search_trans(t))=∅  then
(25)BA.add_trans(q,l(t),q′,S(t))
(26)else
(27)   lett′←(q,lt,q′,St);
(28)l(t′)←l(t′)∨l(t);
(29)S(t′)←S(t′)∪S(t);
(30)end if
(31)end for
(32)end while
(33)return BA;
(34)End procedure


## 4.3. Preliminary Analysis on Complexity

The most time-consuming component in ltltoba is the process of calculating thecover of the formulae. In our work, we remove the redundant states and transitions in each step of expansion. The size of the resulting automata is smaller. Representing the cover by OBDDs contributes to merging equivalent formulae. The on-the-fly degeneralization algorithm contributes to reducing the running time. Therefore, the operation of the algorithm is more efficient and the running time becomes faster. The worst time complexity of the expansion algorithm is O(2n) (where n is the number of elements in f), because we have to travel all nodes in worst case. The average time complexity of our algorithm is much lower than O(2n).


## 5. Experimental Results

The main algorithm, which is described in Section4, is an implementation in C++ by applying CUDD library. This algorithm implements translating an LTL formula to a BA and removing redundant state or transition of the resulting automata. On-the-fly degeneralization is used in this algorithm. It can be used as kernel of other phases.In this section, we extensively tested ltltoba, in comparison with the two state-of-the-art tools, LTL3BA v1.0.2 and Spot v1.1.4. We consider the running time and the number of states and transitions of the resulting automata. For the comparison of the results, we use LBTT 1.2.1 which takes a set of translation tools for testing their running time as input. LBTT [15] is a randomized testbench tool which gives a series of randomly generated formulae to the testing algorithms.We run all tests on a computer with processor Pentium Dual-Core CPU E5300 @2.6 GHz, 4 GB of memory. The operating system was Ubuntu 12.04 LTS. Ltltoba, Spot, and LTL3BA were compiled on this machine to achieve satisfactory results. For the purpose of tests, all programs were configured with the formula simplification enabled.We compare those translators on four sets of random formulae generated by LBTT. Benchmark 1 and Benchmark 3 contain 300 formulae of the length 15–30 and their negation. The number of atomic propositions in Benchmark 1 is 3, and the other is 8. Benchmark 2 and Benchmark 4 contain 400 formulae of the length 25–40 and their negation. The number of atomic propositions in Benchmark 2 is 3, and the other is 8. Table2 presents the cumulative results of translations of all formulae in the four sets. The table illustrates the gradual effect of modification of each of the translators. The automata produced by ltltoba are in sum slightly better than the automata produced by other tools.Table 2
LBTT parameters used for formulae generation.
Translators
Benchmark 1
Benchmark 2
States
Trans.
Time (s)
States
Trans.
Time (s)
LTL3BA
3938
8816
21.25
8765
25251
42.62
LTL3BA-M
3527
7611
18.57
7629
20795
35.53
LTL3BA-S
3650
7697
18.91
7586
19703
34.11
LTL3BA-M-S
3389
7002
17.32
6973
17602
30.72
Spot-BA-any-high
3442
7342
17.98
7621
20461
35.11
Spot-BA-deterministic-high
3091
6447
15.89
6306
15689
27.49
Spot-BA-small-high
2933
5863
14.66
5972
14193
25.20
ltltoba
2886
5437
14.38
5721
13817
23.32
Benchmark 3
Benchmark 4
States
Trans.
Time (s)
States
Trans.
Time (s)
LTL3BA
6474
23526
50.00
18625
103332
152.44
LTL3BA-M
5772
21134
44.84
15722
79481
119.00
LTL3BA-S
6143
21382
45.88
16855
83760
125.77
LTL3BA-M-S
5561
19442
41.67
14582
67669
102.82
Spot-BA-any-high
5730
20850
44.30
17008
90438
134.31
Spot-BA-deterministic-high
5289
18531
39.70
15460
76400
124.82
Spot-BA-small-high
4927
16468
35.66
13452
59704
91.45
ltltoba
4893
15635
34.38
11708
49382
83.34


## 6. Conclusion

In this paper, we presented a new approach to convert an LTL formula to a BA more efficiently. Because the size of the product automata will jump exponentially when we do the product operation, the smaller and more deterministic property automata can improve efficiency of model checking. In order to deal with the infinite path during the expansion of LTL formulae, we attach the contented situation to the state and transition in the automata. In each step of expansion, we remove the redundancy states and transitions. The on-the-fly degeneralization algorithm is presented in this paper. Compared with the standard degeneralization algorithm, the on-the-fly degeneralization algorithm is a more efficient method. A conversion tool, ltltoba, implements these ideas. Because the resulting automata are smaller during expansion, the algorithm of ltltoba is more efficient. After an extensive empirical test,ltltoba can reduce the running time and the number of states and transitions to some degree.



---

*Source: 516104-2015-02-10.xml*