Unifying Theories of Time with Generalised Reactive Processes.

Hoare and He's theory of reactive processes provides a unifying foundationfor the formal semantics of concurrent and reactive languages. Though highlyapplicable, their theory is limited to models that can express event historiesas discrete sequences. In this paper, we show how their theory can begeneralised by using an abstract trace algebra. We show how the algebra,notably, allows us to also consider continuous-time traces and therebyfacilitate models of hybrid systems. We then use this algebra to reconstructthe theory of reactive processes in our generic setting, and provecharacteristic laws for sequential and parallel processes, all of which havebeen mechanically verified in the Isabelle/HOL proof assistant.