Hybrid Branching-Time Logics

We introduce and study an extension of the well-known and well-studied branching-time logics CTL, CTL+, FCTL+, CTL* and the modal μ-calculus with the so called "hybrid framework". This framework borrows ideas from first-order logic to enable more precise "structural" reasoning which is known to be impossible in the original logics. In particular, the extension with this framework enables these logics to uniquely name, reference and test for certain states, similarly to the concepts of variables and constants in first-order logic. We especially study the decision procedures of these new hybrid branching-time logics -- especially their model checking problems -- and develop their model theory based on the already well-established model theory of the underlying branching-time logics. We establish a hybrid branching-time hierarchy that ranks these new hybrid branching-time logics with respect to their expressive power and in doing so provide a clear understanding of what can and cannot be expressed in any of these logics and also characterise some of the limits of their expressive power. Also, we present a complete analysis of the respective model checking problems of these hybrid branching-time logics. We present model checking algorithms, analyse their complexity and provide matching lower bounds showing that our algorithms are optimal from a complexity-theoretical point of view. Mostly, the model checking problems of the hybrid logics tend to have a slightly harder model checking problem than their non-hybrid counterparts with some exceptions like HCTLss which only has a PSPACE-complete model checking problem -- the same complexity as for CTL. We also show that this increase in computational complexity mostly comes from the unbounded use of names and disappears if we limit the number of names that can be used. Lastly, we show that all these hybrid logics have an undecidable satisfiability problem and provide some still decidable fragments of these hybrid branching-time logics.