School of Computing

A Semantics of Simultaneous Events (SSE) for State-Based Formal Specification

Chris Taylor and David Till

Formal Aspects of Computing, pages 182-196, September 2000 (Submitted to journal, currently being refereed.).

Abstract

Simple state-based models use events corresponding to sets of prestate, poststate pairs of system states, and solve the frame problem --- i.e. knowing what else has changed, given that an event has occurred --- by assuming non-concurrent events that uniquely determine the poststate. However, such events are `overspecified' and thus not reusable in other models. This paper describes a more flexible approach to state-based concurrency and the frame problem, in which events --- loosely specified in semantic terms --- may occur simultaneously and can be reused in different contexts without `promotion'.

Download publication 411 kbytes (PostScript)

Bibtex Record

@article{1125,
author = {Chris Taylor and David Till},
title = {A {S}emantics of {S}imultaneous {E}vents ({SSE}) for {S}tate-{B}ased {F}ormal {S}pecification},
month = {September},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {(Submitted to journal, currently being refereed.)},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/1125},
    journal = {Formal Aspects of Computing},
    publication_type = {article},
    submission_id = {20986_970754147},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014