@inproceedings{48f5a8c64ee341bda787d08c34783a39,
title = "Decidability of timed language-inclusion for networks of real-time communicating sequential processes",
abstract = "An important verification problem for concurrent systems in general is that of establishing whether one system is a correct implementation, or refinement, of another system. For untimed systems, trace inclusion (or variants such as failure inclusion) is often used as a criterion of refinement. The natural extension of this criterion to timed systems is timed trace-inclusion. Unfortunately, this problem is undecidable for the commonly used model of timed automata (i.e. finite-state automata extended with clocks) due to the expressive power of the model. This is a serious obstacle to the application of automatic verification methods to timed automata. In this paper, we show that the problem of timed trace-inclusion is decidable for a large and natural class of processes in Reed and Roscoe{\textquoteright}s Timed CSP [RR86]. Essentially, this class includes static networks of processes with finite-control structure and real-valued clocks (modelled implicitly by a delay operator).",
author = "Wang Yi and Bengt Jonsson",
note = "Publisher Copyright: {\textcopyright} 1994, Springer Verlag. All rights reserved.; 14th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1994 ; Conference date: 15-12-1994 Through 17-12-1994",
year = "1994",
doi = "10.1007/3-540-58715-2\_129",
language = "英语",
isbn = "9783540587156",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "243--255",
editor = "P.S. Thiagarajan",
booktitle = "Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings",
address = "德国",
}