Hierarchical hybrid logic

We introduce HHL, a hierarchical variant of hybrid logic. We study first order correspondence results and prove a Hennessy-Milner like theorem relating (hierarchical) bisimulation and modal equivalence for HHL. Combining hierarchical transition structures with the ability to refer to specific states...

Full description

Bibliographic Details
Main Author: Madeira, Alexandre Leite Castro (author)
Other Authors: Neves, Renato Jorge Araújo (author), Martins, Manuel A. (author), Barbosa, L. S. (author)
Format: article
Language:eng
Published: 2018
Subjects:
Online Access:http://hdl.handle.net/1822/69278
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/69278
Description
Summary:We introduce HHL, a hierarchical variant of hybrid logic. We study first order correspondence results and prove a Hennessy-Milner like theorem relating (hierarchical) bisimulation and modal equivalence for HHL. Combining hierarchical transition structures with the ability to refer to specific states at different levels, this logic seems suitable to express and verify properties of hierarchical transition systems, a pervasive semantic structure in Computer Science.