6.2 Incremental Universality Testing
7.2.1 Features
Automata in B¨uchi Store are grouped into equivalence classes induced by the lan-guages that they recognize. For each equivalence class and each type of automaton, only the three smallest automata known to the Store are kept. Every automaton can be identified by a temporal formula in QPTL [82, 83], of which the well-known LTL is a subset.
The main features of the current Store include:
• Search: The user may find the automata that recognize a particular language by posing a query with an equivalent temporal formula. Formula rewriting based on congruence relations [66, 23] is performed and propositions are auto-matically renamed through unification, to increase matches (semantic match-ing is not attempted online due to its high cost). For instance, a search of q U (q U (q U p)) will get the same results as that of p U q, since q U (q U (q U p)) is equivalent (via the congruence q U (q U p) ≡ q U p) to q U p, which does not
exit in the Store but matches with p U q via unification. An “autocomplete”
feature can suggest to the user formulae that match an incomplete input for-mula up to propositions renaming, as illustrated in Figure 1.1. In the case of B¨uchi automata, the search is like asking for a translation from the tem-poral formula into an equivalent B¨uchi automaton. A big difference is that the answer automata, if present in the Store, are the best among the results obtained from a large number of translation algorithms, enhanced with various optimization techniques such as simplification by simulation [86] or even man-ually optimized (and machine-checked for correctness). If no temporal formula in the Store matches the input, a B¨uchi automaton is generated on demand by taking the best result from several translation and simplification algorithms (without manual optimization). A background process of the Store will later check whether the generated automaton indeed represents a new language and take appropriate actions.
Bounded Existence (p goes from false to true at most twice) 16 Globally (¬p W (p W (¬p W (p W2¬p))))
23 After r 2¬r ∨ 3(r ∧ (¬p W q)) Response Chain (p responds to (q, r))
41 Globally 2(q ∧ 3r → (3(r ∧ 3p)))
Response Chain ((q, r) responds to p) 46 Globally 2(p → 3(q ∧ 3r))
47 Before s 3s → (p → (¬s U (q ∧ ¬s ∧ (¬s U r)))) U s 48 After s 2(s → 2(p → (q ∧ 3r)))
49 Between s and t 2((s ∧ 3t) → (p → (¬t U (q ∧ ¬t ∧ (¬t U r)))) U t)
50 After s until t 2(s → (p → (¬t U (q ∧ ¬t ∧ (¬t U r)))) U (t ∨ 2(p → (q ∧ 3r)))) Constrained Chain Patterns ((q, r) without s responds to p)
51 Globally 2(p → 3(q ∧ ¬s ∧ (¬s U r)))
Table 7.3: The LTL formulae in B¨uchi Store that correspond to those on the Spec Patterns site. We have used lower case for the atomic propositions and in many places changed the proposition names, to make the presentation con-sistent with that of other temporal formulae in the Store. We have also moved Universality forwards to follow Absence, as they are essentially isomorphic.
• Browse: The user may browse the entire collection of automata by having the collection sorted according to number of states, temporal formula length, class in the Temporal Hierarchy [65] illustrated in Figure 3.1, or class on the Spec Patterns site [87] (see Table 7.3). The several sorting keys may be applied in any order as defined by the user using a drag-and-drop interface. Types of automata may be selected via a filter. Possible values of the sorting keys also function as filters for the user to select automata of particular sizes, classes, etc.
B¨uchi Store contains automata and their complements for all of the 55 LTL formulae listed on the Spec Patterns site (with several propositions renamed), which are reproduced in Table 7.3. These automata can be viewed according to their classes in Spec Patterns, by choosing appropriate values of the Spec Patterns filter.
• Upload: The user may upload an automaton for a particular temporal for-mula. The uploaded automaton is checked for correctness, i.e., if it is indeed equivalent to the accompanying temporal formula. If it is correct and smaller than the third smallest automaton of the same type in the Store for the lan-guage specified by the temporal formula, the repository is updated accordingly, keeping only the three smallest automata. Unification is performed to increase the possibility of a match between the uploaded formula and an equivalent but syntactically different formula in the Store, which helps to reduce the number of syntactic variants of automata of essentially the same structure. While clas-sification into the Temporal Hierarchy has been automated, the clasclas-sification for Spec Patterns (whose pattern classes lack a semantically precise charac-terization) has not and, for the moment, simply follows the syntactic form of the formulae listed on the Spec Patterns site. The user may choose to upload an automaton without giving a temporal formula. In this case, a background process of the Store will check whether the automaton belongs to an exist-ing language class in the Store. If the check is positive, the Store will send the user an email (if an email address has been provided) containing a link to the language class where the equivalent temporal formulae, if any, may be found; otherwise, a new language class as defined by the uploaded automaton
is added to the Store and the user is informed of this action.
• Miscellany: There is a shopping cart for the user to collect automata and download them in one single batch. The Store also comes with APIs for tool integration. Through the APIs, a tool can search in the Store for automata that are equivalent to a temporal formula. Propositions renaming of the re-turned automata can be performed by the Store automatically. Finally, a help page explains all of the features.
7.2.2 Use Cases
We describe a number of cases that we expect to represent typical usages of B¨uchi Store.
• Linear-time model checking: The user may shop in the Store for B¨uchi automata that are equivalent (with probable propositions renaming) to the negations of the temporal formulae he wants to verify. The automata may be downloaded in the Promela format for model checking using Spin.
• Benchmark cases for evaluating translation and complementation algorithms: B¨uchi Store has a substantial collection of automata with their equivalent temporal formulae. A subset of the collection may serve as a set of benchmark cases for evaluating translation algorithms. Table 7.5 suggests how such an evaluation may be carried out using the negations of the LTL formulae in Spec Patterns. This use case can certainly be adapted for evaluating B¨uchi complementation algorithms. All B¨uchi automata in the current collection, including those for the LTL formulae in Spec Patterns, have their complements in the Store which are reasonably well optimized. Table 7.6 suggests how such
n B¨uchi Store LTL2AUT [17] Couvreur [16] LTL2BA [32] LTL2Buchi [35] Spin [42]
state tran. state tran. state tran. state tran. state tran. state tran.
1 4 16 10 53 4 25 4 16 5 34 4 25
2 9 144 50 1278 13 440 11 201 11 362 9 289
3 16 1024 179 20153 18 2681 32 2860 19 2906 16 2401
4 25 6400 485 242069 29 18993 50 20686 30 19954 25 16641
5 36 36864 - - 69 203296 - - 59 167545 36 103041
6 49 200704 - - - 49 591361
Table 7.4: A comparison of the results from translating formulae of the form 3(p1∧3(p2∧3(· · ·∧3(pn−1∧3pn) · · ·)))∧3(q1∧3(q2∧3(· · ·∧3(qn−1∧3qn) · · ·))).
Under the title of every column except the first, “state” and “tran.” stand for “num-ber of states” and “num“num-ber of transitions” respectively; “-” indicates out of memory (1 GB) or timeout (1 hour). Implementations of the algorithms here were not op-timized for performance, but were made as faithful as possible to the respective original publications in terms of the structure of the generated automaton. The im-plementation of Couvreur’s algorithm here uses an explicit automata representation and also the conversion algorithm applied in LTL2BA for converting transition-based generalized B¨uchi automata to B¨uchi automata. The implementation of LTL2BA is different from [32] in the definitions of transition relations; however, the results are very close to those in [13] for the same formulae. Except for Spin (over which we do not have control), no optimization was attempted on the input formulae or the result automata.
an evaluation of complementation algorithms may be carried out.
No. B¨uchi Store LTL2AUT [17] Couvreur [16] LTL2BA [32] LTL2Buchi [35] Spin [42]
state tran. state tran. state tran. state tran. state tran. state tran.
1 2 4 3 7 2 5 2 4 2 5 2 5
36 3 30 18 166 5 52 5 42 9 88 8 78
Table 7.5: A comparison of the results from translating the negations of the LTL formulae in Spec Patterns (see Table 7.3). “-” indicates timeout (10 minutes). The notes about the translation algorithms in Table 7.4 also apply here.
No. B¨ uchi Store Safra [77] Piterman [74] Rank-Based [57, 79] Slice-Based [47]
state tran. state tran. state tran. state tran. state tran.
1 2 4 6 18 3 9 2 4 3 6
32 4 44 36 396 13 124 7 60 33 226
33 4 48 16 296 9 148 4 48 8 100
34 5 113 1028 35936 95 3088 16 512 2338 83936
35 4 81 1086 37920 67 2326 13 416 932 31274
36 3 30 8 76 4 40 3 20 4 24
44 5 100 250 8296 232 7276 1558 19355 267 10056
45 5 106 - - 453 14946 10986 117610 -
-46 3 24 13 125 8 77 8 77 9 72
47 4 47 22 404 11 168 5 60 11 140
48 4 62 21 480 7 148 6 98 7 108
49 5 126 43 1760 11 396 5 160 38 1160
50 9 248 868 31328 171 5082 1098 15292 840 30607
51 3 48 13 222 14 226 7 126 13 192
52 4 93 30 1000 13 368 7 152 23 520
53 4 118 21 960 7 311 6 181 7 208
54 5 250 57 4672 13 920 7 448 60 3664
55 13 594 634 45888 73 4904 219 8286 616 38171
Table 7.6: A comparison of the results from complementing the automata for the LTL formulae in Spec Patterns (see Table 7.3). “-” indicates timeout (10 minutes). The implementations of complementation algorithms here follow the respective original publications as faithfully as possible without applying any other additional optimization to the input automata or to the resulting complements. Naive conversions from Streett automata and parity automata to B¨uchi automata are applied in Safra and Piterman. For Slice-Based, the transition relation of an input automaton is made complete, as required by the original algorithm, before complementation.
• Classification of temporal formulae: The look of a temporal formula may not tell immediately to which class it belongs in the Temporal Hierarchy.
It should be educational to practice on the cases that do not involve going through complicated operations on automata. For example, 2p ∨ 2q is a safety formula because it is equivalent to 2(2p ∨− 2q) in the canonical safety− form (where 2 means “so-far” or “always in the past”). Another formula− 2(p → 3q) is a recurrence formula because it is equivalent to 23(¬p B q) (where B means “back-to”, the past version of “wait-for” or “weak until”).
• Reverse lookup of temporal formulae from automata: The option of uploading an automaton without giving a temporal formula may be used to find temporal formulae that are equivalent to a given automaton if some equiv-alent automaton with temporal formulae is present in the Store. There is no guarantee of success. However, as the collection of automata and temporal for-mulae in the Store continues to grow, the success rate of such reverse lookups should increase accordingly.
• Synthesis: Deterministic parity automata are widely used in the synthesis of a reactive system that satisfies desired specifications expressed in linear tem-poral logic. For example, the quantitative synthesis tool, QUASY [12], takes as qualitative specifications deterministic parity automata in the GOAL file format (GFF). Thus, the user may shop in the Store for the deterministic par-ity automata that are equivalent (with probable propositions renaming) to the temporal formulae to be satisfied by the system, rename propositions properly perhaps with the help of the GOAL tool, and then perform the synthesis.
• Tool Integration Here is a simple use case of the APIs for tool integration.
Suppose the user of a model checker wants to verify if a system satisfies the temporal logic formula 2(request → 3response). Instead of translating the formula into an equivalent automaton by a translation algorithm, the model checker can request equivalent automata from the Store. Since the Store con-tains automata equivalent to 2(p → 3q), propositions of these automata will be renamed by the Store such that the returned automata are exactly equiv-alent to the required formula.
7.2.3 Implementation Details
We describe below in more details the basic infrastructure of B¨uchi Store, the search features of propositions renaming and autocomplete, a procedure for classification into the Temporal Hierarchy based on deterministic B¨uchi automata, and a “contain-ment partial order” that is helpful in calculating equivalence classes incre“contain-mentally.
• Basic Infrastructure: The basic client-server interactions in accessing the Store are realized by customizing the CodeIgniter [15], which is an open-source Web application framework written in PHP. To perform automata and tem-poral formulae-related operations, such as equivalence checking and formula to automaton translation, the Store relies on the GOAL tool [94] and its re-cent extensions. To achieve better performance, the Store does not invoke the GOAL tool every time an automata or temporal formulae-related operation is needed. Instead, the Store interacts with a single GOAL process hosted on a Tomcat application server [90] via PHP/Java Bridge [73].
• Propositions Renaming: The formulae search with propositions renaming increases matches such that for example 2(p → 3q) in the Store can be found even if the queried formula is 2(request → 3response). This feature is achieved by formulae normalization which renames the propositions of a formula uniformly based on the order of propositions in the parse tree of the formula such that the i-th new proposition is renamed to aux i. When searching for a formula, both the original formula entered by the user and its normalization will be used to find matches. For example, 2(p → 3q) has the normalized formula 2(aux1 → 3aux2 ) stored in the internal database. Since 2(request → 3response) has the same normalized formula, 2(p → 3q) can
I ::= C | ◦u | ◦u I | C ◦b | C ◦b I | • | •X | •X I | ( | ( I C ::= X | ◦u C | C ◦b C | •X C | ( C )
◦u ::= ¬ | |3 | 2 | − | ∼ | 3 |− 2−
◦b ::= ∧ | ∨ | → | ↔ | U | W | R | S | B
• ::= ∃ | ∀
Figure 7.9: The syntax of incomplete formulae I and complete formulae C where X is the set of atomic propositions.
be easily found.
• Autocomplete: The formulae search with autocomplete makes suggestions about formulae that may match an incomplete formula queried by the user.
For example, 2(p → p), 2(p → 3q), 2(p → 3q), etc. will be suggested to− the user when the incomplete formula “2(request →” is entered in the search field. This feature is achieved by parsing incomplete formulae and formulae normalization. Due to the proposition order of the formulae normalization, the syntax of incomplete formulae is restricted to the form shown in Figure 7.9 such that only the rightmost leaves of the parse tree may be missing.
• Classification: The classification of automata and temporal formulae into the Temporal Hierarchy may be performed by the approach in [65] through deterministic Streett automata, which was adopted by an earlier version of B¨uchi Store. The Store now performs the classification in a different way through deterministic B¨uchi automata. Consider a B¨uchi automaton A and its complement A. A belongs to the Recurrence (Response) class if the lan-guage of A can be recognized by a deterministic B¨uchi automaton B [61]. The deterministic B¨uchi automaton B can be constructed by the approach in [61]
through deterministic Muller automata or by the approach in [6] through
de-terministic co-B¨uchi automata3. A belongs to the Persistence class if A is in the Recurrence class. A is in the Reactivity class if it belongs to neither the Recurrence class nor the Persistence class, and A is in the Obligation class if it belongs to both the Recurrence class and the Persistence class. A belongs to the Safety class if the language of B is prefix-closed, which can be verified by checking that all accepting runs stay only in accepting states after maximizing the B¨uchi acceptance set of B without changing the recognized language [91].
In the maximization of a B¨uchi acceptance set, a state s becomes accepting if every cycle containing s also contains some accepting state. Finally, A belongs to the Guarantee class if A belongs to the Safety class.
• Containment partial order: Automata in B¨uchi Store are stored per language-equivalence class for consistency and for saving disk space. The grouping of automata and temporal formulae into equivalence classes is performed offline in batches because equivalence checking is time-consuming. Suppose there are n equivalence classes C1, C2, . . . , Cn in the Store when a new automaton A is considered. Let Bi ∈ Ci, for 1 ≤ i ≤ n, be the representative automata of the equivalence classes. A naive grouping procedure may check for every equivalence class Ci if A is equivalent to Bi and, if it is the case, add A to Ci. To accelerate the grouping, B¨uchi Store keeps a “containment partial order”4
3
The main construction in [6] may be used to obtain a DCW from A that is either exactly equivalent to A if A is DCW-recognizable or an over-approximation of A. We check the equivalence between the constructed DCW and A to see which case it is. If it is the former case, then the DCW equivalent to A can be easily complemented to get a DBW that is equivalent to A, affirming that A belongs to the Recurrence class.
4
The containment partial order maintained in the Store is a (very small) portion of the lattice
of ω-regular languages over a finite alphabet (of boolean combinations of atomic propositions,
determined by the automaton with the most number of atomic propositions) where the partial
order is language containment and the meet and join are respectively the intersection and union of
sets. The maintained portion itself may not be a lattice and rather is just a succinct representation
of the containment relation between the languages/automata in the Store.
of the equivalence classes. If A 6⊆ Bi, then every equivalence class Cj such that Bj ⊆ Bi need not be checked. Similarly, if Bi 6⊆ A, then every equivalence class Cj such that Bi ⊆ Bj need not be checked.
7.3 Summary of this Chapter
We have described GOAL, a graphical interactive tool designed for ω-automata and temporal logics. As the source “Graphical Tool for Omega-Automata and Logics”
of the acronym GOAL suggests, our long-term goal is for the tool to handle the common variants of ω-automata and the logics that are expressively equivalent to these automata. For example, besides B¨uchi and generalized B¨uchi automata, we have extended GOAL to support the editing of and a limited set of direct operations on Muller, Rabin, Streett, and parity automata [36], as well as alternating automata and two-way alternating automata. Although these variants of ω-automata do not necessarily have a direct impact on the model-checking process, they are powerful intermediaries for the development of automata-based algorithms and will make GOAL complete as a learning and teaching tool.
We have also described B¨uchi Store, a Web-based repository that contains a large and expanding collection of B¨uchi automata and other types of ω-automata. Every automaton in the current collection is described by at least one temporal formula and can be easily searched.5 With various options for sorting and filtering, browsing the collection is also fairly convenient to do.
B¨uchi Store appears to be unique in the features that it provides. When only B¨uchi automata are of concern, the most closely-related tool perhaps is the Web
5
This may no longer be true when a user uploads an automaton without a temporal formula
such that the automaton defines a new language.
version of LTL2BA [31]. LTL2BA provides several algorithms for translating a temporal formula into a B¨uchi automaton and several options for optimizing the automaton during or after the translation. Translation is performed online there. It is left for the user to try out different combinations of the algorithms and options to generate the best result. In contrast, B¨uchi Store provides a single access point for the user to get the best known B¨uchi automata for a temporal formula. No translation is performed online here, except in the case that no syntactic match for the temporal formula is found. A manually-optimized automaton may be uploaded and checked for correctness (with respect to the given temporal formula). It can be smaller than any machine-translated automaton. Another advantage of B¨uchi Store is that past temporal operators are supported.
Chapter 8 Conclusion
The automata-theoretic approach to model checking has been developed for near three decades. Because of its proven effectiveness and ease of use, the approach has been a viable alternative to testing and simulation in industry. In this approach, translation of temporal formulae, complementation of B¨uchi automata, and contain-ment testing of B¨uchi automata play important roles. A more efficient translation, complementation, or containment testing can make the model checking process faster in general.
8.1 Contributions
In this dissertation, we make the following contributions.
• Improved translation algorithms for PTL formulae: A backtrace procedure is proposed to extend both state-based and transition-based incremental algo-rithms to support past operators. Two optimization heuristics are also pro-posed to produce smaller automata.
• Improved complementation constructions for B¨uchi automata: Two optimiza-tion heuristics are proposed for the Safra-Piterman construcoptimiza-tion. One op-timization heuristic is proposed for the rank-based construction and is also
applicable to other constructions. Three optimization heuristics are proposed for the slice-based construction.
• An incremental containment testing algorithm based on the determinization-based approach.
• Comparative experimentation on complementation constructions, on transla-tion algorithms for PTL formulae, and on containment testing algorithms.
• Two tools, namely GOAL and B¨uchi Store, which can provide an environment for education and research on ω-automata and temporal logics.