基於自動機理論的模型檢測演算法與工具之改善

(1)

國立臺灣大學管理學院資訊管理學研究所博士論文

Department of Information Management College of Management

National Taiwan University Doctoral Dissertation

基於自動機理論的模型檢測演算法與工具之改善 Improved Algorithms and Tools for

Automata-Theoretic Model Checking

蔡明憲 Ming-Hsien Tsai

指導教授：蔡益坤博士、王柏堯博士

Advisers: Yih-Kuen Tsay, Ph.D., Bow-Yaw Wang, Ph.D 中華民國102年7月

July 2013

(2)

論

論論文文文摘摘摘要要要

以自動機理論為基礎的模型檢測方法已經發展近三十年，此方法被認為具有效率且容易使用，在確保軟體或硬體設計的正確性上，已成為業界測試與模擬之外的另一項選擇。在這個方法中，一個待測的系統會用一個B¨uchi自動機來表示，而系統所需滿足的規格則用一個線性時態邏輯（PTL）式來表示。在線性時態邏輯中，比較常用到的是只能描述未來的版本（LTL）。此方法首先將規格的否定轉換成一個B¨uchi自動機，然後和表示系統的自動機作交集，最後測試交集部分是否不接受任何行為。在這些步驟中，時態邏輯式的轉換扮演一個重要的角色，因為一般來說，轉換出來的自動機越小，則與系統的交集也越小，而模型檢測可以比較快完成。雖然目前已經有很多LTL轉換演算法，然而在其他時態邏輯的部分，

仍有改善的空間，例如比LTL更容易書寫較短規格的PTL。

系統規格也可以直接用B¨uchi自動機來表示，在某些情況下會比時態邏輯式更自然與直接。如此一來，在與系統自動機作交集之前，需要先計算規格自動機的

補集。B¨uchi自動機的補集計算與有限字串長度的傳統自動機相比更加複雜許多，

所以一些最佳化方法對補集計算的效能與效率有很大的幫助。因為B¨uchi 自動機

補集的高複雜度，最近許多研究都跳往不需完整建置補集的漸進式行為包含測

試。在行為包含測試中，以Ramsey理論為基礎的方法已被證明相當有效率，不過

在補集計算的部分卻相當不具競爭力，反而確定性方法是最好的。同樣地，為了加速模型檢測，我們除了改進時態邏輯轉換演算法之外，也可以改進補集計算與包含測試的演算法。

在時態邏輯轉換的部分，我們改善了五個漸進式演算法，利用一個回朔的程

序讓這些演算法可以支援過去時態運算子，同時保持漸進式轉換的好處。對於

狀態基礎演算法中的涵蓋計算程序，我們也利用質含項（Prime Implicant）加以

改善。此外，我們也實作了過去與未來的分離程序，使得一個PTL式子可以被

轉換成另一個相等的LTL式子，然後再利用目前最有效率的LTL轉換演算法（例如LTL2BA或是LTL3BA）來轉換。這使得我們可以比較我們所改善的演算法，以及目前最有效率的LTL轉換演算法。

在B¨uchi補集計算的部分，我們審視四個主要方法，並透過實驗加以比較。雖然傳統的看法是非確定性方法比確定性方法更好，因為非確定性方法有比較低的理論複雜度。然而我們的實驗顯示在B¨uchi補集計算中，確定性方法是最好的。此外，我們也對其中三個方法提出數個改善的點子，使得這三個方法的效率與效能大為改善。

在包含測試中，我們提出一個基於確定性方法的漸進式包含測試演算法。雖然確定性方法的執行一般被認為需要分離成幾個階段，不過我們展示這些階段其實可以合併成一個，而且可以被漸進式地執行。實驗顯示包含關係成立時，

我們的方法比以Ramsey理論為基礎的方法來得好。不過包含關係不成立時，

以Ramsey理論為基礎的方法卻比我們的方法來得好。

最後，我們要應付的問題是自動機與時態邏輯在教育與研究的工具支援。雖然目前已有許多以自動機理論為基礎的模型檢測工具，不過都沒有支援自動機或時態邏輯式視覺化呈現與操作。這激發了我們的第一個工具：GOAL，第一個可以用來學習無限自動機與時態邏輯的視覺化互動工具。除此之外，GOAL也提供功能幫助研究學者開發和測試新演算法、執行實驗、與收集統計資料。除了GOAL以外，我們還建制一個網頁形式的工具：B¨uchi Store。這個工具是許多

常見時態邏輯式與其最小相等自動機的集合，可以被搜尋、瀏覽與擴展。這樣的

集合不僅可以當成一個最佳時態邏輯式轉換演算法，同時也可以作為實驗的比較基礎。GOAL與B¨uchi Store已經幫助我們開發許多改進的演算法，讓模型檢測更

(3)

加快速。我們相信這兩個工具可以提供研究學者一個好的平台，幫助未來開發相關演算法與進行實驗。

(4)

ABSTRACT

Improved Algorithms and Tools for Automata-Theoretic Model Checking

by Ming-Hsien Tsai

Graduate Institute of Information Management National Taiwan University

Advisers: Yih-Kuen Tsay, Ph.D. and Bow-Yaw Wang, Ph.D.

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 become a viable alternative to testing and simulation in industry. In the approach, a system is typically represented by a B¨uchi automaton, while a specification is encoded by a formula in propositional linear temporal logic (PTL), of which the future fragment (usually referred to as LTL) is more often used. The approach proceeds by translating the negation of the formula to a B¨uchi automaton, which is later intersected with the system automaton for testing emptiness. Such translation plays an important role in the approach because in general, the smaller the negated- specification automaton is, the sooner the model checking process may be completed.

Although there has been a long line of research on LTL translation algorithms aiming to produce smaller automata, there are still opportunities of improving translation algorithms for other temporal logics such as PTL, which is expressively more succinct than LTL.

Specifications may also be directly encoded by Büchi automata which in certain cases are more natural and easier than temporal formulae. In such cases, complementation of a specification automaton is performed before taking the intersection with the system automaton. The complementation of Büchi automata is significantly more complicated than that of classic finite automata on finite words. Opti- mization heuristics are critical to good performance. Due to the high complexity of Büchi complementation, much recent emphasis has been shifted to containment testing without constructing the complement. The Ramsey-based approach has been proven to be quite effective in such containment testing, although it is not competitive in complementation where the determinization-based approach is the best in general. Again, to expedite the model checking process, we can improve not only the translation algorithm but also the complementation algorithm and the containment testing algorithm.

For translation of temporal formulae, we extend five existing incremental algorithms with a backtrace procedure to support past operators of PTL, while maintaining the advantages of incremental automata construction. The cover computation

(5)

common to the state-based incremental algorithms is improved based on prime implicants to obtain smaller automata. Besides, we also implement the separation of past and future separators. The separation procedure can convert a PTL formula to an equivalent LTL formula, which can later be translated by an efficient LTL translation algorithm such as LTL2BA or LTL3BA. This allows us to compare our extended algorithms with those existing efficient LTL translation algorithms.

For B¨uchi complementation, we review four approaches and perform a comparative experimentation on the best construction in each approach. Although the conventional wisdom is that the nondeterministic approaches are better than the deterministic approach because of better worse-case bounds, our experimental results show that the deterministic construction is the best for complementation in general. We also propose optimization heuristics for three of the four best constructions. Our experiment shows that the optimization heuristics substantially improve the three constructions.

For containment testing, we propose an incremental containment testing approach based on the determinization-based constructions, of which Safra-Piterman construction is the best in B¨uchi complementation. Although the determinization- based constructions are typically performed in stages, we show that the stages can be merged such that the containment testing can be performed incrementally. Our experimental results show that for cases where the containment relation holds, our incremental Safra-Piterman approach is much better then the Ramsey-based approach. For other cases where the containment relation does not hold, the Ramsey- based outperforms our incremental Safra-Piterman approach.

Finally, we address the issue of tool support for education and research on ω-automata and temporal logics. Although there are various tools for automata- theoretic model checking, none of the tools provide facilities for visually manipulating automata and temporal formulae. This motivated our GOAL tool, which is the first interactive graphical tool for learning ω-automata and temporal logics. Besides, GOAL also provides facilities for helping researchers develop and test new algorithms, perform experiments, and collect statistical data. We also build a Web-based tool called B¨uchi Store, which is an extensible collection of temporal formulae and their equivalent automata. Such a collection can be used not only as a new translation tool that always returns the smallest automata available but also as benchmark cases for experiments. Both GOAL and B¨uchi Store already helped us develop our improved algorithms, which expedite the model checking process.

We believe the two tools provide researchers with a good environement for future development and experimentation of related algorithms.

(6)

List of Figures

1.1 Main page of B¨uchi Store and search of 2(request → 3response) in

progress. . . 12

2.1 A two-way very weak alternating automaton equivalent to p U 3p. . . 19⁻

3.1 The Manna-Pnueli Temporal Hierarchy. Here p, q, p_i, and q_i are past temporal formulae. DCW stands for deterministic co-B¨uchi (word) automaton. . . 31

4.1 Part of an intermediate result of translating 2(p → ⁻(q U r)). . . 38

4.2 Part of an intermediate result of translating 2(p → ⁻(q U r)) after the first backtrace . . . 38

4.3 The NTGW produced by Couvreur for 3p . . . 49

4.4 A comparison of translation algorithms based on the number of timeouts 53 4.5 A comparison of translation algorithms based on the average state size 53 5.1 An NBW where the alphabet is {p, ¬p}, the initial state is q₀, and the acceptance condition is {q1} . . . 66

5.2 Examples of a split tree and a reduced split tree . . . 66

5.3 A decorated reduced split tree of the NBW in Figure 5.1 on the rejected word (p¬p)^ω . . . 67

5.4 The decoration rules D1, D2, D3, and D4 applied in the basic Slice construction. . . 68

7.1 An example of drawing a B¨uchi automaton with GOAL. . . 98

7.2 An example of testing a B¨uchi automaton on a word with GOAL. . . 100

7.3 A screen shot of the step-by-step translation of a temporal formula into an equivalent generalized B¨uchi automaton using the Tableau algorithm. . . 101

7.4 A demonstration of the automaton simplification. . . 103

7.5 The stages in complementing a B¨uchi automaton by Safra’s construction. . . 106

7.6 A safety formula and its equivalent canonical formula. . . 109

7.7 Automata intended for “Even p”; the one in (a) is incorrect. . . 111

7.8 The structure of GOAL . . . 113

7.9 The syntax of incomplete formulae I and complete formulae C where X is the set of atomic propositions. . . 123

(9)

List of Tables

3.1 Tableau rules. . . 27 4.1 Five selected formulae for a comparison of translation algorithms . . . 54 4.2 Comparison of six translation algorithms without and with simplifi-

cations in [86, 24] applied to the final B¨uchi automata based on the five formulae in Table 4.1. The top 5 formulae are without simplification and the bottom 5 are with simplification. A “-” indicates that the algorithm cannot finish the translation in 10 minutes. A “*”

indicates that the algorithm runs out 1 GB memory. . . 54 5.1 A comparison of the four representative complementation construc-

tions based on A15 . . . 57 5.2 A comparison of the four representative complementation construc-

tions based on the nonuniversal automata in A¹⁵ . . . 58 5.3 A comparison of each complementation construction with its im-

proved versions . . . 76 5.4 A comparison of the four improved complementation constructions

based on A¹⁵ without and with preminimization . . . 78 5.5 A comparison of the four improved complementation constructions

based on the nonuniversal automata in A15 without and with preminimization . . . 78 5.6 A comparison of the four representative complementation construc-

tions based on A10, A15, and A20. . . 80 5.7 A comparison of the four representative complementation construc-

tions based on the nonuniversal automata in A10, A15, and A20 . . . . 81 5.8 A comparison of the four improved complementation constructions

based on A10, A15, and A20 . . . 83 5.9 A comparison of the four improved complementation constructions

based on A¹⁰, A¹⁵, and A²⁰ with preminimization . . . 84 5.10 A comparison of the four improved complementation constructions

based on the nonuniversal automata in A10, A15, and A20 . . . 85 5.11 A comparison of the four improved complementation constructions

based on the nonuniversal automata in A¹⁰, A¹⁵, and A²⁰ with preminimization . . . 85 6.1 Comparing three containment testing approaches in terms of running

time based on 600 pairs of automata. The time unit is millisecond.

OOM means that the approach runs out of memory. . . 93

(10)

7.1 Major algorithms in GOAL. The Modified Safra algorithm for complementation is a slight variation of Safra’s construction. . . 97 7.2 Boolean and temporal operators supported in GOAL and their input

formats. . . 99 7.3 The LTL formulae in B¨uchi Store that correspond to those on the

Spec Patterns site. . . 115 7.4 A comparison of the results from translating formulae of the form

3(p¹∧3(p²∧3(· · · ∧ 3(pⁿ⁻¹∧3pⁿ) · · ·))) ∧3(q¹ ∧3(q²∧3(· · · ∧ 3(qⁿ⁻¹∧3qⁿ) · · ·))). . . 118 7.5 A comparison of the results from translating the negations of the LTL

formulae in Spec Patterns . . . 119 7.6 A comparison of the results from complementing the automata for

the LTL formulae in Spec Patterns . . . 120

(11)

Chapter 1 Introduction

The automata-theoretic approach to model checking has been developed for near three decades [102]. Because of its proven effectiveness and ease of use, the approach has been a viable alternative to testing and simulation in industry. In the approach, a system is typically represented by a Büchi automaton M , while a specification is encoded by a formula f in propositional linear temporal logic (PTL), of which the future fragment (usually referred to as LTL) is more often used. Given a Büchi automaton B, L(B) captures the behavior accepted by the automaton B. The system M satisfies the specification f if L(M × A¬f) = ∅ where M × A¬f is the intersection of M and A¬f, and A¬f is a Büchi automaton obtained by translating the negation of the specification formula. Such translation plays an important role in the approach because in general, the smaller the negated-specification automaton is, the sooner the model checking process may be completed. Although there has been a long line of research on LTL translation algorithms aiming to produce smaller automata, there are still opportunities of improving translation algorithms for other temporal logics such as PTL, which is expressively more succinct than LTL [62].

Specifications may also be directly encoded by B¨uchi automata, a type of ω- automata, which in certain cases are more natural and easier than temporal formu-

(12)

lae. In such cases, a system M satisfies a specification encoded by a Büchi automaton A if L(M × A) = ∅ where A is the complement of A. The complementation of Büchi automata is significantly more complicated than that of classic finite automata on finite words. Optimization heuristics are critical to good performance. Due to the high complexity of Büchi complementation, much recent emphasis has been shifted to containment testing without constructing the complement [20, 25, 3, 1]. Again, to expedite the model checking process, we can improve not only the translation algorithm but also the complementation algorithm and the containment testing algorithm.

In this thesis, we focus on improving translation of temporal formulae, complementation of B¨uchi automata, and incremental containment testing. We also address the issue of tool support for education and research on ω-automata and temporal logics.

1.1 Translation of Temporal Formulae

The traditional automaton construction [66] for a PTL specification formula works by building a tableau with the full state space; that is, it creates states for every maximally consistent (healthy) sets of subformulae of the specification formula. It then adds transitions according to subformulae information on each state. This kind of constructions can be easily understood, but they are clearly not suitable for practice as they reach the worst case bound every time.

This obvious drawback motivated incremental algorithms [34, 17] which do not generate the whole tableau at once, but rather start from the initial states and build the state transition graph incrementally. The incremental generation permits truely on-the-fly model checking in that the intersection automaton (of the system and the

(13)

negated specification) is constructed from the initial states and expanded one step further only if no accepting word is found by examining the intersection automaton constructed so far. On-the-fly model checking therefore can find a counterexample early without generating the whole intersection automaton. Besides, a state (a set of subformulae) in the tableau can be represented symbolically such that the translated automaton is even smaller. Though current practice of on-the-fly model checking generates the entire specification automaton before constructing the intersection automaton, the incremental translation algorithms are still preferred, as they in general produce smaller automata. These algorithms are the kernel of temporal formulae to B¨uchi automata translation in the well-known model checker Spin [42]. Unfortu- nately, these incremental algorithms cannot be applied to formulae containing past operators.

It has been shown that PTL and LTL have the same expressive power [29, 30]. However, adding past operators brings additional expressivity from a practical view [64]. For example, it is easy to state that “only event q can trigger a series of event p in the next time” in PTL as2(p → (p S q)). This specification formula with a past operator is easy to understand and to write, but it is not the case in LTL.

The equivalent formula in LTL is2(p ∨ ((¬p) W q)) ∧ ((¬p) W q), where (¬p) W q appears twice. Moreover, in [62], it has been proven that PTL can be exponentially more succinct than LTL.

To support past operators while attempting to maintain efficiency, the two-step algorithm by Gastin and Oddoux [33] generalized the efficient translation algorithm LTL2BA [32]. The generalized algorithm, referred to as PLTL2BA, uses two-way very weak alternating co-B¨uchi automata (2VWAA) and transition-based generalized

(14)

B¨uchi automata (TGBA, where the acceptance condition is imposed on transitions) as the intermediate representations. However, the transition relation of a TGBA in PLTL2BA is not defined in a conventional way. If one uses a more conventional representation of automata, the size of the TGBA produced by PLTL2BA will be as large as 2ⁿ⁺¹× 2ⁿ⁺¹ states where n is the number of temporal subformulae of the input PTL formula. Besides, PLTL2BA has the following two drawbacks during the conversion from a 2VWAA into a TGBA. The first drawback is that the conversion is fully automaton-based, and thus it misses the chance to simplify the TGBA based on the formulae in the states of the 2VWAA. The second drawback is that the saturation loop in the conversion iterates over the whole set of states currently constructed in the TGBA. Even if a timestamp mechanism is used to avoid some redundant computations, the algorithm still spends time in checking the backward consistency between many consistent states.

In this thesis, we propose a PTL translation algorithm, which extends the incremental algorithms with a backtrace procedure to support past operators, while maintaining the advantages of incremental automata construction. The backtrace is only performed when a backward inconsistency is found. The cover computation common to those state-based incremental algorithms is improved based on prime implicants to obtain smaller automata. We have implemented the extended incremental algorithms in the GOAL tool. Experimental results show that one of the extended algorithms produces in most cases smaller automata than other algorithms that support past operators. Besides, we have also implemented the separation of past and future operators proposed by Gabbay [29] (with adaptation since the def- inition of temporal operators differs). The separation procedure can convert a PTL

(15)

formula to an equivalent LTL formula, which can later be translated by an efficient LTL translation algorithm such as LTL2BA or LTL3BA. This allows us to compare our extended algorithms with those existing efficient LTL translation algorithms.

The experimental results show that our extended algorithms perform much better than LTL translation algorithms plus the separation procedure.

1.2 Complementation of B¨ uchi Automata

B¨uchi automata are nondeterministic finite automata on infinite words. They recognize ω-regular languages and are closed under Boolean operations, namely union, intersection, and complementation. The formalism was first proposed and stud- ied by B¨uchi in 1960 as part of a decision procedure for second-order logic [8].

Complementation of Büchi automata is significantly more complicated than that of nondeterministic finite automata on finite words. Given a nondeterministic finite automaton on finite words with n states, complementation yields an automaton with 2ⁿ states through the subset construction [75]. Indeed, for nondeterministic Büchi automata, the subset construction is insufficient for complementation. In fact, Michel showed in 1988 that blow-up of Büchi complementation is at least n!

(approximately (n/e)ⁿ or (0.36n)ⁿ), which is much higher than 2ⁿ [69]. This lower bound was later sharpened by Yan to (0.76n)ⁿ [103], which was matched by an upper bound by Schewe [79].

There are several applications of B¨uchi complementation in formal verification.

For example, whether a system satisfies a property can be verified by checking if the intersection of the system automaton and the complement of the specification automaton is empty [98]. Another example is that the correctness of an LTL translation algorithm can be tested with a reference algorithm [39]. Although recently

(16)

many works have focused on universality and containment testing without going explicitly through complementation [20, 25, 3, 1], it is still unavoidable in some cases [58].

There have been quite a few complementation constructions, which can be classified into four approaches: Ramsey-based approach [8, 83], determinization-based approach [77, 70, 4, 74], rank-based approach [89, 57, 54], and slice-based approach [47, 101]. The second approach is a deterministic approach while the last two are nondeterministic approaches. The first three approaches were reviewed in [100]. Due to the high complexity of B¨uchi complementaton, optimization heuristics are critical to good performance [39, 27, 79, 48, 55]. However, with much recent emphasis shifted to universality and containment, empirical studies of B¨uchi complementation have been scarce [55, 39, 48, 94] in contrast with the rich theoretical developments. A comprehensive empirical study would allow us to evaluate the performance of these complementation approaches that has so far been characterized only by theoretical bounds.

In this thesis, we review the four complementation approaches and perform comparative experimentation on the best construction in each approach. Although the conventional wisdom is that the nondeterministic approaches are better than the deterministic approach because of better worse-case bounds, our experimental results show that the deterministic construction is the best for complementation in general.

At the same time the Ramsey-based approach, which is competitive in universality and containment testing [3, 25, 26], performs rather poorly in our complementation experiments. We also propose optimization heuristics for the determinization-based construction, the rank-based construction, and the slice-based construction. Our

(17)

experiment shows that the optimization heuristics substantially improve the three constructions. Overall, our work confirms the importance of experimentation and heuristics in studying B¨uchi complementation, as worst-case bounds may not be accurate indicators of performance.

1.3 Incremental Containment Testing

Model checking a system against a specification can be performed in another way by testing if the behavior of the system is contained in the behavior allowed by the specification without taking the complementation of the specification. Recently, there were many works focus on universality and containment testing based on the Ramsey-based approach and the rank-based approach without going explicitly through complementation [25, 26, 21, 3, 1, 2]. Among the existing approaches, the Ramsey-based approach is shown to be quite competitive [3, 25, 26].

Although the Ramsey-based approach is competitive in universality and containment testing, it performs rather poorly in our complementation experiments, which show that the determinization-based approach is the best for complementation in general. It is then interesting to see the comparison of the determinization-based approach and the Ramsey-based approach in containment testing.

The determinization-based approach is typically performed in three stages: determinizing a B¨uchi automaton into a deterministic automaton with another acceptance condition, complementing the deterministic automaton, and converting the complement into a B¨uchi automaton. Such three-stage complementation has an advantage of applying various optimizations in each stage but is considered not suitable for incremental containment testing. In fact, the three stages of the determinization- based approach can be merged. On the one hand, this makes us able to perform

(18)

incremental containment testing based on the determinization-based approach. On the other hand, optimization heuristics for complementation may become inappli- cable.

In this thesis, we propose an incremental containment testing approach based on the determinization-based approach. We also compare our determinization-based approach with the Ramsey-based approach and the naive approach that takes a full complement first, then intersection, and finally an emptiness test. The experimental results showed that the Ramsey-based approach performs much better than the incremental determinization-based approach and the naive approach in the cases where the containment relation holds but rather poorly in all other cases. The incremental determinization-based approach performs much better than the naive approach when the containment relation does not hold but worse than the naive approach when the containment relation holds.

1.4 Tool Support

Besides of improved algorithms for model checking, we also address the issue of tool support for education and research on ω-automata and temporal logics. Two tools, namely GOAL and B¨uchi Store, are built for this purpose.

1.4.1 GOAL

The acronym GOAL¹ was originally derived from “Graphical Tool for Omega- Automata and Logics”. It also stands for “Games, Omega-Automata, and Logics”.

The main functions of GOAL include (1) drawing ω-automata, alternating automata, two-way alternating automata, and games, (2) testing and converting ω-

1

The tool is available at http://goal.im.ntu.edu.tw/.

(19)

automata, (3) determinizing and complementing Büchi automata by various algorithms, (4) checking the language equivalence and containment between two ω- automata, (5) simplifying Büchi automata by various simulation relations, (6) translating QPTL (Quantified Propositional Temporal Logic) [83] formulae directly or step-by-step into equivalent Büchi automata by various algorithms, (7) exporting Büchi automata as Promela code, (8) generating random ω-automata and PTL formulae, (9) solving reachability, Büchi, and parity games.

GOAL was originally designed with a graphical interface for learning and teach- ing Büchi automata and linear temporal logics. As shown in [83], Büchi automata and QPTL are expressively equivalent, though translation between the two for- malisms is highly complex [51]. For PTL, practically feasible algorithms exist for translating a PTL formula into an equivalent Büchi automaton [49, 34, 17, 32], though not vice versa. Despite the possibility of mechanical translation, a temporal formula and its equivalent Büchi automaton are two very different artifacts and their correspondence is not easy to grasp. Temporal formulae describe temporal dependency without explicit references to time points and are in general more abstract, while Büchi automata “localize” temporal dependency to relations between states and tend to be of lower level. Understanding their relation is instrumental in dis- covering algorithmic solutions to model checking problems or simply in using those solutions, e.g., specifying a temporal property directly by an automaton rather than a temporal formula so that the property can be verified by an algorithm that op- erates on automata. To enhance this understanding, it helps to go through several translation algorithms with different input temporal formulae or simply by examining more examples of temporal formulae and their equivalent Büchi automata. This

(20)

learning process, however, is tedious and prone to mistakes for the student, while preparing the material is very time-consuming for the instructor. Tool support is needed.

Moreover, in model checking a system M against a specification f in temporal logic, as the emptiness checking of M × A¬f requires time proportional to the size of the system automaton M and to that of the specification automaton A¬f, a larger A¬f would mean a longer verification time. To reduce verification time, it may be worthwhile to construct a smaller A¬f manually. But a way for checking the correctness of a user-defined A¬f is needed. With various translation algorithms and language equivalence testing implemented in GOAL, the correctness of a user-defined specification automaton can be checked against an easier-to-understand QPTL formula, by translating the specification formula into an equivalent automaton and testing the equivalence between the user-defined and the machine-translated automata. Once the specification automaton of an ideal size has been successfully constructed and checked, it can be exported as Promela code which can then be fed into the Spin model checker.

Besides the support for education and learning, GOAL can also support research in various aspects. For example, with the graphical interface, translation algorithms, complementation algorithms, language equivalence testing, and other utility functions implemented, GOAL can help researchers develop new algorithms with cross-checking of correctness, generation of random tests, collection of statistical data from comparison experiments, More importantly, when researchers found some results are different to their expectation, they can use GOAL to “see” what the problem is. Besides the graphical interface, GOAL also provides a command-line

(21)

interface and a script interpreter. The command-line interface and the script interpreter not only make experiments easy to be performed in GOAL, but also make other tools easy to access functions provided by GOAL. With the two features, GOAL has been used by other researchers in their work [11, 12, 56].

To the best of our knowledge, GOAL is the first graphical interactive tool designed for ω-automata and temporal logics. There are other tools that provide translation of LTL into B¨uchi automata, e.g., Spin [42], LTL2BA [32], Wring [86], MoDeLLa [81], and LTL2Buchi [35]. Spin in particular is an automata-theoretic model checker that has been widely used both in practice and in education. None of these tools provide facilities for visually manipulating automata and the temporal logics they support are less expressive than QPTL supported by GOAL. GOAL also supports past temporal operators which make some specifications easier to write.

The operations and tests on B¨uchi automata provided by GOAL are also more comprehensive than those by other tools.

1.4.2 B¨ uchi Store

To apply the automata-theoretic approach, an algorithm for translating a temporal formula into an equivalent B¨uchi automaton is essential. There has been a long line of research on such translation algorithms, aiming to produce smaller automata.

According to our experiments, none of the proposed algorithms outperforms the others for every temporal formula tested. Table 7.5 shows a comparison of some of the well-known translation algorithms for selected temporal formulae. From the table, we observe that, although one algorithm (LTL2BA) is better than the other algorithms in most cases, quite a few of the automata that it produces are still larger than the best ones that we know (in the second column of the table). Following [13],

(22)

Figure 1.1: Main page of B¨uchi Store and search of 2(request → 3response) in progress.

we also experimented with temporal formulae of the form 3(p¹ ∧3(p² ∧3(· · · ∧ 3(pⁿ⁻¹∧3pⁿ) · · ·))) ∧3(q¹∧3(q²∧3(· · · ∧ 3(qⁿ⁻¹∧3qⁿ) · · ·))) as shown in Table 7.4. In this experiment, Spin is the best, but again many of the results may be further improved.

Given that smaller automata usually expedite the model-checking process, it is certainly desirable that one is always guaranteed to get the smallest possible automaton for (the negation of) a specification formula. One way to provide the guarantee is to try all algorithms or even manual constructions and take the best result. This simple-minded technique turns out to be feasible, as most specifications use formulae of the same patterns [22] and the tedious work of trying all alternatives needs only be done once for a particular pattern instance.

Sometimes it may be hard, if not impossible (using quantification over propositions), to give the specification as a temporal formula. When the specification is

(23)

given directly as an automaton, taking the complement (perhaps incrementally) of the specification automaton becomes necessary. Consequently, in parallel with the research on translation algorithms, there has also been substantial research on algorithms for B¨uchi complementation. The aim again is to produce smaller automata.

Several B¨uchi complementation algorithms have been proposed that achieve the lower bound of 2^{Ω(n log n)} [69]. However, the performances of these “optimal” algorithms differ from case to case, sometimes quite dramatically. Table 7.6 shows a comparison of some of the complementation algorithms for selected B¨uchi automata (identified by equivalent temporal formulae). From the table, we again observe that, although one algorithm (Rank-Based) is better than the other algorithms in most cases, many of the results that it produces are still larger (some much larger) than the known best ones. In the literature, evaluations of these algorithms usually stop at a theoretical-analysis level, partly due to the lack of or inaccessibility to actual im- plementations. This may be remedied if a suitable set of benchmark cases becomes available and subsequent evaluations are conducted using the same benchmark.

B¨uchi Store was thus motivated and implemented as a website², whose main page is shown in Figure 1.1. One advantage for the Store to be on the Web is that the user always gets the most recent collection of automata. Another advantage is that it is easily made open for the user to contribute better (smaller) automata.

In the current implementation of the Store, automata are grouped into equivalence classes induced by the languages that they recognize. The current collection contains over two hundred equivalence classes. Most automata are associated with their equivalent temporal formulae. Additional properties such as classification into the Manna-Pnueli temporal hierarchy [65] are also provided.

2

URL of B¨ uchi Store: http://buchi.im.ntu.edu.tw/.

(24)

With the collection of Büchi automata as a start, we soon realized that similar collections are also desired for other types of ω-automata. Of particular interest are deterministic Büchi and deterministic parity automata. In the context of auto- matic synthesis of reactive systems from temporal specifications, deterministic automata are useful for battling high complexity [74, 85]. Though deterministic Büchi (word) automata (DBWs) are less expressive than nondeterministic Büchi automata (NBWs) for encoding temporal properties, DBWs wherever adequate are favored for they allow more efficient synthesis algorithms and produce better results. DBWs are also useful in the classification of temporal properties. Deterministic parity automata (DPWs), on the other hand, are as expressive as NBWs. When used for synthesis, DPWs induce two-player games with the parity condition that are easier to solve than games induced by other types of deterministic ω-automata. However, algorithms for obtaining deterministic automata introduce exponential blow-ups in the number of states and their performances vary for different inputs. Büchi Store can be a good source of small deterministic automata for common temporal properties.

1.5 Overview

This thesis proposal is organized as the following.

Chapter 2 shows related work on temporal formulae translation, B¨uchi complementation, 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.

(25)

Chapter 5 introduces the optimization heuristics for B¨uchi complementation algorithms and a comparative experimentation on the best construction in each complementation 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.

(26)

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 specification. 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

(27)

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 construction 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 successors 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

(28)

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 improved 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 processed 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 rewriting, 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 alternating co-B¨uchi automata (VWAA) and TGBA as its intermediate representations.

(29)

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 conversion 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 during 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

(30)

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üchi automaton by an inductive construction. In the congruent automaton, a new proposition is introduced to represent the time of the evaluaiton of the formula. A Büchi automaton equivalent to the formula is then obtained by taking the intersection of the congruemtn automaton and another Büchi 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 introduced by Büchi in 1960 involves a Ramsey-based combinatorial argument and results in a 2²Ô(n) blow-up in the state size [8]. This construction was later improved by Sistla, Vardi, and Wolper to reach a single-exponential complexity 2Ô(n²⁾ [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 heuristics for the Ramsey-based approach are described in [3, 26], but the focus in these

(31)

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 2^{O(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 understood more easily [70, 4]. In [74], Piterman improved Safra’s construction by using a more compact structure and using parity automata as the intermediate deterministic automata, which yields an upper bound of n²ⁿ. (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 complement DPW to complement 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 simplifying 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

(32)

have complexity 2^{O(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)ⁿ) states, which matches the known lower bound modulo an O(n²) 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)ⁿ while its preliminary version in [101], referred to as Slice here, has a (3n)ⁿblow-up¹. 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 performs 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.

(33)

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.

2.3 Containment Testing of B¨ uchi Automata

Most recent work on incremental containment testing for Büchi automata was motivated by an implicit algorithm with a subsumption relation proposed by Doyen and Raskin [20, 21], which is an extension of the antichain algorithm for classic finite automata [18]. During a test of whether a Büchi automaton A is contained in another Büchi automaton B, this implicit algorithm computes incrementally the product states of A × B based on the rank-based approach until a counterexample is found, while keeping only a minimal set of product states according to a subsumption relation on the product states. Such a subsumption relation allows the discard of product states whose behaviors are subsumed by other states and thus, avoids the exploration of the full product automaton.

Later in [26], Fogarty and Vardi proposed an incremental algorithm based on the Ramsey-based approach for universality testing, which is a special case of containment testing. Rather than computing product states incrementally in the rank-based containment testing algorithm, this Ramsey-based algorithm divides a universality testing of a B¨uchi automaton into smaller tests on proper pairs of elements in the transition monoid of the automaton. Each element in the transition monoid characterizes a set of finite strings that behave exactly the same in the automaton while

(34)

each proper pair characterizes a set of infinite strings that behave exactly the same in the automaton. The algorithm stops as long as it finds a proper pair that characterizes a set of infinite strings rejected by the automaton. They also extended the subsumption relation in [5] to reduce the elements need to take into account.

Their experimental results showed that neither the rank-based algorithm nor the Ramsey-based algorithm to B¨uchi universality testing is superior.

Another important work in containment testing is the application of simulation relations in obtaining larger subsumption relations, which make containment testing even faster. Such a simulation subsumption was first proposed by Abdulla et al. for the universality and containment testing of classic finite automata and tree automata [3]. Later, Abdulla et al. proposed a subsumption with a forward simulation relation for the Ramsey-based containment testing algorithm [1]. Their experimental results showed that their approach consistently outperforms the approach in [26]. The simulation subsumption for the Ramsey-based containment testing algorithm was then extended by Abdulla et al. by using also backward simulation relations and simulation relations between the two automata under test [2].

(35)

Chapter 3 Preliminaries

In this section, we give some common notations and then describe basic definitions of propositional temporal logic (PTL), ω-automata, and the Manna-Pnueli temporal hierarchy.

3.1 Common Notations

Let S be a finite set and ρ = s₀s₁· · · a sequence where s_i ∈ S for all i ≥ 0. The empty sequence is denoted by . The length of ρ is denoted by |ρ|. If the sequence ρ is infinite, then |ρ| = ω. The i-th element of the sequence ρ is denoted by ρ(i) = s_i while the i-th suffix of the sequence is denoted by ρ_i = s_is_i+1· · ·. We use the superscript ∗ and ω over a set to denote respectively finite and infinite sequences of elements of the set. The union of finite sequences and infinite sequences is denoted by the superscript ◦.

3.2 Propositional Temporal Logic

A propositional temporal logic (PTL) formula is inductively constructed from a set AP of atomic propositions where we apply (a) boolean operators, (b) the future operators (next) and U (until), and (c) the past operators ⁻ (previous) and S (since) as follows:

(36)

• Every atomic proposition p ∈ AP is a PTL formula.

• If ϕ, ϕ₁, and ϕ₂ are PTL formulae, then so are ¬ϕ, ϕ₁∨ ϕ₂,ϕ, ϕ₁ U ϕ₂, ⁻ϕ, and ϕ₁ S ϕ₂.

Let ϕ, ϕ1, and ϕ2 be PTL formulae and p an atomic proposition in AP . Other shorthands and operators can be defined as below.

> ≡ p ∨ ¬p ⊥ ≡ ¬>

ϕ₁∧ ϕ₂ ≡ ¬((¬ϕ₁) ∨ (¬ϕ₂))

ϕ1 → ϕ2 ≡ (¬ϕ1) ∨ ϕ2 ϕ1 ↔ ϕ2 ≡ (ϕ1 → ϕ2) ∧ (ϕ2 → ϕ1)

3ϕ ≡ > U ϕ 2ϕ ≡ ¬3¬ϕ

ϕ₁ W ϕ₂ ≡ (2ϕ¹) ∨ (ϕ₁ U ϕ₂) ϕ₁ R ϕ₂ ≡ ¬((¬ϕ₁) U (¬ϕ₂))

∼ϕ ≡ ¬⁻¬ϕ first ≡ ^∼⊥

3ϕ ≡ > S ϕ− 2ϕ ≡ ¬⁻ 3¬ϕ⁻

ϕ₁ B ϕ₂ ≡ (2ϕ⁻ ¹) ∨ (ϕ₁ S ϕ₂) ϕ₁ T ϕ₂ ≡ ¬((¬ϕ₁) S (¬ϕ₂))

A literal is an atomic proposition or its negation. A future formula is a formula without past operators while a past formula is a formula without future operators.

A basic formula is either True, False, a literal, a -formula, a ⁻-formula, or a

∼-formula. A set of formulae is basic if all its formulae are. A non-basic formula ϕ can be decomposed by the tableau rules in Table 3.1 such that

ϕ ↔ ^

ψ1∈α1(ϕ)

ψ₁∨ ^

ψ2∈α2(ϕ)

ψ₂.

A formula is in negation normal form (NNF) if negation only appears right before atomic propositions. For every PTL formula f , there is a PTL formula g in NNF that is congruent (to be described later) to f .

Let w = a₀a₁· · · be an infinite word where each symbol a_i ⊆ AP for all i. A symbol a can be viewed as an evaluation of atomic propositions where an atomic proposition p is true in s if and only if p ∈ s. Given an infinite word w, an index i ≥ 0, and a PTL formula ϕ, the word satisfies the formula at position i if and only if (w, i) |= ϕ. An infinite word w satisfies a PTL formula ϕ (equivalently w

(37)

ϕ α₁(ϕ) α₂(ϕ) f ∧ g f , g false

f ∨ g f g

f U g g f , (f U g) f W g g f , (f W g)

f S g g f , ⁻(f S g) f B g g f , ^∼(f B g)

Table 3.1: Tableau rules.

is a model of ϕ, or ϕ holds on w), denoted by w |= ϕ, if and only if (w, 0) |= ϕ.

The language of a PTL formula ϕ is the set of all models of ϕ, denoted by L(ϕ).

Let p be an atomic proposition and ϕ, ϕ₁, and ϕ₂ PTL formulae. The semantics of (w, i) |= ϕ is given below.

• (w, i) |= p ⇐⇒ p ∈ w(i),

• (w, i) |= ¬ϕ ⇐⇒ (w, i) 6|= ϕ,

• (w, i) |= ϕ1∨ ϕ2 ⇐⇒ (w, i) |= ϕ1 or (w, i) |= ϕ2,

• (w, i) |=ϕ ⇐⇒ (w, i + 1) |= ϕ,

• (w, i) |= ϕ₁ U ϕ₂ ⇐⇒ for some k ≥ i, (w, k) |= ϕ₂, and for all j, i ≤ j <

k, (w, j) |= ϕ₁

• (w, i) |= ⁻ϕ ⇐⇒ i > 0 and (w, i − 1) |= ϕ,

• (w, i) |= ϕ1 S ϕ2 ⇐⇒ for some k ≤ i, (w, k) |= ϕ2, and for all j, k < j ≤ i, (w, j) |= ϕ₁

A formula ϕ is satisfiable if it holds on some model while the formula is called valid, denoted by |= ϕ, if it holds on all models. Formulae ϕ₁ and ϕ₂ are equivalent, denoted by ϕ₁ ∼ ϕ₂ if the formula ϕ₁ ↔ ϕ₂ is valid. Formulae ϕ₁ and ϕ₂ are

(38)

congruent, denoted by ϕ₁ ≈ ϕ₂ if the formula2(ϕ¹ ↔ ϕ₂) is valid. Obviously, every formula ϕ has a formula in NNF that is congruent to ϕ.

3.3 ω-Automata

A nondeterministic ω-automaton A is a tuple (Σ, Q, q₀, δ, F ) where Σ is a finite alphabet, Q a finite set of states, q₀ ∈ Q the initial states, δ : Q × Σ → 2^Q a transition function, and F an acceptance condition, to be described subsequently.

A is deterministic if |δ(q, a)| = 1 for all q ∈ Q and a ∈ Σ. Note that sometimes we may restrict the automaton to have only one initial state for simplicity.

Given an automaton A = (Σ, Q, q₀, δ, F ) and an infinite word w = a₀a₁· · · ∈ Σ^ω, a run ρ of A on w is a sequence q₀q₁· · · ∈ Q^ω satisfying q_i+1 ∈ δ(q_i, a_i) for all i ≥ 0.

A run is accepting if it satisfies the acceptance condition and is rejecting otherwise.

A word is accepted by an automaton if there is an accepting run of the automaton on the word and is rejected otherwise. The language of an automaton A, denoted by L(A), is the set of words accepted by A.

Let ρ be a run and inf (ρ) be the set of states that occur infinitely often in ρ.

Various automata can be defined by assigning different acceptance conditions below.

• B¨uchi condition where F ⊆ Q: ρ satisfies the condition iff |ρ| = ω and inf (ρ)∩

F 6= ∅.

• Generalized B¨uchi condition where F ⊆ 2^Q: ρ satisfies the condition iff |ρ| = ω and for all F ∈ F , inf (ρ) ∩ F 6= ∅.

• Co-B¨uchi condition where F ⊆ Q: ρ satisfies the condition iff |ρ| = ω and inf (ρ) ∩ F = ∅.

(39)

• Muller condition where F ⊆ 2^Q: ρ satisfies the condition iff |ρ| = ω and there exists F ∈ F such that inf (ρ) = F .

• Rabin condition: where F ⊆ 2^Q× 2^Q: ρ satisfies the condition iff |ρ| = ω and there exists (E, F ) ∈ F such that inf (ρ) ∩ E = ∅ and inf (ρ) ∩ F 6= ∅.

• Streett condition where F ⊆ 2^Q× 2^Q: ρ satisfies the condition iff |ρ| = ω and for all (E, F ) ∈ F , inf (ρ) ∩ F 6= ∅ implies inf (ρ) ∩ E 6= ∅.

• Parity condition where F : Q → {0, 1, . . . , n}: ρ satisfies the condition iff

|ρ| = ω and min{F (q) | q ∈ inf (ρ)} is even. F (q) is called the color of a state q and F here is also called a coloring function.

Among automata with these acceptance conditions, only deterministic B¨uchi automata are less expressive than the others.

We use a system of three-letter acronyms to denote these finite-state automata.

The first letter indicates whether the automaton is nondeterministic or deterministic.

The second letter indicates whether the acceptance condition is classic Finite, Büchi, Co-Büchi, Generalized Büchi, Muller, Rabin, Streett, or Parity. The third letter is always a “W” indicating the automaton accepts words. For example, NBW stands for a nondeterministic Büchi automaton and DPW stands for a deterministic parity automaton.

An ω-automaton A is universal iff L(A) = Σ^ω. Two automata A and A⁰ are equivalent iff L(A) = L(A⁰). A state is live if it occurs in an accepting run on some word, and is dead otherwise. Dead states can be discovered using a nonemptiness algorithm, cf. [99], and can be pruned off without affecting the language of the automaton.

(40)

Automata may have labels on states rather than on transitions. A label-on-state automaton is a six tuple (Σ, Q, I, δ, L, F ) where Σ is the finite alphabet, Q a finite set of states, I ⊆ Q a set of initial states, δ ⊆ Q × Q the transition relation, L : Q → 2^Σ a labeling function, and F an acceptance condition. For s_i, s_j ∈ Q, (s_i, s_j) ∈ δ is also denoted by δ(s_i, s_j). Let w = a₀a₁· · · be an infinite word where a_i ∈ Σ for all i.

A run ρ of a label-on-state automaton on w is a sequence of states s₀s₁· · · such that s₀ ∈ I and, for every i ≥ 0, both δ(s_i, s_i+1) and a_i ∈ L(s_i). The acceptance of a run of a label-on-state automaton is the same as that of an automaton. A label-on-state automaton can be easily converted into an equivalent automaton and vice versa.

3.4 Temporal Hierarchy

In the Manna-Pnueli temporal hierarchy [65], properties specifiable by PTL formulae are classified into six classes shown in Figure 3.1. For each class, there is a canonical form of PTL formulae and every automaton in the class has an equivalent PTL formula in that canonical form. Let p, q, p_i, and q_i be past temporal formulae. The six classes and their canonical forms are described as the following.

• Safety: The canonical form of this class is2p. A property in this class basically states that something bad will not happen.

• Guarantee: The canonical form of this class is 3p. A property in this class basically states that something good will eventually happen.

• Obligation: The canonical form of this class is ∧_i(2pⁱ ∨3qⁱ). A property in this class is a combination of properties in the safety and guarantee classes.

• Recurrence: The canonical form of this class is23p. A property in this class

(41)

Safety (2p) Recurrence (23p, DBW)

Obligation (∧i(2pⁱ∨3qⁱ))

Guarantee (3p) Persistence (32p, DCW) Reactivity

(∧_i(23pⁱ∨32qⁱ), NBW)

Figure 3.1: The Manna-Pnueli Temporal Hierarchy. Here p, q, p_i, and q_i are past temporal formulae. DCW stands for deterministic co-B¨uchi (word) automaton.

basically states that some event will occur infinitely often. For each formula in this class, there is a DBW equivalent to the formula.

• Persistence: The canonical form of this class is 32p. A property in this class basically states that some event will constantly occur after some time. For each formula in this class, there is a DCW equivalent to the formula.

• Reactivity: The canonical form of this class is ∧_i(23pⁱ∨32qⁱ). Every PTL formula is equivalent to some PTL formula in the reactivity canonical form.

(42)

Chapter 4 Incremental Translation of PTL Formulae

In this chapter, we first describe the translation algorithm LTL2AUT [17] which can translate an LTL formula to an equivalent label-on-state NGW. The label-on-state NGW can later be converted into an equivalent NBW. We then introduce a backtrace procedure which makes LTL2AUT support PTL formulae including past operators. A correctness proof is given. We also propose some optimization heuristics for the extended algorithm and extend other state-based and transition-based translation algorithms in a similar way. At the end of this chapter, we compare our extended algorithms with others that also support past operators. An experimentative comparison between our extended algorithms and other LTL translation algorithms that rely on a separation of past and future operators to handle PTL formulae is also described.

4.1 The Classic Construction

LTL2AUT uses a cover computation procedure to calculate the successive states of a state. A cover of a set F of formulae is a possibly empty set of sets of PTL formulae