Transition systems are often used to describe the behaviour of software systems. If viewed as a graph then, at their most basic level, vertices correspond to the states of a program and each edge represents a transition between states via the (atomic) action labelled. In this setting, systems are thought to be consistent so that at each state formulas are evaluated as either True or False. On the other hand, when a structure of this sort - for example a map where states represent locations, some local properties are known and labelled transitions represent information available about different routes - is built resorting to multiple sources of information, it is common to find inconsistent or incomplete information regarding what holds at each state, both at the level of propositional variables and transitions. This paper aims at bringing together Belnap's four values, Dynamic Logic and hybrid machinery such as nominals and the satisfaction operator, so that reasoning is still possible in face of contradicting evidence. Proof-theory for this new logic is explored by means of a terminating, sound and complete tableaux system.

翻译：迁移系统常被用于描述软件系统的行为。若将其视为图结构，则在最基本层面上，顶点对应程序状态，每条边表示通过（原子）动作标记实现的状态间迁移。在此设定下，系统被认为是一致的，使得每个状态中的公式求值结果非真即假。另一方面，当这种结构——例如将状态视为位置的地图，其中已知某些局部属性，标记迁移表示不同路径的可用信息——基于多源信息构建时，常会遇到关于各状态命题变量和迁移的不一致或不完整信息。本文旨在融合贝尔纳普四值逻辑、动态逻辑以及混合机制（如名义词和满足算子），使得在存在矛盾证据时推理仍可进行。通过一个可终止、可靠且完备的表列系统，本文探索了这一新逻辑的证明论。