Repairing time-determinism in the process algebra for hybrid systems (Q442292)

Hybrid systems model continuous entities, like temperature, and related discrete events, like switching a heater on and off. ACP-srt-hs is a language for describing hybrid systems. It has an operational semantics that describes how the state of a system evolves as time passes and as a consequence of discrete events. It also has an axiomatic semantics which facilitates proving that two expressions describe the same behaviour. This paper finds, and to a large extent fixes, mismatches between these two semantics. ACP-srt-hs can be thought of as consisting of layers, with a basic process algebra (without parallel composition and hiding) at the bottom, then time and an ``inconsistency'' process added to it, then continuous variables, and finally the rest. The inconsistency process models situations where the set of constraints is unsatisfiable. At the second layer, the choice between two processes, each of which first idles time \(t\), proves not equivalent to a process which first idles time t and then makes the choice, in contradiction with an explicit axiom. This problem is solved in two alternative ways: by modifying the axiom when at least one of the processes can evolve to the inconsistency process as time passes, and by making future inconsistency explicit in the semantics while keeping the axiom unchanged. At the third layer, choice between three processes is not associative, if two branches are guarded by contradicting constraints. This is solved in two alternative ways, one for each solution on layer two. Extending the solutions to the top layer are left for future work, partly because of technical difficulties and partly because of the need to first better understand (and perhaps choose between?) the two alternative solutions on lower layers. On the other hand, the paper discusses additional, less fundamental problems in ACP-srt-hs and mentions other ideas towards solving the two main issues. The conclusion discusses the problems of avoiding similar language design flaws in the future and gaining trust that a language is free from such flaws: ``So far, all we have been able to do [\(\ldots\)] is accompany our proposed repair with proofs. But those proofs are tedious, detailed, and frankly boring to read. So much so, that even the most dedicated reader of our work will have trouble to go through them all. On an honest note, we therefore feel those proofs mainly served to convince ourselves.'' I agree with these remarks. I would like to add that these problems are common in the field, but most other papers simply ignore them. The conclusion continues the discussion for almost a page and makes many valuable points.