This paper proposes Allocational Temporal Logic (ATL) 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 demonstrate the kind of behaviour that can be modelled. The main contribution of the paper is a tableau-based model checking algorithm for ATL, along the lines of Lichtenstein and Pnueli's algorithm for LTL.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Publication status||Published - Dec 2001|
|Name||CTIT technical report series|
|Publisher||University of Twente, Centre for Telematics and Information Technology (CTIT)|
Distefano, D. S., Rensink, A., & Katoen, J. P. (2001). Model Checking Dynamic Allocation and Deallocation. (CTIT technical report series; No. TR-CTIT-01-40). Enschede: Centre for Telematics and Information Technology (CTIT).