Abstraction and probabilities for hybrid logics

Abstract

We suggest and develop mathematical foundations for quantitative versions of hybrid logics by means of two related themes: a relational abstraction technique for hybrid computation tree logic and hybrid Kripke structures as an extension of the model-checking framework for computation tree logic with the ability to name, bind, and retrieve states; and a syntax and semantics for hybrid probabilistic computation tree logic over hybrid extensions of labelled Markov chains for which the relational abstraction techniques of hybrid Kripke structures should be transferable.