No Cover Image

Conference Paper/Proceeding/Abstract 1041 views

Modular semantics for transition system specifications with negative premises

Martin Churchill, Peter Mosses Orcid Logo, Mohammad Reza Mousavi

CONCUR 2013 – Concurrency Theory, Volume: 8052, Pages: 46 - 60

Swansea University Author: Peter Mosses Orcid Logo

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1007/978-3-642-40184-8_5

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 specificati...

Full description

Published in: CONCUR 2013 – Concurrency Theory
Published: Berlin Heidelberg Springer 2013
URI: https://cronfa.swan.ac.uk/Record/cronfa17525
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2014-03-25T02:30:08Z
last_indexed 2019-02-11T19:06:18Z
id cronfa17525
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-02-11T15:47:30.3223105</datestamp><bib-version>v2</bib-version><id>17525</id><entry>2014-03-24</entry><title>Modular semantics for transition system specifications with negative premises</title><swanseaauthors><author><sid>3f13b8ec315845c81d371f41e772399c</sid><ORCID>0000-0002-5826-7520</ORCID><firstname>Peter</firstname><surname>Mosses</surname><name>Peter Mosses</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2014-03-24</date><deptcode>FGSEN</deptcode><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 &#x2013; 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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>CONCUR 2013 &#x2013; Concurrency Theory</journal><volume>8052</volume><paginationStart>46</paginationStart><paginationEnd>60</paginationEnd><publisher>Springer</publisher><placeOfPublication>Berlin Heidelberg</placeOfPublication><keywords/><publishedDay>31</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2013</publishedYear><publishedDate>2013-08-31</publishedDate><doi>10.1007/978-3-642-40184-8_5</doi><url/><notes/><college>COLLEGE NANME</college><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-02-11T15:47:30.3223105</lastEdited><Created>2014-03-24T09:44:49.1199650</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Martin</firstname><surname>Churchill</surname><order>1</order></author><author><firstname>Peter</firstname><surname>Mosses</surname><orcid>0000-0002-5826-7520</orcid><order>2</order></author><author><firstname>Mohammad Reza</firstname><surname>Mousavi</surname><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2019-02-11T15:47:30.3223105 v2 17525 2014-03-24 Modular semantics for transition system specifications with negative premises 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false 2014-03-24 FGSEN 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. Conference Paper/Proceeding/Abstract CONCUR 2013 – Concurrency Theory 8052 46 60 Springer Berlin Heidelberg 31 8 2013 2013-08-31 10.1007/978-3-642-40184-8_5 COLLEGE NANME Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2019-02-11T15:47:30.3223105 2014-03-24T09:44:49.1199650 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Martin Churchill 1 Peter Mosses 0000-0002-5826-7520 2 Mohammad Reza Mousavi 3
title Modular semantics for transition system specifications with negative premises
spellingShingle Modular semantics for transition system specifications with negative premises
Peter Mosses
title_short Modular semantics for transition system specifications with negative premises
title_full Modular semantics for transition system specifications with negative premises
title_fullStr Modular semantics for transition system specifications with negative premises
title_full_unstemmed Modular semantics for transition system specifications with negative premises
title_sort Modular semantics for transition system specifications with negative premises
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter Mosses
author Peter Mosses
author2 Martin Churchill
Peter Mosses
Mohammad Reza Mousavi
format Conference Paper/Proceeding/Abstract
container_title CONCUR 2013 – Concurrency Theory
container_volume 8052
container_start_page 46
publishDate 2013
institution Swansea University
doi_str_mv 10.1007/978-3-642-40184-8_5
publisher Springer
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2013-08-31T03:20:15Z
_version_ 1763750565667405824
score 11.014067

Similar Items