A proof system for timed automata

Huimin Lin, Wang Yi

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

6 Scopus citations

Abstract

A proof system for timed automata is presented, based on a CCS-style language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgments of the proof system are conditional equations of the form θ ▷ t = u where θ is a clock constraint and t, u are terms denoting timed automata. It is proved that the proof system is complete for timed bisimulation over the recursion-free subset of the language. The completeness proof relies on the notion of symbolic timed bisimulation. The axiomatisation is also extended to handle an important variation of timed automata where each node is associated with an invariant constraint.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures - Third International Conference, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
EditorsJerzy Tiuryn
PublisherSpringer Verlag
Pages208-222
Number of pages15
ISBN (Print)3540672575, 9783540672579
DOIs
StatePublished - 2000
Externally publishedYes
Event3rd International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 - Berlin, Germany
Duration: 25 Mar 20002 Apr 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1784 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
Country/TerritoryGermany
CityBerlin
Period25/03/002/04/00

Fingerprint

Dive into the research topics of 'A proof system for timed automata'. Together they form a unique fingerprint.

Cite this