Affiliations: Fakultät für Mathematik and Informatik, Universität Mannheim, 68131 Mannheim, Germany. [email protected] | School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT, UK. [email protected]
Note: [] Address for correspondence: Universität Bonn, Institut für Informatik I, Römerstr. 164, 53117 Bonn.
Note: [] Address for correspondence: Universität Bonn, Institut für Informatik I, Römerstr. 164, 53117 Bonn.
Abstract: The classification of properties of concurrent programs into safety and liveness was first proposed by Lamport [22]. Since then several characterizations of hierarchies of properties have been given, see e.g. [3, 20, 9, 21]; 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 [3]; Chang, Manna & Pnueli [9]; and Kwiatkowska, Peled & Penczek [21]. Syntactic characterizations of the properties in the hierarchy in terms of temporal logic are also studied.
Keywords: Temporal logic, partial order models, safety, liveness, response and persistence properties, topological characterization
