On topological hierarchies of temporal properties

• Autorzy: Baier Ch. , Kwiatkowska M.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

temporal logic; partial order models; safety; liveness; response and persistence properties; topological characterization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2000
• Tom: Vol. 41, Nr 3
• Strony: 259--294
• Opis fizyczny: bibliogr. 35 poz.

Twórcy

autor

Baier Ch.

autor

Kwiatkowska M.

• Universität Bonn, Institut für Informatik I, Römerstr. 164, 53117 Bonn,