Slicing Petri nets with an application to workflow verification

Abstract

We introduce the notion of net-slice to describe a subnet of a marked Petri net E that approximates Σ's temporal behaviour with respect to a set of places P. We consider slices Σ′ whose set of places comprises the places referred to by a CTL* formula Φ. If Σ is fair w.r.t. the transitions of a slice, Σ \= Φ can be verified and falsified by examining the slice, given Φ is a CTL* formula built without using the next-time operator. Verification of LTL-X formulas is thus possible under these very weak fairness assumptions, though LTL formulas using next-time can be falsified. © Springer-Verlag Berlin Heidelberg 2008.