Truth-as-Simulation: Towards a Coalgebraic Perspective on Logic and Games.211 Software Engineering

摘要

Building an the work of L. Moss on coalgebraic logic, I study in a general211u001esetting a class of infinitary modal logics for F-coalgebras, designed to capture 211u001esimulation and bisimulation. For a notion of coalgebraic simulation, I use the 211u001ework of A. Thijs on modeling simulation in terms of relators (extensions of SET-211u001efunctors along some family of preoders): simulation is the analogue for relators 211u001eof the notion of bisimulation for functors. I prove the logics introduced here 211u001ecan indeed capture coalgebraic simulation and bisimulation. Moreover, one can 211u001echaracterize any given coalgebra up to simulation (and, in certain conditions, up 211u001eto bisimulation) by a single sentence. An interesting feature of these logics is 211u001ethat their notion of truth or satisfaction can be understood as a simulation 211u001erelation itself, but with respect to a (relator associated to a) richer functor 211u001eF; moreover, truth is the largest simulation, i.e. the similarity relation 211u001ebetween states of the coalgebra and elements of the language. This sheds a new 211u001eperspective on the classical preservation and characterizability results, and 211u001ealso on logical games. The two kinds of games normally used in logic ('truth 211u001egames' to define the semantics dynamically, and 'similarity games' between two 211u001estructures) are seen to be the same kind of game at the level of coalgebras: 211u001esimulation games.