Techniques for Solving Boolean Equation Systems

CONTENTS......Page 9
List of Figures......Page 11
List of Tables......Page 12
PREFACE......Page 13
1 INTRODUCTION......Page 15
1.1 Related Work......Page 17
1.2 Contribution of the Thesis......Page 18
1.3 Organization of the Thesis......Page 21
2.2 The µ-Calculus as a Speci cation Language......Page 22
2.3 Boolean Equation Systems......Page 25
2.4 µ-Calculus Model Checking with Boolean Equation Systems......Page 32
2.5 Boolean Equation Systems and Parity Games......Page 35
2.6 Normal Logic Programs......Page 38
2.7 Difference Logic......Page 40
3.1 Partitioning Boolean Equation Systems......Page 42
3.2 Types of Blocks of a Boolean Equation System......Page 43
3.3 General Solution Algorithm for Boolean Equation Systems......Page 44
4.2 Minimal and Maximal Blocks as Logic Programs......Page 48
5.1 Properties of Conjunctive and Disjunctive Blocks......Page 52
5.2 Depth-First Search Based Algorithm......Page 55
5.3 An Algorithm Based on Hierarchical Clustering......Page 57
5.4 Discussion......Page 66
6.1 Solving General Form Blocks in Answer Set Programming......Page 68
6.2 Properties of General Boolean Equation System......Page 69
6.3 From General Blocks to Logic Programs......Page 71
6.4 Correctness of the Translation......Page 72
6.5 Implementation Issues......Page 74
7.1 Solving General Form Blocks with Satis ability Solvers......Page 76
7.2 Characterising Solutions with µ-Annotations......Page 78
7.3 Encoding Solutions in Difference Logic......Page 80
7.4 Correctness of the Encoding......Page 81
7.5 An Encoding into Propositional Logic......Page 83
7.6 Discussion......Page 85
8.1 Tests for Conjunctive and Disjunctive Blocks......Page 87
8.2 Tests for General Form Blocks......Page 93
9 CONCLUSION......Page 99
References......Page 101