Repairing time-determinism in the process algebra for hybrid systems ACPhssrt

The process algebra for hybrid systems of Bergstra and Middelburg (2005) [6], called ACPhssrt, is a well-known formalism for the specification of hybrid systems (i.e. systems in which discrete and continuous behavior both play a role). Recently, a number of errors have been found in it. Most importantly, the semantics chosen in [6] is such that the alternative composition (+) is not associative, and also the axiom of time-determinism (SRT3), together with some other axioms related to choice are violated. In this paper, we make a start in repairing ACPhssrt, by studying the most basic sub-algebra of ACPhssrt for which the time-determinism axiom fails: the Basic Process Algebra with Standard Relative Timing and Non-existence (BPA⊥srt). We repair BPA⊥srtin two different ways: by adapting the axioms to the semantics, and by adapting the semantics to the axioms. Furthermore, we extend these two solutions to (two versions of) the basic process algebra for hybrid systems BPAhssrt.