Proceedings of the 2012 National Conference on Information Technology and Computer Science

Characterizing Petri Nets with the Temporal Logic CTL

Authors
Zhifeng Liu, Zhihu Xing
Corresponding Author
Zhifeng Liu
Available Online November 2012.
DOI
https://doi.org/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
Open Access
This is an open access article distributed under the CC BY-NC license.

Download article (PDF)

Proceedings
2012 National Conference on Information Technology and Computer Science
Part of series
Advances in Intelligent Systems Research
Publication Date
November 2012
ISBN
978-94-91216-39-8
ISSN
1951-6851
DOI
https://doi.org/10.2991/citcs.2012.97How to use a DOI?
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  -