A refinement-based process algebra for timed automata

Stefano Cattani, Marta Kwiatkowska

Research output: Contribution to journalArticle

9 Citations (Scopus)


We propose a real-time extension to the process algebra CSR Inspired by timed automata, a very successful formalism for the specification and verification of real-time systems, we handle real time by means of clocks, i.e. real-valued variables that increase at the same rate as time. This differs from the conventional approach based on timed transitions. We give a discrete trace and failures semantics to our language and define the resulting refinement relations. One advantage of our proposal is that it is possible to automatically verify refinement relations between processes. We demonstrate how this can be achieved and under which conditions.
Original languageEnglish
Pages (from-to)138-159
Number of pages22
JournalFormal Aspects of Computing
Issue number2
Publication statusPublished - 1 Aug 2005


Dive into the research topics of 'A refinement-based process algebra for timed automata'. Together they form a unique fingerprint.

Cite this