@inproceedings{56943c1b5f5a4d78a9b3a4cb24699e43,
title = "Deciding properties of regular real timed processes",
abstract = "We discuss the decidability problem associated with verifying properties of processes expressed in the real time process calculus TCCS of [W90]. A regular subcalculus TC of TCCS is considered. Two operational semantics, and associated timed notions of bisimulation, are given: a standard infinite semantics, and a symbolic finite semantics. The consistency between the two semantics is proved. We show that both the equivalences are decidable for regular processes relative to comparisons between real numbers. As an alternative specification formalism, we present a timed modal logic. It turns out that this logic characterises timed bisimulation equivalence in the sense that equivalent processes enjoy exactly the same properties expressed within the logic. Moreover, we prove that the problem of deciding whether a given regular real timed process satisfies a given property of the logic is decidable, relative to first order assertions about real numbers. Two interpretations of the modal logic are offered, based on the standard and symbolic operational semantics of TC respectively and the consistency between these interpretations is proved.",
author = "Uno Holmer and Kim Larsen and Wang Yi",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1992.; 3rd International Workshop on Computer Aided Verification, CAV 1991 ; Conference date: 01-07-1991 Through 04-07-1991",
year = "1992",
doi = "10.1007/3-540-55179-4\_41",
language = "英语",
isbn = "9783540551799",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "443--453",
editor = "Larsen, \{Kim G.\} and Arne Skou",
booktitle = "Computer Aided Verification - 3rd Intenational Workshop, CAV 1991, Proceedings",
address = "德国",
}