The Temporal Logic of Appearance and Disappearance

Bauer, Jörg and Toben, Tobe and Westphal, Bernd
Reports of SFB/TR 14 AVACS
An interesting class of systems is characterised by a changing and potentially unbounded number of processes. Prominent instances are ad-hoc networks, dynamic communication systems, and object-oriented programs. Properties of such systems are naturally specified by predicative variants of temporal logic. So a number of logics have been proposed. However, the proposals are inconsistent among each other and lack a common understanding of the underlying systems. In this article, we comprehensively identify features whose characteristics determine the design of such logics. Given dynamic object creation and destruction, it turns out that the most crucial feature is that of disappearance. That is, how does a formula evaluate if its actors disappear? While some approaches avoid this problem at all, we propose a generalised logic subsuming the existing ones. We show that our proposal conservatively extends propositional temporal logic and conduct first investigations of emerging new issues of such temporal logics.
06 / 2007