The lattice of congruences of a finite line frame

C. Areces, M. Campercholi, D. Penazzi, and P. Sánchez Terraf. The lattice of congruences of a finite line frame. Journal of Logic and Computation, 27(8):2653–2688, 2017.

Download

[pdf] 

Abstract

Let F = (F, R) be a finite Kripke frame. A congruence of F is a bisimulation of F that is also an equivalence relation on F. The set of all congruences of F is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that F is a finite line frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence rho, the interval [Id_F, rho] embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute.

BibTeX

@Article{Areces2017b,
  author =       "C. Areces and M. Campercholi and D. Penazzi and P.
                 S{\'a}nchez Terraf",
  journal =      "Journal of Logic and Computation",
  title =        "The lattice of congruences of a finite line frame",
  year =         "2017",
  number =       "8",
  pages =        "2653--2688",
  volume =       "27",
  abstract =     "Let F = (F, R) be a finite Kripke frame. A congruence
                 of F is a bisimulation of F that is also an equivalence
                 relation on F. The set of all congruences of F is a
                 lattice under the inclusion ordering. In this article
                 we investigate this lattice in the case that F is a
                 finite line frame. We give concrete descriptions of the
                 join and meet of two congruences with a nontrivial
                 upper bound. Through these descriptions we show that
                 for every nontrivial congruence rho, the interval
                 [Id_F, rho] embeds into the lattice of divisors of a
                 suitable positive integer. We also prove that any two
                 congruences with a nontrivial upper bound permute.",
  bibsource =    "dblp computer science bibliography, https://dblp.org",
  biburl =       "https://dblp.org/rec/journals/logcom/ArecesCPT17.bib",
  doi =          "10.1093/logcom/exx026",
  timestamp =    "Tue, 02 Jan 2018 16:25:27 +0100",
  URL =          "https://doi.org/10.1093/logcom/exx026",
}