The anchored version of the temporal framework

Abstract

In this survey paper we present some of the recent developments in the temporal formal system for the specification, verification and development of reactive programs. While the general methodology remains very much the one presented in some earlier works on the subject, such as [MP83c,MP83a,Pnu86], there have been several technical improvements and gained insights in understanding the computational model, the logic itself, the proof system and its presentation, and connections with alternative formalisms, such as finite automata. In this paper we explicate some of these improvements and extensions. The main difference between this and preceding versions is that here we consider a notion of validity for temporal formulae, which is anchored at the initial state of the computation. The paper discusses some of the consequences of this decision.