Decidability of Parameterized Verification

丛 书 名：Synthesis Lectures on Distributed Computing Theory

作     者：Bloem, Roderick Jacobs, Swen Khalimov, Ayrat 

I S B N：(纸本) 9781627057431 

出 版 社：Morgan & Claypool Publishers 

出 版 年：2015年

主 题 词：Parallel Processing 

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

摘      要：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 whether, for all 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.