Model Checking Dynamic Allocation and Deallocation

    Research output: Book/ReportReportOther research output


    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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Publication statusPublished - Dec 2001

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    ISSN (Print)1381-3625


    • EWI-5896
    • IR-63091

    Cite this