Characterizing Petri Nets with the Temporal Logic CTL

Model checking is a powerful technique for verifying systems and detecting errors at early stages of the design process. When model checking is used to check properties of Petri net, the specification has to be expressed in temporal logics. In this paper we will focus on how to characterize some important properties of Petri net such as reachability, liveness et al. with the computation tree logic CTL. Under the characterization Petri net can be verified automatically with the help of a model checker. Keywords-model checking; petri net; computation tree logic