Characterizing Petri Nets with the Temporal Logic CTL
Zhifeng Liu, Zhihu Xing
Available Online November 2012.
- https://doi.org/10.2991/citcs.2012.97How to use a DOI?
- model checking; petri net; computation tree logic
- 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
- Open Access
- This is an open access article distributed under the CC BY-NC license.
Cite this article
TY - CONF AU - Zhifeng Liu AU - Zhihu Xing PY - 2012/11 DA - 2012/11 TI - Characterizing Petri Nets with the Temporal Logic CTL BT - 2012 National Conference on Information Technology and Computer Science PB - Atlantis Press SP - 372 EP - 375 SN - 1951-6851 UR - https://doi.org/10.2991/citcs.2012.97 DO - https://doi.org/10.2991/citcs.2012.97 ID - Liu2012/11 ER -