Abstract
In this paper, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass \({\cal TA}^{wtb}\) of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for \({\cal TA}^{wtb}\) are PSPACE-complete. Furthermore we show that for a TA in \({\cal TA}^{wtb}\) with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.
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.
Similar content being viewed by others
References
Aceto, L., Laroussinie, F.: Is Your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics. In: Journal of Logic and Algebraic Programming, vol. 52-53, pp. 7–51. Elsevier Science Publishers, Amsterdam (august 2002)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science B 126, 183–235 (1994)
Aura, T., Lilius, J.: A causal semantics for time Petri nets. Theoretical Computer Science 243(1-2), 409–447 (2000)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of Different Semantics for Time Petri Nets. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 293–307. Springer, Heidelberg (2005) (to appear)
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) (to appear)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets (2005), Research Report IRCCyN R2005-2 available at http://www.lamsade.dauphine.fr/~haddad/publis.html
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)
Cassez, F., Roux, O.H.: Structural Translation of Time Petri Nets into Timed Automata. In: Huth, M. (ed.) Workshop on Automated Verification of Critical Systems (AVoCS 2004). Electronic Notes in Computer Science, Elsevier, Amsterdam (August 2004)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, Springer, Heidelberg (1989)
Haar, S., Simonot-Lion, F., Kaiser, L., Toussaint, J.: Equivalence of Timed State Machines and safe Time Petri Nets. In: Proceedings of WODES 2002, Zaragoza, Spain, pp. 119–126 (2002)
Lime, D., Roux, O.H.: State class timed automaton of a time Petri net. In: PNPM 2003, September 2003, IEEE Computer Society Press, Los Alamitos (2003)
Merlin, P.M.: A study of the recoverability of computing systems. Ph.D thesis, University of California, Irvine, CA (1974)
Pezzé, M., Young, M.: Time Petri Nets: A Primer Introduction. In: Tutorial presented at the Multi-Workshop on Formal Methods in Performance Evaluation and Applications, Zaragoza, Spain (September 1999)
Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Ph.D thesis, Massachusetts Institute of Technology, Cambridge, MA (1974)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H. (2005). When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_22
Download citation
DOI: https://doi.org/10.1007/11590156_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30495-1
Online ISBN: 978-3-540-32419-5
eBook Packages: Computer ScienceComputer Science (R0)