Forcing Monotonicity in Parameterized Verification: From Multisets to Words

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 ng 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 city. 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, ems where the abstract transition relation is a set of rewriting rules on words over a finite alphabet.

• Type: Journal
• Year: 2010
• Where: SOFSEM
• Authors: Parosh Aziz Abdulla
• Keywords: Abstract Transition Relation, Parameterized Systems, SOFSEM 2010, Theoretical Computer Science, Transition System