Permutable bisimulation equivalences of Kripke frames

MIGUEL CAMPERCHOLI; DANIEL PENAZZI; PEDRO SÁNCHEZ TERRAF

Lima

Congreso; Congreso Latinoamericano de Álgebra; 2014

One reason for the failure of Beth?s definability theorem on (modal) logics is that there are new connectives ?algebraically? definable. That is, in the variety of dual objects (Boolean algebras with operators, BAOs) there are algebraic functions that are not terms of the variety. Algebraic functions are those defined systems of equations having unique solutions in the variety. Our research program consists in studying algebraic functions of varieties of BAOs, first in the case with discriminator. For finitely many finite alge- bras, algebraic functions are essentially characterized as those preserved by intersection of subalgebras. Via the duality, we have to consider the struc- ture of all bisimulation equivalences of a Kripke frame with the operation of join. In this work in progress, we started studying a very small case, that of Kripke frames that are finite linear (symmetric) graphs L = {0, . . . , n}, R , where x R y iff |x − y| ≤ 1. Already in this case, the computation of the join is non trivial and shows a very interesting combinatorial behavior. Our main results are that all pairs of bisimulations having a join different from L × L permute and an explicit formula for calculating the cardinal of the quotient frame L/θ ∨ δ given some parameters of the bisimulations θ and δ.