Abstract
We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be dynamically updated. Our extension provides two mechanisms for updating the timing constraints of a net. First, we propose to change the static time interval of a transition each time it is newly enabled; in this case the new time interval is given as a function of the current marking. Next, we allow to update the firing date of a transition when it is persistent, that is when a concurrent transition fires. We show how to carry the widely used state class abstraction to this new kind of time Petri nets and define a class of nets for which the abstraction is exact. We show the usefulness of our approach with two applications: first for scheduling preemptive task, as a poor man’s substitute for stopwatch, then to model hybrid systems with non trivial continuous behavior.
This work has been partially supported by the ITEA2 project OpenETCS.
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
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)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Software Engineering 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 17, 133–158 (2007)
Berthomieu, B., Menasche, M.: A state enumeration approach for analyzing time Petri nets. In: Proc. of ATPN, Applications and Theory of Petri Nets (1982)
Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time petri nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 82–97. Springer, Heidelberg (2006)
Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research 42(14), 2741–2756
Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Heidelberg (2014)
Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theoretical Computer Science 321(23), 291–345 (2004)
Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed state space analysis of real-time preemptive systems. IEEE Transactions on Software Engineering 30(2) (2004)
Cellier, F.-E., Kofman, E.: Continuous System Simulation. Springer (2006)
Cellier, F.-E., Kofman, E., Migoni, G., Bortolotto, M.: Quantized state system simulation. In: Proc. GCMS 2008, Grand Challenges in Modeling and Simulation (2008)
Daws, C., Yovine, S.: Two examples of verification of multirate timed automata with kronos. In: Proc. of RTSS, IEEE Real-Time Systems Symposium (1995)
Foures, D., Albert, V., Nketsa, A.: Formal compatibility of experimental frame concept and FD-DEVS model. In: Proc. of MOSIM, International Conference on Modeling, Optimization and Simulation (2012)
Gardey, G., Lime, D., Magnin, M., Roux, O(H.): Romeo: A tool for analyzing time petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)
Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California (1974)
Nasr, O., Rached, M., Bodeveix, J.-P., Filali, M.: Spécification et vérification d’un ordonnanceur en B via les automates temporisés. L’Objet 14(4) (2008)
Ramalingam, G., Song, J., Joscovicz, L., Miller, R.E.: Solving difference constraints incrementally. Algorithmica 23 (1995)
Dal Zilio, S., Fronc, L., Berthomieu, B., Vernadat, F.: Time petri nets with dynamic firing dates: Semantics and applications. Technical Report 14148, LAAS-CNRS (2014) arXiv: 1404.7067
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Berthomieu, B., Dal Zilio, S., Fronc, Ł., Vernadat, F. (2014). Time Petri Nets with Dynamic Firing Dates: Semantics and Applications. In: Legay, A., Bozga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2014. Lecture Notes in Computer Science, vol 8711. Springer, Cham. https://doi.org/10.1007/978-3-319-10512-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-10512-3_7
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10511-6
Online ISBN: 978-3-319-10512-3
eBook Packages: Computer ScienceComputer Science (R0)