Verification of networks of timed automata using mCRL2

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


It has been our long time wish to combine the best parts of the real-time verification methods based on timed automata (TA) (the use of regions and zones), and of the process-algebraic approach of languages like LOTOS and timed muCRL. This could provide us with additional verification possibilities for real-time systems, not available in existing timed-automata-based tools like UPPAAL. In this paper we extend the applicability of such discretization to extensions of TA available in UPPAAL as networks of timed automata and shared variables. To this end, we make use of mCRL2, the newer version of muCRL that includes time and multi-actions. The multi-actions are used to model the simultaneous access to shared variables and action synchronization.
Original languageEnglish
Title of host publicationProceedings 22nd IEEE International Parallel and Distributed Processing Symposium (IPDPS 2008, Miami FL, USA, April 14-18, 2008)
Place of PublicationPiscataway NJ
PublisherInstitute of Electrical and Electronics Engineers
ISBN (Print)978-1-4244-1693-6
Publication statusPublished - 2008


Dive into the research topics of 'Verification of networks of timed automata using mCRL2'. Together they form a unique fingerprint.

Cite this