Oberseminar (SoSe 2023)

Unravelling the Power of Alternating Automata over Nominal Sets

The notion of alternation was initially introduced by Chandra, Kozen, and Stockmeyer in their seminal paper. Besides alternating Turing machines, their investigation encompasses alternating finite automata, in particular demonstrating their equivalence to classical NFA and DFA models. This talk aims to explore the utilisation of alternation in the context of regular nondeterministic nominal automata (RNNA). The development of RNNA was motivated by the need to recognise Bar Languages, which involve data languages where names can be bound for the remainder of the word. To address this, we introduce a novel automaton called the regular alternating nominal automaton (RANA) and delve into its semantics. We will analyse RANAs and their connection with the linear-time fixpoint logic Bar-μTL, which was introduced in a recent paper by Daniel, Lutz, and Stefan at MFCS 2021. Finally, we will conclude the talk with a brief overview of our ongoing and future research endeavours. More information:

• Bar-μTL Paper

Action Codes

This talk is about a joint paper with Frits Vaandrager (Radboud University, Nijmegen, NL) accepted for publication at ICALP 2023.We provide a new perspective on the problem how high-level state machine models with abstract actions can be related to low-level models in which these actions are refined by sequences of concrete actions. We describe the connection between high-level and low-level actions using action codes, a variation of the prefix codes known from coding theory. For each action code R, we introduce a contraction operator α_R that turns a low-level model M into a high-levelmodel, and a refinement operator ρR that transforms a high-level model N into a low-level model. We establish a Galois connection ρ_R(N) ⊑ M <=> N ⊑ α_R(M), where ⊑ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model M. To this end, we also introduce a concretization operator γ_R, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection α_R(M) ⊑ N <=> M ⊑ γ_R(N). Action codes may be used to construct adaptors that translate between concrete and abstract actions during learning and testing of Mealy machines. If Mealy machine M models a black-box system then αR(M) describes the behavior that can be observed by a learner/tester that Znteracts with this system via an adaptor derived from code R. Whenever α_R(M) implements (or conforms to) N, we may conclude that M implements (or conforms to) γ_R(N).Almost all results and examples are formalized in Coq. More information:

• Preprint on Arxiv
• Coq Formalization

Kleene Monads in a Long While

Notions of iteration range from the arguably most general Elgot iteration to a very specific Kleene iteration. The fundamental nature of Elgot iteration has been extensively explored by Bloom and Esik in the form of iteration theories, while Kleene iteration became extremely popular as an integral part of (untyped) formalisms, such as automata theory, regular expressions and Kleene algebra. Here, we establish a formal connection between Elgot iteration and Kleene iteration in the form of Elgot monads and Kleene monads, respectively. We also introduce a novel class of while-monads, which like Kleene monads admit a relatively simple description in purely algebraic terms, and like Elgot monads cover a large diversity of models that meaningfully support while-loops, but may fail to support a Kleene-style iteration operator altogether, or else fail the Kleene algebra laws.