Unifying theories of time with generalised reactive processes

DOI10.1016/J.IPL.2018.02.017MaRDI QIDQ1708268zbMATH OpenOpenAlexFDO

Authors Simon Foster, Ana Cavalcanti, Frank Zeyda, Jim Woodcock

Publication date 5 April 2018

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1712.10213, https://eprints.whiterose.ac.uk/127797/1/grproc.pdf

zbMATH Keywords

hybrid systemsprocess algebratheorem provingformal semanticsunifying theories

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• scientific article; zbMATH DE number 67867
• Towards a general theory of action and time
• A theory of processes with durational actions
• A general perspective on time observables
• THE CATEGORY THEORY OF TIME SYSTEMS
• A path-integral approach to the problem of time
• Towards bridging time and causal reversibility
• Temporal causality in reactive systems
• scientific article; zbMATH DE number 2011635

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• A UTP semantics for \textsf{Circus}
• A formal model for a hybrid programming language
• An algebra of hybrid systems
• Building program construction and verification tools from algebraic principles
• Circus Time with Reactive Designs
• Process algebra for synchronous communication
• Termination of Real-Time Programs: Definitely, Definitely Not, or Maybe
• Towards a UTP semantics for Modelica
• Unifying heterogeneous state-spaces with lenses
• Unifying theories of programming that distinguish nontermination and abort

Cited in

(7)

• Automated verification of reactive and concurrent programs by calculation
• Unifying operational semantics with algebraic semantics for instantaneous reactions
• UTP semantics of reactive processes with continuations
• UTP, \textsf{\textit{Circus}}, and Isabelle
• A Unary Semigroup Trace Algebra
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• Unifying theories of reactive design contracts

Describes a project that uses

Uses Software

• Isabelle/HOL
• Circus

This page was built for publication: Unifying theories of time with generalised reactive processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1708268)