This informal workshop brings together a group of researchers working on Kleene algebra and many-valued logic. The workshop takes place within the GRADLACT project run by Igor Sedlár.

Venue

Programme

Tuesday, 28 November

• 9:00–10:10 Georg Struth (University of Sheffield):
  Formalising Algebras for Higher-Dimensional Rewriting with a Proof Assistant
• 10:10–11:20 Tobias Kappé (University of Amsterdam and Open Universiteit):
  Completeness and the Finite Model Property for Kleene Algebra, Reconsidered Abstract
  

  Observations due to Pratt (1980) tell us that KA is complete w.r.t. relational models. A less known result due to Palka (2005) says that the same holds for finite models. These two results can be proved by leveraging Kozen’s result about the language model. Perhaps surprisingly, the implication is mutual: given that KA is complete w.r.t. finite (resp. relational) models, Palka’s (resp. Pratt’s) arguments show that it is complete w.r.t. the language model.

  We embark on a study of the different complete models of KA. This yields a fourth result subsuming those of Palka and Pratt, namely that KA is complete w.r.t. finite relational models. Next, we put an algebraic spin on Palka’s techniques, which yield an elementary proof of the finite model property, and by extension, of Kozen’s and Pratt’s theorems. In contrast with earlier approaches, this proof relies not on minimality or bisimilarity of automata, but rather on representing the regular expressions involved in terms of the transition monoid that they induce.

• 11:20–12:30 Brett McLean (Ghent University):
  Expressive Completeness for Operations on Partial Functions Abstract
  

  Algebras of partial functions are like algebras of binary relations except the elements of the algebras are partial functions. Of the many operations that these algebras have been equipped with, virtually all can be defined by a term in the signature of Tarski's relation algebras. Of course, we can only specify an operation in this way if it is guaranteed to yield a partial function when its arguments are partial functions.

  I will present results on the question of whether it is possible to find a finite set of these function-preserving operations that is complete in the sense that it can express any other function-preserving operation defined by a relation algebra term.

  The answer to this general question is no. However, if we restrict to "forward looking" operations, then there is an expressively complete set of four familiar operations: composition, intersection, antidomain, and preferential union. Similarly, for the analogous question about injective-partial-function preservation, a set of five operations is complete: composition, intersection, antidomain, inverse, and an "injective union" operation.

  (Joint work with Bart Bogaerts, Balder ten Cate, and Jan Van den Bussche.)

• 12:30–14:30 Lunch break
• 14:30–16:30 Discussion session
• 19:30– Workshop dinner

Wednesday, 29 November

• 10:10–11:20 Wolfgang Poiger (University of Luxembourg):
  Many-Valued Coalgebraic Logic: From Boolean Algebras to Semi-Primal Varieties Abstract
  

  We discuss how to lift algebra/coalgebra dualities (e.g., Jónsson-Tarski duality), as well as algebraic semantics of classical coalgebraic logics (e.g., classical modal logic) to a many-valued level. More specifically, we describe a canonical way to lift endofunctors on the variety of Boolean algebras to endofunctors on the variety generated by a semi-primal algebra (e.g., a finite MV-chain). We show that completeness and expressivity of the corresponding classical logics are preserved under this lifting, and give axiomatizations for the resulting varieties of many-valued modal algebras in certain cases.

• 11:20–12:30 Igor Sedlár (Czech Academy of Sciences):
  WedKAT: Kleene Algebra for Weighted Preconditions Abstract
  

  In weighted relational semantics of programs, costs of terminating runs are expressed in addition to their existence or absence. Weighted preconditions, a variant of a well known notion introduced by Dijkstra, express the least constly terminating run of a program that achieves some desired postcondition. We discuss a version of weighted Kleene algebra with tests and domain that is able to express weighted preconditions of programs.

• 12:30–14:30 Lunch break
• 14:30–16:30 Discussion session