This thesis proposal is organized as the following.
Chapter 2 shows related work on temporal formulae translation, B¨uchi comple-mentation, and containment testing.
Chapter 3 gives the preliminaries where PTL is introduced in Section 3.2, ω-automata in Section 3.3, and the Manna-Pnueli temporal hierarchy in Section 3.4.
Chapter 4 introduces the proposed incremental translation algorithm for full PTL formulae. The prerequisites are Sections 3.2 and 3.3.
Chapter 5 introduces the optimization heuristics for B¨uchi complementation al-gorithms and a comparative experimentation on the best construction in each com-plementation approach. The prerequisite is Section 3.3.
Chapter 6 introduces an on-the-fly containment testing based on the determinization-based constructions. The prerequisites are Section 3.3 and the improved Safra-Piterman construction introduced in Chapter 5.
Chapter 7 introduces the tools GOAL and B¨uchi Store. The prerequisites are Sections 3.2, 3.3, and 3.4.
Chapter 8 concludes and describes the future work.
Chapter 2
Related Work
We review in this chapter related work on translation of propositional temporal formulae, complementation of B¨uchi automata, and containment testing of B¨uchi automata.
2.1 Translation of Propositional Temporal For-mulae
The traditional automaton construction for a PTL specification works by creating states for every maximally consistent (healthy) sets of subformulae of the specifi-cation. For example, the algorithm in [66], referred to as Tableau here, expands formula ϕ to compute the closure of ϕ, which is then combined with classification rules to create atoms. The edges between atoms are created by the information on every pair of atoms. Next, the accepting states are set according to the promising formulae and fulfilling requirements. Finally, the constructed temporal tableau is converted into a B¨uchi automaton.
Of the same type as Tableau, the algorithm in [52, 50], referred to as Tester here, uses the intermediate structure Fair Discrete System (FDS), a variant of Fair Tran-sition System (FTS). Both of these two algorithms first compute all states (atoms), which contain subformulae of the given PTL formula and then build transitions by
evaluating the information on each states (atoms). The rest is to impose accepting conditions on states. These two algorithms generate large automata because they always create the full state space first, but they are easy to understand.
The algorithm in [49], referred to as IncTableau here, is another tableau con-struction which incrementally creates only reachable states from valid initial states.
The construction starts with an automaton containing a set of initial states and a forged final state, and it then refines the automaton by creating and removing states and transitions until there are no inconsistent transitions. This construction produces smaller automata than Tableau and Tester.
All the above three translation algorithms support full PTL formulae. Tableau and Tester are considered not efficient because they always create full state space first. Although IncTableau constructs the automaton incrementally and supports past operators as well, a global view is maintained such that it cannot be used in truely on-the-fly model checking. Moreover, IncTableau has to fix both forward inconsistencies and backward inconsistencies. A forward inconsistency from a state s to a state t is resolved by computing the satisfactory successors of s as the cover of {f : f ∈ s} ∪ {¬f : ¬ f ∈ s} ∪ t or {f : f ∈ s} ∪ t if the input formula is in negation normal form. However, our algorithm computes satisfactory succes-sors from scratch as the cover of {f : f ∈ s} which contains less formulae than IncTableau. Since only basic formulae are stored in a state under the setting of LTL2AUT, it is earier in our Extended LTL2AUT+ to find a satisfactory successor from existing states and thus result in a smaller automaton.
Subsequently, several incremental algorithms were developed to enable truely on-the-fly model checking. Only reachable states are computed from initial states
during model checking. The automata representing the system, specification, and product can be created as needed during emptiness checking. We will recall three such incremental algorithms using the same convention as [17] to designate the three algorithms.
GPVW is the “simple on-the-fly” algorithm which uses a cover computation based on the tableau rules in Table 3.1 to expand the successors of a state [34]. An im-proved version (GPVW+) is suggested in the same paper. Later on, LTL2AUT [17]
improves GPVW+ by syntactical implication. The difference among these algorithms lies on how information is stored in a state and how contradiction and redundancy are detected during a cover computation. For example, GPVW always stores a pro-cessed formula while LTL2AUT stores only basic formulae. A formula is redundant in GPVW if it has been processed, while in LTL2AUT, it is redundant if it can be syntactically implied by the stored basic formulae.
EQLTL [23] and Wring [86] proceed in three stages, namely formulae rewrit-ing, translation, and optimization. The two constructions both use incremental algorithms as their core translation algorithm, but apply different techniques in the rewriting and optimization stages and actually produce smaller automata. All the above incremental translation algorithms can produce smaller automata than Tableau, Tester, and IncTableau and are faster, but they do not support past operators.
Another kind of translation aims at a two-step translation which translates a PTL formula to an intermediate representation and then converts it into a B¨uchi automaton for model checking. Of this kind, LTL2BA [32] utilizes very-weak alter-nating co-B¨uchi automata (VWAA) and TGBA as its intermediate representations.
s0 = p U✸p− s1 = p p
true
p p
true
Figure 2.1: A two-way very weak alternating automaton equivalent to p U 3p. The− solid transitions go forward while the dashed transition goes backward.
Although a two-step translation is used, LTL2BA can produce even smaller automata than incremental algorithms and is also faster. However, LTL2BA does not support past operators until its authors propose its generalization PLTL2BA.
PLTL2BA uses 2VWAA and TGBA as the intermediate representations. It has the following drawbacks in the conversion from a 2VWAA into a TGBA: (1) the conver-sion is fully automaton-based, and thus it misses the change of using the formulae on the states of the 2VWW to produce smaller TGBA, and (2) the saturation loop in the conversion iterates over the whole set of states currently constructed in the TGBA and thus many consistent states are checked for backward inconsistency dur-ing each iteration even if a timestamp mechanism is used to avoid some redundant computations. Consider the 2VWAA in Figure 2.1 as an example demonstrating the first drawback. During the conversion from the 2VWAA into a TGBA, it may create a state {p U 3p, p} in the TGBA. From the view of PTL formulae, p U− 3p− is implied by p and thus p U 3p can be discarded if p is present. However, from the− view of automata, the conversion is not aware of this simplification.
Both Couvreur’s translation algorithm [16], referred to as Couvreur here, and LTL2BUCHI [35] use transition-based generalized B¨uchi automata (TGBA) as the only intermediate representation. While Couvreur uses BDD to represent an expanded formula and applies prime implicants to simplify the formula, LTL2BUCHI adopts
the core translation algorithm of LTL2AUT. The observation is that when we move labels from states to transitions, two states can be merged if they have the same successors before moving labels. Besides the direct simulation simplification on a TGBA proposed in LTL2BUCHI, several simplification techniques proposed by EQLTL and Wring are also implemented in LTL2BUCHI.
The algorithm proposed by Kesten and Pnueli in [51], denoted by KP02 here, can translate a QPTL formula into a congruent B¨uchi automaton by an inductive construction. In the congruent automaton, a new proposition is introduced to rep-resent the time of the evaluaiton of the formula. A B¨uchi automaton equivalent to the formula is then obtained by taking the intersection of the congruemtn au-tomaton and another B¨uchi automaton where the new proposition is true initially.
This translation algorithm does not deal with2, 2, U , and S formulae but instead− converts these formulae into longer formulae with quantifications, ,3, −, 3, and− negations. For the case of a negated formula, complementation of B¨uchi automata is required. Thus, the algorithm produces large automata in general.
2.2 Complementation of B¨ uchi Automata
Ramsey-based approach. The very first complementation construction intro-duced by B¨uchi in 1960 involves a Ramsey-based combinatorial argument and re-sults in a 22O(n) blow-up in the state size [8]. This construction was later improved by Sistla, Vardi, and Wolper to reach a single-exponential complexity 2O(n2) [83].
In the improved construction, referred to as Ramsey in this paper, the complement is obtained by composing certain automata among a set of B¨uchi automata which form a partition of Σω, based on Ramsey’s Theorem. Various optimization heuris-tics for the Ramsey-based approach are described in [3, 26], but the focus in these
works is on universality and containment. In spite of the quadratic exponent of the Ramsey-based approach, it is shown in [3, 25, 26] to be quite competitive for universality and containment.
Determinization-based approach. Safra’s 2O(n log n) construction is the first complementation construction that matches the Ω(n!) lower bound [77]. Later on, Muller and Schupp introduced a similar determinization construction which records more information and yields larger complements in most cases, but can be under-stood more easily [70, 4]. In [74], Piterman improved Safra’s construction by using a more compact structure and using parity automata as the intermediate determin-istic automata, which yields an upper bound of n2n. (See also [80].) Piterman’s construction, referred to as SP in this paper, performs complementation in stages:
from NBW to DPW, from DPW to complement DPW, and finally from comple-ment DPW to complecomple-ment NBW. The idea is the use of (1) a compact Safra tree to capture the history of all runs on a word and (2) marks to indicate whether a run passes an accepting state again or dies.
Since the determinization-based approach performs complementation in stages, different optimization techniques can be applied separately to the different stages.
For instance, several optimization heuristics on Safra’s determinization and on sim-plifying the intermediate DRW were proposed by Klein and Baier [55].
Rank-based approach. The rank-based approach, proposed by Kupferman and Vardi, uses rank functions to measure the progress made by a node of a run tree towards fair termination [57]. The basic idea of this approach may be traced back to Klarlund’s construction with a more complex measure [54]. Both constructions
have complexity 2O(n log n). There were also several optimization techniques proposed in [39, 27, 48]. A final improvement was proposed recently by Schewe [79] to the construction in [27]. The later construction performs a subset construction in the first phase. In the second phase, it continually guesses ranks from some point and verifies the guesses. Schewe proposed doing this verification in a piecemeal fash-ion. This yields a complement with O((0.76n)n) states, which matches the known lower bound modulo an O(n2) factor. We refer to the construction with Schewe’s improvement as Rank in this paper.
Unlike the determinization-based approach that collects information from the history, the rank-based approach guesses ranks bounded by 2(n − |F |) and results in many nondeterministic choices. This nondeterminism means that the rank-based construction often creates more useless states because many guesses may be verified later to be incorrect.
Slice-based approach. The slice-based construction was proposed by K¨ahler and Wilke in 2008 [47]. The blow-up of the construction is 4(3n)n while its preliminary version in [101], referred to as Slice here, has a (3n)nblow-up1. Unlike the previous two approaches that analyze run trees, the slice-based approach analyzes reduced split trees. The construction Slice uses slices as states of the complement and per-forms a construction based on the evolution of reduced split trees in the first phase.
By decorating vertices in slices at some point, it guesses whether a vertex belongs to an infinite branch of a reduced split tree or the vertex has a finite number of descendants. In the second phase, it verifies the guesses and enforces that accepting states will not occur infinitely often.
1
The construction in [47] has a higher complexity than its preliminary version because it treats
complementation and disambiguation in a uniform way.
The first phase of Slice in general creates more states than the first phase of Rank because of an ordering of vertices in the reduced split trees. Similar to Rank, Slice also introduces nondeterministic choices in guessing the decorations. While Rank guesses ranks bounded by 2(n − |F |) and continually guesses ranks in the second phase, Slice guesses only once the decorations from a fixed set of size 3 at some point.