A logic for the specification of multi-object systems

Jan Broersen, Roel Wieringa

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

    42 Downloads (Pure)

    Abstract

    We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specication of systems that are conceptually described by a multitude of objects. The semantics and entailment properties of MODL are based on some a priori requirements for a modal multi-object specication logic. In an example specication of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. In this example we introduce the idea of identifying the concept of event-triggering, which is used in the graphical languages, with the concept of action implication (action calling) in MODL. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL.
    Original languageEnglish
    Title of host publicationFormal Methods for Open Object-Based Distributed Systems
    Subtitle of host publicationIFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)
    EditorsPaolo Ciancarini, Alessandro Fantechi, Robert Gorrieri
    Place of PublicationBoston, MA
    PublisherKluwer Academic Publishers
    Pages387-398
    Number of pages12
    ISBN (Electronic)978-0-387-35562-7
    ISBN (Print)978-1-4757-5266-3
    DOIs
    Publication statusPublished - Feb 1999
    Event3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999 - Florence, Italy
    Duration: 15 Feb 199918 Feb 1999
    Conference number: 3

    Publication series

    NameIFIP Advances in Information and Communication Technology
    PublisherKluwer Academic Publishers
    Volume10
    ISSN (Print)1868-4238
    ISSN (Electronic)1868-422X

    Conference

    Conference3rd IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 1999
    Abbreviated titleFMOODS
    CountryItaly
    CityFlorence
    Period15/02/9918/02/99

    Keywords

    • SCS-Services
    • Dynamic logic
    • Liveness property
    • Action symbol
    • State predicate
    • Intuitive meaning

    Fingerprint Dive into the research topics of 'A logic for the specification of multi-object systems'. Together they form a unique fingerprint.

    Cite this