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.