View source for Publications:Modular Semantics for Transition System Specifications with Negative Premises

<div style='display: none'>
== Do not edit this section ==
</div>
{{PublicationSetupTemplate|Author=Martin Churchill, Peter D. Mosses, Mohammad Reza Mousavi
|PID=645854
|Name=Churchill, Martin (Swansea University, Swansea, Wales, United Kingdom) (Department of Computer Science);Mosses, Peter D. (Swansea University, Swansea, Wales, United Kingdom) (Department of Computer Science);Mousavi, Mohammad Reza [mohmou] (Högskolan i Halmstad [2804], Sektionen för Informationsvetenskap, Data– och Elektroteknik (IDE) [3905], Halmstad Embedded and Intelligent Systems Research (EIS) [3938], Centrum för forskning om inbyggda system (CERES) [6702]) (Eindhoven University of Technology, Eindhoven, The Netherlands)
|Title=Modular Semantics for Transition System Specifications with Negative Premises
|PublicationType=Conference Paper
|ContentType=Refereegranskat
|Language=eng
|Journal=
|JournalISSN=
|Status=
|Volume=
|Issue=
|HostPublication=Proceedings of the 24th International Conference on Concurrency Theory
|Conference=24th International Conference on Concurrency Theory, CONCUR 2013, Buenos Aires, Argentina, 27–30 August 2013
|StartPage=46
|EndPage=60
|Year=2013
|Edition=
|Pages=
|City=Heidelberg
|Publisher=Springer Berlin/Heidelberg
|Series=Lecture Notes in Computer Science ; 8052
|SeriesISSN=0302-9743
|ISBN=978-3-642-40183-1;978-3-642-40184-8
|Urls=
|ISRN=
|DOI=http://dx.doi.org/10.1007/978-3-642-40184-8_5
|ISI=
|PMID=
|ScopusId=2-s2.0-84882769400
|NBN=urn:nbn:se:hh:diva-23495
|LocalId=
|ArchiveNumber=
|Keywords=Structural Operational Semantics;Well-Supported Proof;Conservative Extensions
|Categories=Data- och informationsvetenskap (102)
|ResearchSubjects=
|Projects=
|Notes=
|Abstract=<p>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. © 2013 Springer-Verlag.</p>
|Opponents=
|Supervisors=
|Examiners=
|Patent=
|ThesisLevel=
|Credits=
|Programme=
|Subject=
|Uppsok=
|DefencePlace=
|DefenceLanguage=
|DefenceDate=
|CreatedDate=2013-09-05
|PublicationDate=2013-09-05
|LastUpdated=2013-11-12
|diva=http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:645854}}
<div style='display: none'>

== Keep all hand-made modifications below ==
</div>{{PublicationDisplayTemplate}}