×

Branching-depth hierarchies. (English) Zbl 1260.03034

Aceto, Luca (ed.) et al., EXPRESS’00: 7th international workshop on expressiveness in concurrency. Proceedings of the satellite workshop of CONCUR 2000, University Park, PA, USA, August 21, 2000. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 39, No. 1, 65-78 (2003).
Summary: We study the distinguishing and expressive power of branching temporal logics with bounded nesting depth of path quantifiers. We define the fragments CTL\(^{*}_{i}\) and CTL\(_{i}\) of CTL\(^{*}\) and CTL, where at most \(i\) nestings of path quantifiers are allowed. We show that for all \(i \geq 1\), the logic CTL\(^{*}_{i+1}\) has more distinguishing and expressive power than CTL\(^{*}_{i}\); thus the branching-depth hierarchy is strict. We describe equivalence relations \(H_{i}\) that capture CTL\(^{*}_{i}\): two states in a Kripke structure are \(H_{i}\)-equivalent iff they agree on exactly all CTL\(^{*}_{i}\) formulas. While \(H_{1}\) corresponds to trace equivalence, the limit of the sequence \(H_{1}, H_{2},\ldots\) is Milner’s bisimulation. These results are not surprising, but they give rise to several interesting observations and problems. In particular, while CTL\(^{*}\) and CTL have the same distinguishing power, this is not the case for CTL\(^{*}_{i}\) and CTL\(_{i}\). We define the branching depth of a structure as the minimal index \(i\) for which \(H_{i+1}=H_{i}\). The branching depth indicates on the possibility of using bisimulation instead of trace equivalence (and similarly for simulation and trace containment). We show that the problem of finding the branching depth is PSPACE-complete.
For the entire collection see [Zbl 1260.68009].

MSC:

03B44 Temporal logic
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDFBibTeX XMLCite
Full Text: DOI