Powiadomienia systemowe
- Sesja wygasła!
- Sesja wygasła!
Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
The classification of properties of concurrent programs into safety and liveness was first proposed by Lamport. Since then several characterizations of hierarchies of properties have been given, see e.g.; this includes syntactic characterizations (in terms classes of formulas of logics such as the linear temporal logic) as well as extensional (as sets of computations in some abstract domain). The latter often admits a topological characterization with respect to the natural topologies of the domain of computations. We introduce a general notion of a linear time model of computation which consists of partial and completed computations satisfying certain axioms. The model is endowed with a natural topology. We show that the usual topologies on strings, Mazurkiewicz traces and pomsets arise as special cases. We then introduce a hierarchy of properties including safety, liveness, guarantee, response and persistence properties, and show that our definition subsumes the hierarchies of: Alpern & Schneider ; Chang, Manna & Pnueli; and Kwiatkowska, Peled & Penczek. Syntactic characterizations of the properties in the hierarchy in terms of temporal logic are also studied.
Wydawca
Czasopismo
Rocznik
Tom
Strony
259--294
Opis fizyczny
bibliogr. 35 poz.
Twórcy
autor
autor
- Universität Bonn, Institut für Informatik I, Römerstr. 164, 53117 Bonn, baier@informatik.uni-mannheim.de
Bibliografia
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS1-0007-0091