Abstract
We present a model checking algorithm for safety properties that is applicable to parameterized systems and hence provides a unifying approach of model checking for parameterized systems. By analysing the conditions under which the proposed algorithm terminates, we obtain a characterisation of a subclass for which this problem is decidable. The known decidable subclasses, token rings and broadcast systems, fall in our subclass, while the main novel feature is that (unnested) quantification over index variables is allowed, which means that global guards can be expressed.
Cite
CITATION STYLE
Maidl, M. (2001). A unifying model checking approach for safety properties of parameterized systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2102, pp. 311–323). Springer Verlag. https://doi.org/10.1007/3-540-44585-4_29
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
