Modular semantics for transition system specifications with negative premises

M. Churchill, P.D. Mosses, M.R. Mousavi

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

    1 Citation (Scopus)

    Abstract

    Transition rules with negative premises are needed in the structural operational semantics of programming and specification constructs such as priority and interrupt, as well as in timed extensions of specification languages. The well-known proof-theoretic semantics for transition system specifications involving such rules is based on well-supported proofs for closed transitions. Dealing with open formulae by considering all closed instances is inherently non-modular – proofs are not necessarily preserved by disjoint extensions of the transition system specification. Here, we conservatively extend the notion of well-supported proof to open transition rules. We prove that the resulting semantics is modular, consistent, and closed under instantiation. Our results provide the foundations for modular notions of bisimulation such that equivalence can be proved with reference only to the relevant rules, without appealing to all existing closed instantiations of terms.
    Original languageEnglish
    Title of host publicationCONCUR 2013 - Concurrency Theory (24th International Conference on Concurrency Theory, Buenos Aires, Argentina, August 27-30, 2013. Proceedings)
    EditorsP.R. D'Argenio, H. Melgratti
    Place of PublicationBerlin
    PublisherSpringer
    Pages46-60
    ISBN (Print)978-3-642-40183-1
    DOIs
    Publication statusPublished - 2013

    Publication series

    NameLecture Notes in Computer Science
    Volume8052
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Modular semantics for transition system specifications with negative premises'. Together they form a unique fingerprint.

    Cite this