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

formal semanticshybrid systemsprocess algebratheorem provingunifying 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

• A formal model for a hybrid programming language
• A UTP semantics for \textsf{Circus}
• An algebra of hybrid systems
• Building program construction and verification tools from algebraic principles
• Circus Time with Reactive Designs
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• 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)

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

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)