Helle Hvid Hansen

Automata admitting at most one accepting run per structure, known as unambiguous automata, find applications in verification of reactive systems as they extend the class of deterministic automata whilst maintaining some of their desirable properties. In this paper, we generalise a classical construction of unambiguous automata from thin trees to thin coalgebras for analytic functors. This achieves two goals: extending the existing construction to a larger class of structures, and providing conceptual clarity and parametricity to the construction by formalising it in the coalgebraic framework. As part of the construction, we link automaton acceptance of languages of thin coalgebras to language recognition via so-called coherent algebras, which were previously introduced for studying thin coalgebras. This link also allows us to establish an automata-theoretic characterisation of languages recognised by finite coherent algebras.

We show that Propositional Dynamic Logic (PDL) has the Craig Interpolation Property. This question has been open for many years. Three proof attempts were published, but later criticized in the literature or retracted. Our proof is based on the main ideas from Borzechowski (1988). We define a cyclic tableau system for PDL with a loading mechanism to recognize successful repeats. For this system, we show soundness and completeness via a game. To show interpolation, we modify Maehara's method to work for tableaux with repeats: we first define pre-interpolants at each node, and then use a quasi-tableau to define interpolants for clusters (strongly connected components). In different terms, our method solves the fixpoint equations that characterize the desired interpolants, and the method ensures that the solutions to these equations can be expressed within PDL. The proof is constructive and we show how to compute interpolants. We also make available a Haskell implementation of the proof system that provides interpolants. Lastly, we mention ongoing work to formally verify this proof in the interactive theorem prover Lean, and several questions for future work.

Composite theories are the algebraic equivalent of distributive laws. In this paper, we delve into the details of this correspondence and concretely show how to construct a composite theory from a distributive law and vice versa. Using term rewriting methods, we also describe when a minimal set of equations axiomatises the composite theory.