Relational Dualities and Bisimulation

TL;DR

This paper extends categorical dualities to relations like bisimulations, linking system relations with predicate relations via relational extensions of Tarski and Thomason dualities.

Contribution

It introduces relational extensions of classical dualities, connecting well-behaved system relations with predicate relations, and sketches a related proof system.

Findings

Constructed relational extensions of Tarski and Thomason dualities.

Established correspondence between system relations and predicate relations.

Outlined a proof system relating formulae across different systems.

Abstract

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.