Timed verification with muCRL

muCRL is a process algebraic language for specification and verification of distributed systems. muCRL allows to describe temporal properties of distributed systems but it has no explicit reference to time. In this work we propose a manner of introducing discrete time without extending the language. The semantics of discrete time we use makes it possible to reduce the time progress problem to the diagnostics of 'no action is enabled' situations. The synchronous nature of the language facilitates the task. We show some experimental verification results obtained on a timed communication protocol.