Analysis of timed processes with data using algebraic transformations

In this paper, we outline a method to describe and analyze real-time systems using timed μCRL. Most descriptions of such systems contain operators such as parallel composition that complicate analysis. As a first step towards the analysis of such systems, we linearize the given description using the algorithm from the work of Usenko (2002). The result is a timed linear process equation (TLPE) which is equivalent to the original description and has a very simple structure. Next, we outline how a TLPE can be transformed into an LPE, i.e., a linear process equation without time. This transformation, called time-free abstraction, has been used for non-recursive timed μCRL processes in the work of Rieners et al. (2002). Crucial for this transformation is that the TLPE is transformed into a well-timed TLPE. Finally, all time-stamping is captured in the parameters of atomic actions. The result is an LPE for which the machinery of untimed μCRL can be put to use for further analysis. These are based on symbolic analysis of the specifications, such as invariants, term rewriting and theorem proving, or on explicit state space generation and model-checking.