|Title:|| A TEMPORAL LOGIC FOR PROVING PROPERTIES OF TOPOLOGICALLY GENERAL EXECUTIONS.
|Authors:|| R. Ben-Eliyahu and M. Magidor
We present a generalization of the temporal propositional logic of linear time which is useful for stating and proving properties of the generic execution sequence of a parallel program or a non-deterministic program. The formal system we present is exactly the same as the third of three logics presented in [LS82], but we give it a different semantics. The models are tree models of arbitrary size similar to those used in branching time temporal logic. The formulation we use allows us to state properties of ``co-meagre'' family of paths, where the term ``co-meagre'' refers to a set whose complement is of the first category in Baire's classification, looking at the set of paths in the model as a metric space. Our system is decidable, sound and complete for models of arbitrary size, but it has the finite model property, namely every sentence having a model has a finite model.
|Copyright||The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information|
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/1994/CS/CS0795), rather than to the URL of the PDF files directly. The latter URLs may change without notice.
To the list of the CS technical reports of 1994
To the main CS technical reports page
Computer science department, Technion