Unfoldings (eBook)

A Partial-Order Approach to Model Checking

Javier Esparza, Keijo Heljanko (Autoren)

eBook Download: PDF

2008
172 Seiten
Springer Berlin (Verlag)
9783540774266 (ISBN)

Infos

In this book the authors introduce unfoldings, an approach to model checking which alleviates the state explosion problem by means of concurrency theory. They offer an introduction to the basics of the method and detail an unfolding-based algorithm for model checking concurrent systems against properties specified as formulas of linear temporal logic (LTL). The book will be of value to researchers and graduate students engaged in automatic verification and concurrency theory.

Inhalt

Foreword by Ken McMillan 7
Preface 9
Contents 11
1 Introduction 13
Structure of the Book 15
2 Transition Systems and Products 17
2.1 Transition Systems 17
2.2 Products of Transition Systems 18
2.3 Petri Net Representation of Products 20
2.4 Interleaving Representation of Products 22
Bibliographical Notes 24
3 Unfolding Products 25
3.1 Branching Processes and Unfoldings 26
3.2 Some Properties of Branching Processes 34
3.3 Veri.cation Using Unfoldings 38
3.4 Constructing the Unfolding of a Product 40
3.5 Search Procedures 45
3.6 Goals and Milestones for Next Chapters 47
Bibliographical Notes 49
4 Search Procedures for the Executability Problem 53
4.1 Search Strategies for Transition Systems 53
4.2 Search Scheme for Transition Systems 55
4.3 Search Strategies for Products 60
4.4 Search Scheme for Products 68
4.5 Adequate Search Strategies 71
4.6 Complete Search Scheme for Arbitrary Strategies 79
Bibliographical Notes 83
5 More on the Executability Problem 85
5.1 Complete Pre.xes 85
5.2 Least Representatives 94
5.3 Breadth-First and Depth-First Strategies 98
5.4 Strategies Preserved by Extensions Are Well- Founded 103
Bibliographical Notes 106
6 Search Procedures for the Repeated Executability Problem 109
6.1 Search Scheme for Transition Systems 109
6.2 Search Scheme for Products 113
Bibliographical Notes 117
7 Search Procedures for the Livelock Problem 119
7.1 Search Scheme for Transition Systems 119
7.2 Search Scheme for Products 127
Bibliographical Notes 135
8 Model Checking LTL 137
8.1 Linear Temporal Logic 138
8.2 Interpreting LTL on Products 138
8.3 Testers for LTL Properties 141
8.4 Model Checking with Testers: A First Attempt 148
8.5 Stuttering Synchronization 150
Bibliographical Notes 159
9 Summary, Applications, Extensions, and Tools 163
9.1 Looking Back: A Two-Page Summary of This Book 163
9.2 Some Experiments 164
9.3 Some Applications 165
9.4 Some Extensions 166
9.5 Some Tools 168
References 169
Index 177

Produkt-Details

• Erscheint lt. Verlag: 12.3.2008
• Reihe/Serie: Monographs in Theoretical Computer Science. An EATCS Series
• Reihe/Serie: Monographs in Theoretical Computer Science. An EATCS Series
• Zusatzinfo: XII, 172 p. 51 illus.
• Verlagsort: Berlin
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Schlagworte: algorithm • algorithms • Automat • Computer-Aided Verification • Concurrency • Distributed Systems • Logic • Model Checking • Petri Nets • Unfoldings • verification
• ISBN-13: 9783540774266 / 9783540774266