We present a tutorial on verification of safety properties for parameterized systems. Such a system consists of an arbitrary number of processes; the aim is to prove correctness of the system regardless of the number of processes inside the system. First, we consider a class of parameterized systems whose behaviours can be captured exactly as Petri nets using counter abstraction. This allows analysis using the framework of monotonic transition systems introduced in [1]. Then, we consider parameterized systems for which there is no natural ordering which allows monotonicity. We describe the method of monotonic abstraction which provides an over-approximation of the transition system. We consider both systems where the over-approximation gives rise to reset Petri nets, and systems where the abstract transition relation is a set of rewriting rules on words over a finite alphabet. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Abdulla, P. A. (2010). Forcing monotonicity in parameterized verification: From multisets to words. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5901 LNCS, pp. 1–15). https://doi.org/10.1007/978-3-642-11266-9_1
Mendeley helps you to discover research relevant for your work.