Analysis of Timed Processes with Data Using Algebraic Transformations

The language of timed µCRL is an extension of an ACP-style process algebra-based language µCRL with time-related features. In this paper we describe this language and its equational axiomatization, and give an example specification. We outline the method of simplifying transformations based on this equational axiomatization, and illustrate it on this This transformation method allows for a time-free abstraction of the specification, which in turn enables the use of tools and techniques for verification of untimed systems. We prove some properties of the example using a known invariants technique. Key words: Process Algebra, Real Time, Axioms, Verification.

• Type: Conference
• Year: 2005
• Where: TIME
• Authors: Michel A. Reniers, Yaroslav S. Usenko
• Keywords: Equational Axiomatization, Logical Reasoning, Process Algebra-based Language, TIME 2005, Timed µCRL