On the Hybrid Extension of CTL and CTL+

TL;DR

This paper explores the expressivity, succinctness, and complexity of hybrid extensions of CTL and CTL+ with variables, revealing their expressive power and computational limits.

Contribution

It demonstrates that hybrid CTL+ with one variable is exponentially more succinct than hybrid CTL, and that multiple variables do not capture CTL* properties, with complexity results for satisfiability.

Findings

H1CTL+ and H1CTL are expressively equivalent.

H1CTL+ is exponentially more succinct than H1CTL.

Satisfiability for H1CTL+ is triply exponential time complete.

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.