Regular Processes and Timed Automata

TitleRegular Processes and Timed Automata
Publication TypeConference Proceedings
Year of Conference1997
AuthorsD'Argenio, PR
EditorBertran, M, Rus, T
Conference NameTransformation-Based Reactive Systems Development, 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, Palma, Mallorca, Spain, May 21-23, 1997, Proceedings
Series TitleLecture Notes in Computer Science
Volume1231
Pagination141-155
PublisherSpringer
ISBN Number3-540-63010-4
AbstractIn [DB96], an algebra for timed automata has been introduced. In this article, we introduce a syntactic characterisation of finite timed automata in terms of that process algebra. We show that regular processes, i.e., processes defined using finitely many guarded recursive equations, are as expressive as finite timed automata. The proof uses only the axiom system and unfolding of recursive equations. Since the proofs are basically algorithms, we also provide an effective method to translate from one model into the other. A remarkable corollary of these proofs is that regular recursive specifications may need one clock less than timed automata in order to represent the same process.
DOI10.1007/3-540-63010-4_10
PDF (Full text):