Analysis of three hybrid systems in timed uCRL

We study three simple hybrid control systems in timed $mu$CRL cite{Gr97. 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 $mu$CRL seems to allow detailed analysis and verification of hybrid systems. The operators for parallelism and encapsulation are handled using some basic results from cite{GvW98. It turns out that the expansion and encapsulation of a parallel composition of processes generally leads to a considerable number of potential {it 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 cite{BG94, have to be employed to master these complications.