Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 5215))
Included in the following conference series:
555Accesses
Abstract
We consider here time Petri nets (the TPN model) and two of its state space abstractions: the state class graph (SCG) and the zone based graph (ZBG). We show that only some time points of the clock/firing domains of abstract states are relevant to construct a TPN reachability graph. Moreover, for the state class graph method, the graph computed using relevant time points is smaller than the SCG.
This is a preview of subscription content,log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Behrmann, G., Bouyer, P., Larsen, K.G., Pelànek, R.: Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer 8(3), 204–215 (2006)
Bengtsson, J.: Clocks, DBMs and States in Timed Systems, PhD thesis, Dept. of Information Technology, Uppsala University (2002)
Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 442–457. Springer, Heidelberg (2003)
Boucheneb, H., Rakkay, H.: A more efficient time Petri net state space abstraction preserving linear properties. In: Proc. of the seventh International Conference on Application of Concurrency to System Design (ASCD 2007), pp. 61–70. IEEE Computer Society, Los Alamitos (2007)
Boucheneb, H., Hadjidj, R.: CTL* model checking for time Petri nets. Journal of Theoretical Computer Science TCS 353(1-3), 208–227 (2006)
Gardey, G., Roux, O.H., Roux, O.F.: State space computation and analysis of time Petri nets. Theory and Practice of Logic Programming (TPLP), Special Issue on Specification Analysis and Verification of Reactive Systems 6(3), 301–320 (2006)
Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets, Technical Report IRCCyN number RI 2006-14 (2006)
Penczek, W., Pólrola, A.: Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 37–76. Springer, Heidelberg (2004)
Popova-Zeugmann, L., Schlatter, D.: Analyzing paths in time Petri nets. Fundamenta Innformaticae 37, 311–327 (1999)
Yoneda, T., Schlingloff, B.H.: Efficient Verification of Parallel Real-Time Systems. Formal Methods in System Design 11(2), 187–215 (1997)
Author information
Authors and Affiliations
Laboratoire VeriForm, Department of Computer Engineering, École Polytechnique de Montréal, P.O. Box 6079, Station Centre-ville, Montréal, Québec, Canada, H3C 3A7
Hanifa Boucheneb
Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 192 rue Saint Martin, Paris Cedex 03, France
Kamel Barkaoui
- Hanifa Boucheneb
You can also search for this author inPubMed Google Scholar
- Kamel Barkaoui
You can also search for this author inPubMed Google Scholar
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boucheneb, H., Barkaoui, K. (2008). Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs. In: Cassez, F., Jard, C. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2008. Lecture Notes in Computer Science, vol 5215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85778-5_19
Download citation
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-540-85777-8
Online ISBN:978-3-540-85778-5
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative