A complete axiomatisation for timed automata

Huimin Lin, Wang Yi

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

Abstract

In this paper we present a complete proof system for timed automata. It extends our previous axiomatisation of timed bisimulation for the class of loop-free timed automata with unique fixpoint induction. To our knowledge, this is the first algebraic theory for the whole class of timed automata with a completeness result, thus fills a gap in the theory of timed automata. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value–passing processes.

Original languageEnglish
Title of host publicationFST TCS 2000
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 20th Conference, Proceedings
EditorsSanjiv Kapoor, Sanjiva Prasad
PublisherSpringer Verlag
Pages277-289
Number of pages13
ISBN (Print)3540414134, 9783540414131
DOIs
StatePublished - 2000
Externally publishedYes
Event20th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2000 - New Delhi, India
Duration: 13 Dec 200015 Dec 2000

Publication series

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

Conference

Conference20th Conference on Foundations of Software Technology and Theoretical Computer Science, FST TCS 2000
Country/TerritoryIndia
CityNew Delhi
Period13/12/0015/12/00

Fingerprint

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

Cite this