Applying Step Coverability Trees to Communicating Component-Based Systems

Like reachability, coverability is an important tool for verifying behavioural properties of dynamic systems. When a system is modelled as a Petri net, the classical Karp-Miller coverability tree construction can be used to decide questions related to the (required) capacity of local states. Correctness (termination) of the construction is based on a monotonicity property: more resources available implies more behaviour possible. Here we …