Model Checking Birth and Death
Dino Distefano, Arend Rensink, Joost-Pieter Katoen · 2002
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. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.