1994 | ReviewPaper | Buchkapitel
Liveness in timed and untimed systems
verfasst von : Rainer Gawlick, Roberto Segala, Jørgen Søgaard-Andersen, Nancy Lynch
Erschienen in: Automata, Languages and Programming
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.