Branching-time property preservation between real-time systems

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

1 Citaat (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.
Originele taal-2Engels
TitelAutomated Technology for Verification and Analysis
Subtitel4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings
RedacteurenSusanne Graf, Wenhui Zhang
Plaats van productieBerlin
Aantal pagina's16
ISBN van elektronische versie978-3-540-47238-4
ISBN van geprinte versie3-540-47237-1, 978-3-540-47237-7
StatusGepubliceerd - 2006
Evenementconference; ATVA 2006, Beijing, China; 2006-10-23; 2006-10-26 -
Duur: 23 okt 200626 okt 2006

Publicatie series

NaamLecture Notes in Computer Science (LNCS)
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349


Congresconference; ATVA 2006, Beijing, China; 2006-10-23; 2006-10-26
AnderATVA 2006, Beijing, China

Vingerafdruk Duik in de onderzoeksthema's van 'Branching-time property preservation between real-time systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit