CTL* model checking for time Petri nets

31Citations
Citations of this article
14Readers
Mendeley users who have this article in their library.

Abstract

This paper aims at applying the CTL*1 model checking method to the time Petri net (TPN) model. We show here how to contract its generally infinite state space into a graph that captures all its CTL* properties. This graph, called atomic state class graph (ASCG), is finite if and only if, the model is bounded.2 Our approach is based on a partition refinement technique, similarly to what is proposed in [Berthomieu, Vernadat, State class constructions for branching analysis of time Petri nets, Lecture Notes in Computer Science, vol. 2619, 2003; Yoneda, Ryuba, CTL model checking of time Petri nets using geometric regions, IEICE Trans. Inf. Syst. E99-D(3) (1998)]. In such a technique, an intermediate abstraction (contraction) of the TPN state space is first built, then refined until CTL* properties are restored. Our approach improves the construction of the ASCG in two ways. The first way deals with speeding up the refinement process by using a much more compact intermediate contraction of the TPN state space than those used in [Berthomieu, Vernadat, State class constructions for branching analysis of time Petri nets, Lecture Notes in Computer Science, vol. 2619, 2003; Yoneda, Ryuba, CTL model checking of time Petri nets using geometric regions, IEICE Trans. Inf. Syst. E99-D(3) (1998)]. The second way deals with computing each ASCG node in O(n2) instead of O(n3), n being the number of transitions enabled at the node. Experimental results have shown that our improvements have a good impact on performances. © 2005 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Boucheneb, H., & Hadjidj, R. (2006). CTL* model checking for time Petri nets. Theoretical Computer Science, 353(1–3), 208–227. https://doi.org/10.1016/j.tcs.2005.11.002

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free