Abstract
We present a process algebra suitable to the modelling of timed concurrent systems and to their efficient verification through model checking. The algebra is provided with two consistent semantics: a structural operational semantics (as usual for process algebras) and a denotational semantics in terms of Petri nets in which time is introduced through counters of explicit clock ticks. This way of modelling time has been called causal time so the process algebra is itself called the Causal Time Calculus (CTC). It was shown in a separate paper that the causal time approach allowed for efficient verification but suffered from a sensitivity to the constants to which counts of ticks are compared. We show in this paper how this weakness can be removed.
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
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2). Elsevier (1994)
Best, E., Devillers, R., Hall, J.: The Petri Box Calculus: a new causal algebra with multilabel communication. In: Rozenberg, G. (ed.) APN 1992. LNCS, vol. 609, Springer, Heidelberg (1992)
Bui Thanh, C., Klaudel, H., Pommereau, F.: Petri nets with causal time for system verification. In: MTCS 2002. Electronic Notes in Theoretical Computer Sciences, vol. 68.5, Elsevier, Amsterdam (2002)
Bui Thanh, C., Klaudel, H., Pommereau, F.: Box Calculus with Coloured Buffers. LACL Technical report (2002), Available at http://www.univ-paris12.fr/lacl
Corradini, F., D’Ortenzio, D., Inverardi, P.: On the relationship among four timed process algebras. Fundamenta Informaticae 34. IOS Press (1999)
D’Argenio, P.R.: Algebras and automata for real-time systems. PhD. Thesis, Department of Computer Science, University of Twente (1999)
Durchholz, R.: Causality, time, and deadlines. Data & Knowledge Engineering 6. North-Holland (1991)
Esparza, J.: Model checking using net unfoldings. Science of Computer Programming 23. Elsevier (1994)
Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 582. Springer, Heidelberg (2002)
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)
Koutny, M.: A compositional model of time Petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 303. Springer, Heidelberg (2000)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journalon Software Tools and Technology Transfer 1(1-2). Springer (1997)
Mäkelä, M.: MARIA: modular reachability analyser for algebraic system nets (1999), Online manual http://www.tcs.hut.fi/maria
Marroquín Alonzo, O., de Frutos Escrig, D.: Extending the Petri Box Calculus with time. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, p. 303. Springer, Heidelberg (2001)
Merlin, P.M., Farber, D.J.: Recoverability of communication protocols—implications of a theoretical study. IEEE Transaction on Communication 24. IEEE Society (1976)
Milner, R.: Communication and concurrency. Prentice Hall, Englewood Cliffs (1989)
Plotkin, G.D.: A Structural approach to Operational Semantics. Technical Report FN-19, Computer Science Department, University of Aarhus (1981)
Pommereau, F.: Causal Time Calculus. LACL Technical report (2002), Available at http://www.univ-paris12.fr/lacl
Ramchandani, C.: Analysis of asynchronous concurrent systems using Petri nets. PhD. Thesis, project MAC, MAC-TR 120. MIT (1974)
Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1/2). Springer (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pommereau, F. (2004). Causal Time Calculus. In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol 2791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40903-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-40903-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21671-1
Online ISBN: 978-3-540-40903-8
eBook Packages: Springer Book Archive