Who is pointing when to whom?

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    19 Citations (Scopus)

    Abstract

    This paper introduces an extension of linear temporal logic that allows to express properties about systems that are composed of entities (like objects) that can refer to each other via pointers. Our logic is focused on specifying properties about the dynamic evolution (such as creation, adaptation, and removal) of such pointer structures. The semantics is based on automata on infinite words, extended with appropriate means to model evolving pointer structures in an abstract manner. A tableau-based model-checking algorithm is proposed to automatically verify these automata against formulae in our logic.
    Original languageUndefined
    Title of host publicationFSTTCS 2004: foundations of software technology and theoretical computer science
    EditorsK. Lodaya, M. Mahajan
    Place of PublicationBerlin
    PublisherSpringer
    Pages250-262
    ISBN (Print)3-540-24058-6
    Publication statusPublished - 16 Dec 2004

    Publication series

    Name
    NumberXVI
    Volume3328
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • METIS-221294

    Cite this

    Distefano, D. S., Katoen, J. P., & Rensink, A. (2004). Who is pointing when to whom? In K. Lodaya, & M. Mahajan (Eds.), FSTTCS 2004: foundations of software technology and theoretical computer science (pp. 250-262). Berlin: Springer.