Unifying Theories of Time with Generalised Reactive Processes

Simon David Foster; Ana Lucia Caneca Cavalcanti; JAMES Charles Paul Woodcock; Frank Zeyda

doi:10.1016/j.ipl.2018.02.017

Unifying Theories of Time with Generalised Reactive Processes

Simon David Foster, Ana Lucia Caneca Cavalcanti, JAMES Charles Paul Woodcock, Frank Zeyda

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

Hoare and He’s theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.

Original language	English
Pages (from-to)	47-52
Number of pages	6
Journal	Information Processing Letters
Volume	135
Early online date	23 Feb 2018
DOIs	https://doi.org/10.1016/j.ipl.2018.02.017
Publication status	Published - Jul 2018

Bibliographical note

Keywords

cs.LO
cs.FL

Access to Document

10.1016/j.ipl.2018.02.017

grproc
© Elsevier, 2018. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.
Accepted author manuscript, 282 KBLicence: CC BY-NC-ND

https://arxiv.org/abs/1712.10213

Cite this

@article{0ec252f436bb440abb9c29a6450081af,

title = "Unifying Theories of Time with Generalised Reactive Processes",

abstract = "Hoare and He{\textquoteright}s theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.",

keywords = "cs.LO, cs.FL",

author = "Foster, {Simon David} and Cavalcanti, {Ana Lucia Caneca} and Woodcock, {JAMES Charles Paul} and Frank Zeyda",

note = "{\textcopyright} Elsevier, 2018. This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. ",

year = "2018",

month = jul,

doi = "10.1016/j.ipl.2018.02.017",

language = "English",

volume = "135",

pages = "47--52",

journal = "Information Processing Letters",

issn = "0020-0190",

publisher = "Elsevier",

}

TY - JOUR

T1 - Unifying Theories of Time with Generalised Reactive Processes

AU - Foster, Simon David

AU - Cavalcanti, Ana Lucia Caneca

AU - Woodcock, JAMES Charles Paul

AU - Zeyda, Frank

N1 - © Elsevier, 2018. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy.

PY - 2018/7

Y1 - 2018/7

N2 - Hoare and He’s theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.

AB - Hoare and He’s theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.

KW - cs.LO

KW - cs.FL

U2 - 10.1016/j.ipl.2018.02.017

DO - 10.1016/j.ipl.2018.02.017

M3 - Article

SN - 0020-0190

VL - 135

SP - 47

EP - 52

JO - Information Processing Letters

JF - Information Processing Letters

ER -