hh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Modular Semantics for Transition System Specifications with Negative Premises
Swansea University, Swansea, Wales, United Kingdom. (Department of Computer Science)
Swansea University, Swansea, Wales, United Kingdom. (Department of Computer Science)
Halmstad University, School of Information Science, Computer and Electrical Engineering (IDE), Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES). Eindhoven University of Technology, Eindhoven, The Netherlands.ORCID iD: 0000-0002-4869-6794
2013 (English)In: Proceedings of the 24th International Conference on Concurrency Theory / [ed] Pedro R. D'Argenio & Hernán Melgratti, Heidelberg: Springer Berlin/Heidelberg, 2013, 46-60 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Heidelberg: Springer Berlin/Heidelberg, 2013. 46-60 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8052
Keyword [en]
Structural Operational Semantics, Well-Supported Proof, Conservative Extensions
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:hh:diva-23495DOI: 10.1007/978-3-642-40184-8_5Scopus ID: 2-s2.0-84882769400ISBN: 978-3-642-40183-1 ISBN: 978-3-642-40184-8 OAI: oai:DiVA.org:hh-23495DiVA: diva2:645854
Conference
24th International Conference on Concurrency Theory, CONCUR 2013, Buenos Aires, Argentina, 27–30 August 2013
Funder
eLLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications
Available from: 2013-09-05 Created: 2013-09-05 Last updated: 2014-11-11Bibliographically approved

Open Access in DiVA

fulltext(755 kB)96 downloads
File information
File name FULLTEXT01.pdfFile size 755 kBChecksum SHA-512
770c9edeeaa0459a5d345dace1c70e8c3572e48557b30147c9ed1d41f59adc78ab8be3da1537f0f46b2d0eab7cc59378140315dde88513b96a70139bc5966a03
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Mousavi, Mohammad Reza
By organisation
Centre for Research on Embedded Systems (CERES)
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 96 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 95 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf