Binders for Switch Graphs Specification
摘要
Switch graphs, as proposed by Marcelino and Gabbay are relation-changing state transition structures which make use of higher-level directed edges (edges connecting edges) to represent how the accessibility relation changes. In previous work, the same authors propose an hybrid logic to describe such systems. In this work we consider a variant of hybrid logic that excludes nominals and considers state-variables, and we explore how this logic can be used to describe these structures, in particular, higher-level edges. Afterwards, we define two classes of behavioural equivalence and discuss their utility and limitation with some examples.