Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components
DOI:
https://doi.org/10.7146/dpb.v26i519.7048Abstract
In this paper we present a CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets. The logic has been designed to express properties of both state and transition information. This is possible because the state spaces are labelled transition systems. We compare the expressiveness of our logic with CTL's. Then, we present a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules. We present empirical results for non-trivial examples and compare the performance of our algorithm with that of Clarke, Emerson, and Sistla.Downloads
Published
1997-03-01
How to Cite
Cheng, A., Christensen, S., & Mortensen, K. H. (1997). Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components. DAIMI Report Series, 26(519). https://doi.org/10.7146/dpb.v26i519.7048
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.