Abstract
We present a coordinated pair of general labeled transition system models for describing timed and untimed concurrent systems. Both of the models incorporate liveness properties as well as safety properties. The models are related via an embedding of the untimed model into the timed model, which preserves all the interesting attributes of the untimed model. Both models include notions of environment-freedom, which express the idea that the liveness properties can be guaranteed by the system, independently of the behavior of the environment in which it operates. These environment-freedom conditions are used to prove compositionality results for both models. This pair of models, which generalize several existing models, is intended to comprise a general formalism for the verification of timed and untimed concurrent systems.
Full report appears as [8]. Supported by NSF grant CCR-92-25124, DARPA contract N00014-92-J-4033, ONR contract N00014-91-J-1046, and by the Danish Technical Research Council.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In [5], pages 1–27.
M. Abadi and L. Lamport. Composing specifications. TOPLAS, 15(1):73–132, 1993.
B. Alpern and F. Schneider. Defining liveness. IPL, 21(4):181–185, 1985.
Proceedings of CONCUR 92, Stony Brook, NY, USA, LNCS 630, 1992.
Proceedings of the REX Workshop “Real-Time: Theory in Practice”, LNCS 600, 1991.
F. Dederichs and R. Weber. Safety and liveness from a methodological point of view. Information Processing Letters, 36(1):25–30, 1990.
D. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1988.
R. Gawlick, R. Segala, J. Søgaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Technical Report MIT/LCS/TR-587, November 1993.
Butler Lampson. Principles for computer system design, 1993. Turing Award Talk.
N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. PODC, 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.
N. Lynch and F. Vaandrager. Forward and backward simulations — part I: Untimed systems. Technical Report MIT/LCS/TM-486, May 1993. Preliminary version in [5].
N. Lynch and F. Vaandrager. Forward and backward simulations — part II: Timing-based systems. Technical Report MIT/LCS/TM-487, September 1993. Preliminary version in [5].
M. Merritt, F. Modugno, and M. Tuttle. Time constrained automata. In Proceedings CONCUR 91, Amsterdam, LNCS 527, 1991.
N. Reingold, D. Wang, and L. Zuck. Games I/O automata play. In [4], pages 325–339.
J. Søgaard-Andersen, B. Lampson, and N. Lynch. Correctness of at-most-once message delivery protocols. In Proc. FORTE 93, 1993.
J. Søgaard-Andersen, N. Lynch, and B. Lampson. Correctness of communication protocols, a case study. Technical Report MIT/LCS/TR-589, November 1993.
F. Vaandrager and N. Lynch. Action transducers and timed automata. In [4].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gawlick, R., Segala, R., Søgaard-Andersen, J., Lynch, N. (1994). Liveness in timed and untimed systems. In: Abiteboul, S., Shamir, E. (eds) Automata, Languages and Programming. ICALP 1994. Lecture Notes in Computer Science, vol 820. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58201-0_66
Download citation
DOI: https://doi.org/10.1007/3-540-58201-0_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58201-4
Online ISBN: 978-3-540-48566-7
eBook Packages: Springer Book Archive