On the Hybrid Extension of CTL and CTL+
Abstract
The paper studies the expressivity, relative succinctness and complexity of satisfiability for hybrid extensions of the branching-time logics CTL and CTL+ by variables. Previous complexity results show that only fragments with one variable do have elementary complexity. It is shown that H1CTL+ and H1CTL, the hybrid extensions with one variable of CTL+ and CTL, respectively, are expressively equivalent but H1CTL+ is exponentially more succinct than H1CTL. On the other hand, HCTL+, the hybrid extension of CTL with arbitrarily many variables does not capture CTL*, as it even cannot express the simple CTL* property EGFp. The satisfiability problem for H1CTL+ is complete for triply exponential time, this remains true for quite weak fragments and quite strong extensions of the logic.
Cite
@article{arxiv.0906.2541,
title = {On the Hybrid Extension of CTL and CTL+},
author = {Ahmet Kara and Martin Lange and Thomas Schwentick and Volker Weber},
journal= {arXiv preprint arXiv:0906.2541},
year = {2015}
}