Relational Dualities and Bisimulation
For logicians and computer scientists studying relational structures and bisimulations, this provides a theoretical framework to connect system relations with logical predicates.
The paper extends categorical dualities between relational frames and algebras to relations, enabling a correspondence between bisimulations and relations between predicates. This yields a proof system for relating formulae across different systems.
The Kripke semantics of various logics arises via categorical dualities between a category of relational frames and their maps, and a category of algebras and logical homomorphisms. When the relational frames are considered as computational systems (e.g. the states of a machine), the corresponding algebra is one of logical predicates on these systems (e.g. predicates on these states, i.e. program logics). Our aim is to extend this phenomenon to relations, putting well-behaved relations between systems (e.g. bisimulations) in correspondence with relations between predicates. This is achieved by constructing particular relational extensions of Tarski duality (for infinitary classical propositional logic) and Thomason duality (for infinitary classical modal logic). We sketch how these dualities give rise to a proof system that relates formulae between different systems.