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

## 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

### 論

### 論 論文 文 文摘 摘 摘要 要 要

以自動機理論為基礎的模型檢測方法已經發展近三十年，此方法被認為具有效 率且容易使用，在確保軟體或硬體設計的正確性上，已成為業界測試與模擬之外 的另一項選擇。在這個方法中，一個待測的系統會用一個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已經幫助我們開發許多改進的演算法，讓模型檢測更

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

### 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¨uchi automata which in certain cases are more natural and easier than temporal formulae. In such cases, comple- mentation of a specification automaton is performed before taking the intersection with the system automaton. The complementation of B¨uchi automata is signifi- cantly 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¨uchi complementation, much recent emphasis has been shifted to containment test- ing without constructing the complement. The Ramsey-based approach has been proven to be quite effective in such containment testing, although it is not compet- itive 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 algo- rithms with a backtrace procedure to support past operators of PTL, while maintain- ing the advantages of incremental automata construction. The cover computation

common to the state-based incremental algorithms is improved based on prime im- plicants 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 compar- ative 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 re- sults show that the deterministic construction is the best for complementation in general. We also propose optimization heuristics for three of the four best construc- tions. Our experiment shows that the optimization heuristics substantially improve the three constructions.

For containment testing, we propose an incremental containment testing ap- proach 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 ap- proach. 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 manipu- lating automata and temporal formulae. This motivated our GOAL tool, which is the first interactive graphical tool for learning ω-automata and temporal log- ics. 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.

## Contents

1 Introduction 1

1.1 Translation of Temporal Formulae . . . 2

1.2 Complementation of B¨uchi Automata . . . 5

1.3 Incremental Containment Testing . . . 7

1.4 Tool Support . . . 8

1.4.1 GOAL . . . 8

1.4.2 B¨uchi Store . . . 11

1.5 Overview . . . 14

2 Related Work 16 2.1 Translation of Propositional Temporal Formulae . . . 16

2.2 Complementation of B¨uchi Automata . . . 20

2.3 Containment Testing of B¨uchi Automata . . . 23

3 Preliminaries 25 3.1 Common Notations . . . 25

3.2 Propositional Temporal Logic . . . 25

3.3 ω-Automata . . . 28

3.4 Temporal Hierarchy . . . 30

4 Incremental Translation of PTL Formulae 32 4.1 The Classic Construction . . . 32

4.2 Construction wtih Past Operators . . . 35

4.2.1 The Translation Algorithm . . . 36

4.2.2 The Backtrace Procedure . . . 37

4.2.3 The AddTransition Procedure . . . 39

4.3 Correctness . . . 39

4.4 Optimization Heuristics . . . 44

4.5 Extension to Other Algorithms . . . 46

4.5.1 Extended GPVW . . . 46

4.5.2 Extended MoDeLLa . . . 47

4.5.3 Extended Couvreur . . . 48

4.5.4 Extended LTL2BUCHI . . . 50

4.6 Experimental Results . . . 51

4.7 Summary of this Chapter . . . 54

5 Complementation Algorithms 56

5.1 Comparison of Complementation Approaches . . . 56

5.2 Safra-Piterman Construction . . . 59

5.3 Rank-Based Construction . . . 63

5.4 Slice-Based Construction . . . 64

5.4.1 Definitions . . . 65

5.4.2 The Basic Slice Construction . . . 67

5.4.3 The Improved Slice Construction . . . 71

5.5 Experimental Results . . . 76

5.6 Complete Experimental Results . . . 79

5.6.1 Comparisons of Basic Constructions . . . 80

5.6.2 Comparisons of Improved Constructions . . . 82

5.7 Summary of this Chapter . . . 83

6 Containment Testing Algorithms 86 6.1 Safra-Piterman Construction . . . 86

6.2 Incremental Universality Testing . . . 88

6.3 Incremental Containment Testing . . . 91

6.4 Experimental Results . . . 92

6.5 Summary of this Chapter . . . 94

7 Tool Support 95 7.1 GOAL . . . 96

7.1.1 Main Functions . . . 96

7.1.2 Use Cases . . . 105

7.1.3 Implementation Details . . . 112

7.2 B¨uchi Store . . . 112

7.2.1 Features . . . 113

7.2.2 Use Cases . . . 117

7.2.3 Implementation Details . . . 122

7.3 Summary of this Chapter . . . 125

8 Conclusion 127 8.1 Contributions . . . 127

8.2 Future Work . . . 128

## 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_{0}, 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 construc- tion. . . 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

## 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 simpli- fication 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^{15} . . . 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^{15} 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 premi- nimization . . . 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^{10}, A^{15}, and A^{20} 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^{10}, A^{15}, and A^{20} with prem-
inimization . . . 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

7.1 Major algorithms in GOAL. The Modified Safra algorithm for com- plementation 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^{1}∧3(p^{2}∧3(· · · ∧ 3(p^{n−1}∧3p^{n}) · · ·))) ∧3(q^{1} ∧3(q^{2}∧3(· · · ∧
3(q^{n−1}∧3q^{n}) · · ·))). . . 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

## 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¨uchi 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¨uchi 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¨uchi 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-

lae. In such cases, a system M satisfies a specification encoded by a B¨uchi automaton A if L(M × A) = ∅ where A is the complement of A. The complementation of B¨uchi 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¨uchi 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 al- gorithm.

In this thesis, we focus on improving translation of temporal formulae, comple- mentation 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

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 au- tomaton, 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

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^{n+1}× 2^{n+1} 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 conver-
sion 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 in- cremental 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 incre- mental 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

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 rec- ognize ω-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¨uchi 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^{n} states through the subset construction [75]. Indeed, for nondeterministic
B¨uchi automata, the subset construction is insufficient for complementation. In
fact, Michel showed in 1988 that blow-up of B¨uchi complementation is at least n!

(approximately (n/e)^{n} or (0.36n)^{n}), which is much higher than 2^{n} [69]. This lower
bound was later sharpened by Yan to (0.76n)^{n} [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 trans- lation algorithm can be tested with a reference algorithm [39]. Although recently

many works have focused on universality and containment testing without going ex- plicitly 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 clas- sified 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 com- parative experimentation on the best construction in each approach. Although the conventional wisdom is that the nondeterministic approaches are better than the de- terministic 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

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 contain- ment 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: de- terminizing a B¨uchi automaton into a deterministic automaton with another accep- tance condition, complementing the deterministic automaton, and converting the complement into a B¨uchi automaton. Such three-stage complementation has an ad- vantage 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

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^{1} 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 au- tomata, two-way alternating automata, and games, (2) testing and converting ω-

1

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

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

GOAL was originally designed with a graphical interface for learning and teach- ing B¨uchi automata and linear temporal logics. As shown in [83], B¨uchi 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¨uchi automaton [49, 34, 17, 32], though not vice versa. Despite the possibility of mechanical translation, a temporal formula and its equivalent B¨uchi automaton are two very different artifacts and their correspondence is not easy to grasp. Temporal formulae describe temporal depen- dency without explicit references to time points and are in general more abstract, while B¨uchi 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 examin- ing more examples of temporal formulae and their equivalent B¨uchi automata. This

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 tempo- ral 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 algo- rithms 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 automa- ton 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 re- search 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 statis- tical 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

interface and a script interpreter. The command-line interface and the script inter- preter 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 de- signed 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],

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^{1} ∧3(p^{2} ∧3(· · · ∧
3(p^{n−1}∧3p^{n}) · · ·))) ∧3(q^{1}∧3(q^{2}∧3(· · · ∧ 3(q^{n−1}∧3q^{n}) · · ·))) 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 propo- sitions), to give the specification as a temporal formula. When the specification is

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 algo- rithms 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” algo-
rithms 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^{2}, 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/.

With the collection of B¨uchi automata as a start, we soon realized that similar collections are also desired for other types of ω-automata. Of particular interest are deterministic B¨uchi and deterministic parity automata. In the context of auto- matic synthesis of reactive systems from temporal specifications, deterministic au- tomata are useful for battling high complexity [74, 85]. Though deterministic B¨uchi (word) automata (DBWs) are less expressive than nondeterministic B¨uchi 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 au- tomata (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¨uchi Store can be a good source of small deterministic automata for common temporal prop- erties.

## 1.5 Overview

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 2^{2}^{O(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^{O(n}^{2}^{)} [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 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 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 n^{2n}. (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 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 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 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)^{n}) states, which matches the known
lower bound modulo an O(n^{2}) 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)^{n}blow-up^{1}. 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.

## 2.3 Containment Testing of B¨ uchi Automata

Most recent work on incremental containment testing for B¨uchi automata was mo- tivated 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¨uchi automaton A is contained in another B¨uchi 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 subsump- tion 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 contain- ment 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 char- acterizes a set of finite strings that behave exactly the same in the automaton while

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 char- acterizes 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].

## 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_{0}s_{1}· · · 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_{i}s_{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:

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

• If ϕ, ϕ_{1}, and ϕ_{2} are PTL formulae, then so are ¬ϕ, ϕ_{1}∨ ϕ_{2},^{
}ϕ, ϕ_{1} U ϕ_{2}, ^{
}^{−}ϕ,
and ϕ_{1} S ϕ_{2}.

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 ϕ1 ↔ ϕ2 ≡ (ϕ1 → ϕ2) ∧ (ϕ2 → ϕ1)

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

ϕ_{1} W ϕ_{2} ≡ (2ϕ^{1}) ∨ (ϕ_{1} U ϕ_{2}) ϕ_{1} R ϕ_{2} ≡ ¬((¬ϕ_{1}) U (¬ϕ_{2}))

∼ϕ ≡ ¬^{
}^{−}¬ϕ first ≡ ^{
}^{∼}⊥

3ϕ ≡ > S ϕ− 2ϕ ≡ ¬^{−} 3¬ϕ^{−}

ϕ_{1} B ϕ_{2} ≡ (2ϕ^{−} ^{1}) ∨ (ϕ_{1} S ϕ_{2}) ϕ_{1} T ϕ_{2} ≡ ¬((¬ϕ_{1}) S (¬ϕ_{2}))

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(ϕ)

ψ_{1}∨ ^

ψ2∈α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_{0}a_{1}· · · 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

ϕ α_{1}(ϕ) α_{2}(ϕ)
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 ϕ, ϕ_{1}, and ϕ_{2} 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) |= ϕ_{1} U ϕ_{2} ⇐⇒ for some k ≥ i, (w, k) |= ϕ_{2}, and for all j, i ≤ j <

k, (w, j) |= ϕ_{1}

• (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) |= ϕ_{1}

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 ϕ_{1} and ϕ_{2} are equivalent,
denoted by ϕ_{1} ∼ ϕ_{2} if the formula ϕ_{1} ↔ ϕ_{2} is valid. Formulae ϕ_{1} and ϕ_{2} are

congruent, denoted by ϕ_{1} ≈ ϕ_{2} if the formula2(ϕ^{1} ↔ ϕ_{2}) 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_{0}, δ, F ) where Σ is a finite
alphabet, Q a finite set of states, q_{0} ∈ 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_{0}, δ, F ) and an infinite word w = a_{0}a_{1}· · · ∈ Σ^{ω},
a run ρ of A on w is a sequence q_{0}q_{1}· · · ∈ 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 = ∅.

• 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 au- tomata 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¨uchi, Co-B¨uchi, Generalized B¨uchi, 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¨uchi automaton and DPW stands for a deterministic parity automaton.

An ω-automaton A is universal iff L(A) = Σ^{ω}. Two automata A and A^{0} are
equivalent iff L(A) = L(A^{0}). 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.

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_{0}a_{1}· · · 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_{0}s_{1}· · · such that
s_{0} ∈ 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^{i} ∨3q^{i}). 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

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

Obligation
(∧i(2p^{i}∨3q^{i}))

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

(∧_{i}(23p^{i}∨32q^{i}), 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^{i}∨32q^{i}). Every PTL
formula is equivalent to some PTL formula in the reactivity canonical form.

## 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 com- parison 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