Model Checking Dynamic Allocation and Deallocation

    Research output: Book/ReportReportOther research output

    Abstract

    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)
    No.TR-CTIT-01-40
    ISSN (Print)1381-3625

    Keywords

    • EWI-5896
    • IR-63091

    Cite this

    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).