A Logic for robotics? - Madeira, Alexandre (2015)
This paper introduces HHL, a hierarchical variant of hybrid logic. First-order correspondence and a Hennessy-Milner like theorem relating (hierarchical) bisimulation and logical equivalence for HHLare presented. Combining hierarchical transition structures with the ability to refer to specific states at any level of description, this logic seems suitable to express and verify properties of hierarchical transition systems, a pervasive semantic structure in Computer Science.