Model checking birth and death

Abstract

This paper proposes Allocational Temporal Logic (AℓℓTL) as a formalism to express properties concerning the dynamic allocation (birth) and de-allocation (death) of entities, such as the objects in an object-based system. The logic is interpreted on History-Dependent Automata, extended with a symbolic representation for certain cases of unbounded allocation. The paper also presents a simple imperative language with primitive statements for (de)allocation, with an operational semantics, to illustrate the kind of behaviour that can be modelled. The main contribution of the paper is a tableau-based model checking algorithm for AℓℓTL, along the lines of Lichtenstein and Pnueli's algorithm for LTL.