Abstract
This paper proposes a new method to compute symbolic unfoldings for safe Stopwatch Petri Nets (SwPNs), extended with time parameters, that symbolically handle both the time and the parameters.
We propose a concurrent semantics for (parametric) SwPNs in terms of timed processes à la Aura and Lilius. We then show how to compute a symbolic unfolding for such nets, as well as, for the subclass of safe time Petri nets, how to compute a finite complete prefix of this unfolding.
Our contribution is threefold: unfolding in the presence of stopwatches or parameters has never been addressed before. Also in the case of time Petri nets, the proposed unfolding has no duplication of transitions and does not require read arcs and as such its computation is more local. Finally the unfolding method is implemented (for time Petri nets) in the tool Romeo.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Iyer, S.P., Nylen, A.: Unfoldings of unbounded Petri nets. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 495–507. Springer, Heidelberg (2000)
Aura, T., Lilius, J.: A causal semantics for time Petri nets. Theoretical Computer Science 243(2), 409–447 (2000)
Baldan, P., Busi, N., Corradini, A., Pinna, G.M.: Functorial concurrent semantics for Petri nets with read and inhibitor arcs. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 442–457. Springer, Heidelberg (2000)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Soft. Eng. 17(3), 259–273 (1991)
Berthomieu, B., Lime, D., Roux, O.H., Vernadat, F.: Reachability problems and abstract state spaces for time Petri nets with stopwatches. Journal of Discrete Event Dynamic Systems - Theory and Applications (DEDS) 17(2), 133–158 (2007)
Chatain, T., Jard, C.: Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 125–145. Springer, Heidelberg (2006)
Chatain, T., Jard, C.: Sémantique concurrente symbolique des réseaux de Petri saufs et dépliages finis des réseaux temporels. In: Proceedings of NOTERE, Tozeur, Tunisia. IEEE Computer Society Press, Los Alamitos (May-June 2010)
Esparza, J.: Model checking using net unfoldings. Science of Computer Programming 23, 151–195 (1994)
Esparza, J., Heljanko, K.: Unfoldings, A Partial-Order Approach to Model Checking. In: Monographs in Theoretical Computer Science. Springer, Heidelberg (2008)
Grabiec, B., Traonouez, L.-M., Jard, C., Lime, D., Roux, O.H.: Diagnosis using unfoldings of parametric time Petri nets. In: Proceedings of FORMATS, Vienna, Austria. LNCS. Springer, Heidelberg (to appear, September 2010)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences 57, 94–124 (1998)
Khomenko, V., Koutny, M.: Branching processes of high-level Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 458–472. Springer, Heidelberg (2003)
Lime, D., Roux, O.(H.): Formal verification of real-time systems with preemptive scheduling. Journal of Real-Time Systems 41(2), 118–151 (2009)
McMillan, K.L.: Using unfolding to avoid the state space explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993)
Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, Dep. of Information and Computer Science, University of California, Irvine, CA (1974)
Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. Journal of Universal Computer Science (J.UCS) 15(17), 3273–3304 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Traonouez, LM., Grabiec, B., Jard, C., Lime, D., Roux, O.H. (2010). Symbolic Unfolding of Parametric Stopwatch Petri Nets. In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-15643-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15642-7
Online ISBN: 978-3-642-15643-4
eBook Packages: Computer ScienceComputer Science (R0)