Analysis of three hybrid systems in timed μCRL

We study three simple hybrid control systems in timed μCRL . A temperature regulation system, a bottle filling system and a railway gate control system are specified component-wise and expanded to linear process equations. Some basic properties of the systems are analysed and a few correctness requirements are proven to be satisfied. Although not designed for this purpose, timed μCRL seems to allow detailed analysis and verification of hybrid systems. The operators for parallelism and encapsulation are handled using some basic results from . It turns out that the expansion and encapsulation of a parallel composition of processes generally leads to a considerable number of potential time deadlocks, which generally turn out to be harmless. Also inherent to parallelism are the multiple time dependencies between the summands of the separate components. As a consequence, expansions tend to lead to large numbers of terms. Various techniques, such as the use of invariants , have to be employed to master these complications.