@inproceedings{eca80fd3b5f144e097c705351841a34c,
title = "Branching-time property preservation between real-time systems",
abstract = "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.",
author = "J. Huang and M.C.W. Geilen and J.P.M. Voeten and H. Corporaal",
year = "2006",
doi = "10.1007/11901914_21",
language = "English",
isbn = "3-540-47237-1",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "260--275",
editor = "Susanne Graf and Wenhui Zhang",
booktitle = "Automated Technology for Verification and Analysis",
address = "Germany",
note = "conference; ATVA 2006, Beijing, China; 2006-10-23; 2006-10-26 ; Conference date: 23-10-2006 Through 26-10-2006",
}