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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Binders for Switch Graphs Specification

  • Daniel Figueiredo,
  • Alexandre Madeira

摘要

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.