2024-06-26

We provide a finite equational presentation of graphs of treewidth at most three, solving an instance of an open problem by Courcelle and Engelfriet.
We use a syntax generalising series-parallel expressions, denoting graphs with a small interface. We introduce appropriate notions of connectivity for such graphs (components, cutvertices, separation pairs). We use those concepts to analyse the structure of graphs of treewidth at most three, showing how they can be decomposed recursively, first canonically into connected parallel components, and then non-deterministically. The main difficulty consists in showing that all non-deterministic choices can be related using only finitely many equational axioms.

We are motivated by explaining the behavioural inequivalence of two states in a finite transition system. Since good explanations are usually concise, our goal is to compute minimal distinguishing behaviour. We use the Hennessy-Milner logic (HML) to express behavioural properties. An HML formula that is satisfied in exactly one of the states is called a distinguishing formula, since it contains behaviour exhibited by one state but not the other. Our goal is to compute a minimal distinguishing formula.
In this talk we show by a reduction to CNF-SAT that computing a minimal distinguishing formula is NP-complete. We relate this result to the earlier algorithms that compute distinguishing formulas that are somewhat minimal. We conclude by showing that we can improve upon the known methods. By using the older inductive notion of bisimilarity we obtain minimal observation-depth, and negation-depth formulas in polynomial time. An implementation shows that the generated formulas are useful as witness even for larger transition systems.

[1] J.J.M. Martens and J.F. Groote. Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. CONCUR 2023, LIPIcs vol. 279.

Among the most celebrated results in category theory is the Lawvere-Linton correspondence theorem relating equational theories in the sense of universal algebra, the algebraic theories of Lawvere, and finitary monads on the category of sets. In this talk, we discuss an extension of the monad-theory part of this correspondence to the setting of graded monads, a generalization of monads given by a stratification of the monad structure in a monoidal category. In detail, we will describe a notion of graded equational theory along with a graded variant of Birkhoff's equational logic. This will allow the formulation of a syntactic characterization of finitary graded monads on sets. Time permitting, I will indicate some details on how graded equational theories can be adapted to the setting of locally presentable categories (e.g. posets, metric spaces, nominal sets, etc.).