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

The process algebra for hybrid systems of Bergstra and Middelburg (2005) [6], called ACP(hs)(srt), 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 ACP(hs)(srt), by studying the most basic sub-algebra of ACP(hs)(srt) for which the time-determinism axiom fails: the Basic Process Algebra with Standard Relative Timing and Non-existence (BPA(perpendicular to)(srt)). We repair BPA(perpendicular to)(srt) in 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 BPA(hs)(srt). (c) 2012 Elsevier B.V. All rights reserved.