More Efficient On-the-Fly Verification Methods of Colored Petri Nets

Authors

  • Cong He Department of Computer Science and Technology, Tongji University, Shanghai, China
  • Zhijun Ding Department of Computer Science and Technology, Tongji University, Shanghai, China

DOI:

https://doi.org/10.31577/cai_2021_1_195

Keywords:

Model checking, CPN, on-the-fly, LTL, state space

Abstract

Colored Petri Nets (CP-nets or CPNs) are powerful modeling language for concurrent systems. As for CPNs' model checking, the mainstream method is unfolding that transforms a CPN into an equivalent P/T net. However the equivalent P/T net tends to be too enormous to be handled. As for checking CPN models without unfolding, we present three practical on-the-fly verification methods which are all focused on how to make state space generation more efficient. The first one is a basic one, based on a standard state space generation algorithm, but its efficiency is low. The second one is an overall improvement of the first. The third one sacrifices some applicability for higher efficiency. We implemented the three algorithms and validated great efficiency of latter two algorithms through experimental results.

Downloads

Download data is not yet available.

Downloads

Published

2021-08-03

How to Cite

He, C., & Ding, Z. (2021). More Efficient On-the-Fly Verification Methods of Colored Petri Nets. COMPUTING AND INFORMATICS, 40(1), 195–215. https://doi.org/10.31577/cai_2021_1_195