Oberseminar (WiSe 2022/23)

In this talk, we take a look at the coalgebraic trace semantics for regular nominal nondeterministic Büchi automata (Büchi RNNAs), a form of nominal automata with name binding that accepts infinite words. We will present the outlines of the proof that the coalgebraic trace semantics for parity and Büchi automata defined by Urabe, Hasuo, and Shimizu coincides with the standard language semantics, which maps a state in a Büchi RNNA to its accepting ω-bar language. The proof itself is based on equational systems for fixed points on complete lattices.

In model theory, first-order logic is the standard language that is used when stating properties of relational systems, with universal and existential quantification allowing for a high level of expressiveness. This is not without cost, however, as validity of FOL formulae is undecidable. In the case where relational systems are understood as models of transition systems that come with a notion of successor state, however, FOL is often more expressive than needed. This has lead researchers to consider less expressive fragments of FOL that have more desirable algorithmic properties. Probably most importantly among these, modal logic restricts quantification to immediate successor states, which results in a less expressive logic that comes with a PSPACE decision procedure. Since its introduction, modal logic has been identified as the fragment of FOL that is invariant under bisimulations, meaning that not only is each modal formula bisimulation-invariant, but also that each bisimulation-invariant first-order formula is equivalent to a modal one, a result known as the van Benthem theorem.

In the past few years, the classical van Benthem theorem has been complemented with various new results characterizing the semantics of different flavours of modal logic within their corresponding ambient first-order logics. These results generalize from the original theorem by abstracting over the system type via coalgebras and over the domain of truth values via quantales. This talk will be a survey of the modal characterization theorems that arose as part of my research here at FAU.

An observer’s ability to distinguish different states of a system is heavily dependent on the observer’s ability to interact with and gather information about the system. We work in a quantitative setting, where, similar to the discrete setting, there is a vast number of behavioural distances for a given kind of state-based system. We transfer the framework of graded semantics to the category of metric spaces to establish generic quantitative semantics, as well as corresponding multi-valued modal logics. We provide a criterion for expressivity of the latter, and discuss the necessity of adaptations to the framework in comparison to previous instantiations The technical setup relies heavily on graded monads, which are, in metric spaces, induced by quantitative equational theories, in which equations are qualified by a margin of error. We instantiate these notions in relevant examples, either providing expressive logics, in which semantic distances are witnessed by formulae, or showihg their nonexistence. A stronger notion of expressivity is discussed, requiring any (homomorphism invariant) property of the semantics to be approximately expressible by a formula. We conclude with thoughts on how the failure of this stronger type of expressivity in prominent examples shapes our general approach.

Graded monads provide a framework for the abstraction of semantics for process equivalences and their characteristic logics via graded semantics, graded algebras and depth-1 theories. The aim of this talk is to give a digestible introduction to the core concepts, and plans for extending the semantics to include fixpoint logics, yielding more generality in their granularity.

In probabilistic learning there are two approaches: learning according to Pearl and learning according to Jeffrey. They are not clearly distinguished in the literature, but they can give quite different outcomes. This presentation will give both an overview of the topic and also explain the details in terms of operations in the Kleisli category of the (discrete) distribution monad.

For background information:

https://jair.org/index.php/jair/article/view/11349/26514

https://doi.org/10.4204/EPTCS.351.8

In this talk, we first introduce a particular kind of dcpo congruences, called natural ones, which are equivalence relations which make the quotient set of a dcpo into a dcpo with a specific order, called natural order, and also make the canonical surjections into dcpo maps.
Notice that dcpo congruences are not necessarily natural. In contrast to the case of algebraic structures, we found there that the image of a dcpo map need not be a quotient dcpo modulo natural congruences while this is true if we consider “strong” dcpo maps.

Then we move from natural dcpo congruences to dcpo congruences in a general setting. In order to characterize dcpo congruences, we introduce the concept of a pre-congruence relation, and characterize dcpo congruences as equivalence relations generated by pre-congruences.

Moreover, applying the notion of “directed kernel” for order-preserving maps, we give a characterization of pre-congruences as directed kernels of surjective dcpo maps. Furthermore,
we obtain the important result that the dcpo congruences are exactly kernels of surjective dcpo maps.

Although it is shown that the kernel of a non-surjective dcpo map need not be a dcpo congruence, we find a sufficient condition under which the kernel of a dcpo map is a dcpo congruence.
Finally, the Decomposition Theorem and its consequences for dcpo maps are obtained.

For details, please:

https://link.springer.com/article/10.1007/s00012-017-0424-5

https://www.sciencedirect.com/science/article/abs/pii/S0022404919300118