No Cover Image

Conference Paper/Proceeding/Abstract 496 views

Modular semantics for transition system specifications with negative premises / Martin Churchill; Peter Mosses; Mohammad Reza Mousavi

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

Swansea University Author: Peter, Mosses

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!
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.
College: College of Science
Start Page: 46
End Page: 60