A temporal logic for proving properties of topologically general executions (Q1917070)

When considering correctness and termination of (possibly infinite) computations of nondeterministic or parallel programs, usually one restricts the attention to particular kinds of computation (e.g., fair ones) with the implicit assumption that they represent the more ``generic'' case. \textit{D. Lehmann} and \textit{S. Shelah} [Inf. Control 53, 165-198 (1982; Zbl 0523.03016)] proposed a formal system based on temporal logics which allows one to prove properties of probabilistic programs, when these properties hold for ``most'' (in the probabilistic sense) computations. In this paper, the authors reinterpret such a formal system by considering a different semantics for it, which is based on the topological notion of ``co-meagre'' set of computation paths. This provides an adequate formalization of the concept of ``generic'' computation, since the ``meagre'' set is well known to topologists as an adequate formalization of the notion of ``exceptional'' or ``non-generic''. The authors prove that the system defined by Lehmann and Shelah is sound and complete for this topological interpretation, thus obtaining a system which can be used for reasoning about properties of ``generic'' computations of non-deterministic or parallel programs. Another interesting fact is that the system has the finite model property, namely every sentence having a model (in general a tree model of arbitrary size) has a finite model.