Abstract
The paper presents results of ongoing work aiming at the unification of some behavioural description formalisms for timed systems.
We propose for ATP a very general semantics in terms of a time domain.
It is then shown how ATP can be translated into a variant of timed graphs. This result allows the application of existing model-checking techniques to ATP.
Finally, we propose a notion of hybrid systems as a generalisation of timed graphs. Such systems can evolve, either by executing a discrete transition, or by performing some “continuous” transformation.
The formalisms studied admit the same class of models: time deterministic and time continuous, possibly infinitely branching transition systems labelled by actions or durations.
Work supported by the ESPRIT BRA SPEC
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of the fifth annual IEEE symposium on Logic In Computer Science, pages 414–425, Philadelphia, PA., June 1990.
G. Berry and L. Cosserat. The Esterel synchronous programming language and its mathematical semantics. In LNCS 197: Proceedings CMU Seminar on Concurrency, Springer-Verlag, 1985.
J.A. Bergstra and J.W. Klop. Algebra of Communicating Processes. Technical Report CS-R8420, Centre for Mathematics and Computer Science, Amsterdam, the Netherlands, 1984.
J.A. Bergstra and J.W. Klop. Process algebra: specification and verification in bisimulation semantics. In M. Hazewinkel, J.K. Lenstra, and L.G.L.T. Meertens, editors, Proceedings of the CWI Symposium Mathematics and Computer Science II (CWI Monograph 4), pages 61–94, North Holland, Amsterdam, 1986.
F. Moller and C. Tofts. A Temporal Calculus of Communicating Processes. In J.C.M. Baeten and J.W. Klop, editors, LNCS 458. Proceedings of CONCUR '90 (Theories of Concurrency: Unification and Extension), Amsterdam, the Netherlands, pages 401–415, Springer-Verlag, August 1990.
X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron. ATP: an Algebra for Timed Processes. In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990.
X. Nicollin and J. Sifakis. The algebra of timed processes ATP: theory and application. Technical Report RT-C26, LGI-IMAG, Grenoble, Prance, December 1990.
G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Århus University. Computer Science Department, Århus, Denmark, 1981.
Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, LNCS 458. Proceedings of CONCUR '90 (Theories of Concurrency: Unification and Extension), Amsterdam, the Netherlands, pages 502–520, Springer-Verlag, August 1990.
Wang Yi. CCS + Time = an Interleaving Model for Real Time Systems. In Proceedings of ICALP '91, Madrid, Spain, July 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nicollin, X., Sifakis, J., Yovine, S. (1992). From ATP to timed graphs and hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032007
Download citation
DOI: https://doi.org/10.1007/BFb0032007
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55564-3
Online ISBN: 978-3-540-47218-6
eBook Packages: Springer Book Archive