Safety and Liveness for Trace Languages
LSV, ENS de Cachan, France.
Safety and Liveness are basic properties used in the specification of systems. In the sequential case, there are topological characterizations of these properties as well as syntactical characterizations in temporal logic. We extend these definitions and characterizations to concurrent systems that can described by Mazurkiewicz traces. Two extensions are proposed, depending on whether we are interested in global or local semantics