Characterizing Petri Nets with the Temporal Logic CTL

DOI

10.2991/citcs.2012.97How to use a DOI?

Keywords

model checking; petri net; computation tree logic

Abstract

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

Copyright

© 2012, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Zhifeng Liu
AU  - Zhihu Xing
PY  - 2012/11
DA  - 2012/11
TI  - Characterizing Petri Nets with the Temporal Logic CTL
BT  - Proceedings of the 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  - 10.2991/citcs.2012.97
ID  - Liu2012/11
ER  -