Javier Esparza is Professor and Chair of Foundations of Software Reliability and Theoretical Computer Science at the Technical University of Munich and coauthor of Free Choice Petri Nets and Unfoldings: A Partial-Order Approach to Model Checking. Michael Blondin is Associate Professor of Computer Science at the Université de Sherbrooke.
Inhaltsangabe
Preface xiii 0 Overview 1 I Automata on Finite Words 1 Automata Classes and Conversions 9 2 Minimization and Reduction 49 3 Operations on Sets: Implementations 75 4 Application 1: Pattern Matching 101 5 Operations on Relations: Implementations 113 6 Finite Universes and Decision Diagrams 131 7 Application II: Verification 163 8 Automata and Logic 193 9 Application III: Presburger Arithmetic 229 II Automata on Infinite Words 10 Classes of Automata and Conversions 247 11 Boolean Operations: Implementations 289 12 Emptiness Check: Implementations 313 13 Application I: Verification and Temporal Logic 341 14 Application II: MSO Logics on Words and Linear Arithmetic 365 Solutions 377 Bibliographic Notes 523 Bibliography 531 Index 539
