A really abstract concurrent model and its temporal logic

Abstract

In this paper we advance the radical notion that a computational model based on the <i>reals</i> provides a more abstract description of concurrent and reactive systems, than the conventional <i>integers</i> based behavioral model of execution <i>sequences.</i> The real model is studied in the setting of temporal logic, and we illustrate its advantages by providing a <i>fully abstract</i> temporal semantics for a simple concurrent language, and an example of verification of a concurrent program within the real temporal logic defined here. It is shown that, by imposing the crucial condition of <i>finite variability,</i> we achieve a balanced formalism that is insensitive to <i>finite</i> stuttering, but can recognize <i>infinite</i> stuttering, a distinction which is essential for obtaining a fully abstract semantics of non-terminating processes. Among other advantages, going into real-based semantics obviates the need for the controversial representation of concurrency by interleaving, and most of the associated fairness constraints.