Decidability of Parameterized Verification (Synthesis Lectures on Distributed Computing Theory)

While the classic model checking problem is to decide whether a finite system satisfies a specification, the goal of parameterized model checking is to decide, given finite systems M(n) parameterized by n in N, whether, for all n in N, the system M(n) satisfies a specification. In this book we consider the important case of M(n) being a concurrent system, where the number of replicated processes depends on the parameter n but each process is independent of n. Examples are cache coherence protocols, networks of finite-state agents, and systems that solve mutual exclusion or scheduling problems. Further examples are abstractions of systems, where the processes of the original systems actually depend on the parameter. We literature in this area has studied a wealth of computational models based on a variety of synchronization and communication primitives, including token passing, broadcast, and guarded transitions. Often, different terminology is used in the literature, and results are based on implicit assumptions. In this book, we introduce a computational model that unites the central synchronization and communication primitives of many models, and unveils hidden assumptions from the literature. We survey existing decidability and undecidability results, and give a systematic view of the basic problems in this exciting research area. Acknowledgments 11 Introduction 13 Motivation 14 Who Should Read This Book? 16 Organization of the Book 16 System Model and Specification Languages 17 Preliminary Terminology and Definitions 17 System Model 18 Some Standard Synchronization Primitives 21 Runs and Deadlocks 24 Parameterized Family of Uniform Concurrent Systems 25 Parameterized Specifications 25 Indexed Temporal Logics 26 Action-based Specifications 30 Specifications in the Literature 30 Model Checking Problems for Concurrent Systems 31 Computability Assumptions 32 Standard Proof Machinery 35 Techniques to Prove Undecidability of PMCP 35 How to Prove Decidability of the PMCP 36 Well-structured Transition Systems 37 Vector Addition Systems with States (and Petri Nets) 39 Decompositions and Cutoffs 40 Token-passing Systems 43 System Model 44 Direction-aware Parameterized Systems 44 Token-passing Systems 46 Results for Direction-unaware Token-passing Systems 49 Decidability for Simple Token-passing in Uni-directional Rings 50 Decidability for Simple Token-passing in Graphs 52 Undecidability Results for Multi-valued Tokens 54 Results for Direction-aware Token-passing Systems 56 Cutoffs for Change-bounded Tokens in Bi-directional Rings 56 Undecidability for Direction-aware TPSs 57 Discussion 58 Variations of the Model 60 Rendezvous and Broadcast 63 System Model 63 Decidability Results 67 Counter Representation 67 Decidability for All Three Primitives 70 Decidability for Pairwise Rendezvous 70 Undecidability Results 71 Undecidability for Broadcast 71 Undecidability for Asynchronous Rendezvous 74 Discussion 74 Variations of the Model 76 Guarded Protocols 77 Motivating Example 77 System Model 81 Classes of Guarded Protocols 85 Specifications 86 Undecidability: Boolean and Conjunctive Guards 88 Decidability: Init-Conjunctive and Disjunctive Guards 93 Preliminaries 94 Proof Schemas 96 Init-conjunctive Guards 98 Disjunctive Guards 101 Disjunctive Guards vs. Rendezvous 108 Variations on the Model: Guards and Synchronization Primitives 111 Discussion 112 Ad Hoc Networks 115 Running Example 115 System Model 116 PMC Problems for Ad Hoc Networks 117 Parameterized Connectivity Graphs BP_k, BPC_k, BD_k, C, All 119 Results for (Non-lossy) AHN s 120 Undecidability Results for (Non-lossy) AHN s 120 Decidability Results for (Non-lossy) AHN s 128 Decidability Results for Lossy Ad Hoc Networks 135 Discussion 139 Variations of the Model 140 Related Work 141 Abstraction Techniques 141 Regular Model Checking 143 Symbolic Techniques 144 Dynamic Cutoff Detection 146 Network Invariants 147 Invisible Invariants 149 Other Aspiring Approaches 149 Parameterized Model Checking Tools 151 Conclusions 155 Bibliography 157 Authors' Biographies 169 While the classic model checking problem is to decide whether a finite system satisfies a specification, the goal of parameterized model checking is to decide, given finite systems ����(n) parameterized by n ∈ N, whether, for all n ∈ N, the system ����(n) satisfies a specification. In this book we consider the important case of ����(n) being a concurrent system, where the number of replicated processes depends on the parameter n but each process is independent of n. Examples are cache coherence protocols, networks of finite-state agents, and systems that solve mutual exclusion or scheduling problems. Further examples are abstractions of systems, where the processes of the original systems actually depend on the parameter. The literature in this area has studied a wealth of computational models based on a variety of synchronization and communication primitives, including token passing, broadcast, and guarded transitions. Often, different terminology is used in the literature, and results are based on implicit assumptions. In this book, we introduce a computational model that unites the central synchronization and communication primitives of many models, and unveils hidden assumptions from the literature. We survey existing decidability and undecidability results, and give a systematic view of the basic problems in this exciting research area. While the classic model checking problem is to decide whether a finite system satisfies a specification, the goal of parameterized model checking is to decide, given finite systems M(n) parameterized by n ∈ N, whether, for all n ∈ N, the system M(n) satisfies a specification. In this book we consider the important case of M(n) being a concurrent system, where the number of replicated processes depends on the parameter n but each process is independent of n. Examples are cache coherence protocols, networks of finite-state agents, and systems that solve mutual exclusion or scheduling problems. Further examples are abstractions of systems, where the processes of the original systems actually depend on the parameter.The literature in this area has studied a wealth of computational models based on a variety of synchronization and communication primitives, including token passing, broadcast, and guarded transitions. Often, different terminology is used in the literature, and results are based on implicit assumptions. In this book, we introduce a computational model that unites the central synchronization and communication primitives of many models, and unveils hidden assumptions from the literature. We survey existing decidability and undecidability results, and give a systematic view of the basic problems in this exciting research area