Branching-time property preservation between real-time systems

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

1 Citation (Scopus)


In the past decades, many formal frameworks (e.g. timed automata and temporal logics) and techniques (e.g. model checking and theorem proving) have been proposed to model a real-time system and to analyze real-time properties of the model. However, due to the existence of ineliminable timing differences between the model and its realization, real-time properties verified in the model often cannot be preserved in its realization. In this paper, we propose a branching representation (timed state tree) to specify the timing behavior of a system, based on which we prove that real-time properties represented by Timed CTL∗ (TCTL∗ in short) formulas can be preserved between two neighboring real-time systems. This paper extends the results in [1][2], such that a larger scope of real-time properties can be preserved between real-time systems.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings
EditorsSusanne Graf, Wenhui Zhang
Place of PublicationBerlin
Number of pages16
ISBN (Electronic)978-3-540-47238-4
ISBN (Print)3-540-47237-1, 978-3-540-47237-7
Publication statusPublished - 2006
Eventconference; ATVA 2006, Beijing, China; 2006-10-23; 2006-10-26 -
Duration: 23 Oct 200626 Oct 2006

Publication series

NameLecture Notes in Computer Science (LNCS)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conferenceconference; ATVA 2006, Beijing, China; 2006-10-23; 2006-10-26
OtherATVA 2006, Beijing, China


Dive into the research topics of 'Branching-time property preservation between real-time systems'. Together they form a unique fingerprint.

Cite this