Showing 1–50 of 60 results for author: König, B

ChemKANs for Combustion Chemistry Modeling and Acceleration

Authors: Benjamin C. Koenig, Suyong Kim, Sili Deng

Abstract: Efficient chemical kinetic model inference and application for combustion problems is challenging due to large ODE systems and wideley separated time scales. Machine learning techniques have been proposed to streamline these models, though strong nonlinearity and numerical stiffness combined with noisy data sources makes their application challenging. The recently developed Kolmogorov-Arnold Netwo… ▽ More Efficient chemical kinetic model inference and application for combustion problems is challenging due to large ODE systems and wideley separated time scales. Machine learning techniques have been proposed to streamline these models, though strong nonlinearity and numerical stiffness combined with noisy data sources makes their application challenging. The recently developed Kolmogorov-Arnold Networks (KANs) and KAN ordinary differential equations (KAN-ODEs) have been demonstrated as powerful tools for scientific applications thanks to their rapid neural scaling, improved interpretability, and smooth activation functions. Here, we develop ChemKANs by augmenting the KAN-ODE framework with physical knowledge of the flow of information through the relevant kinetic and thermodynamic laws, as well as an elemental conservation loss term. This novel framework encodes strong inductive bias that enables streamlined training and higher accuracy predictions, while facilitating parameter sparsity through full sharing of information across all inputs and outputs. In a model inference investigation, we find that ChemKANs exhibit no overfitting or model degradation when tasked with extracting predictive models from data that is both sparse and noisy, a task that a standard DeepONet struggles to accomplish. Next, we find that a remarkably parameter-lean ChemKAN (only 344 parameters) can accurately represent hydrogen combustion chemistry, providing a 2x acceleration over the detailed chemistry in a solver that is generalizable to larger-scale turbulent flow simulations. These demonstrations indicate potential for ChemKANs in combustion physics and chemical kinetics, and demonstrate the scalability of generic KAN-ODEs in significantly larger and more numerically challenging problems than previously studied. △ Less

Submitted 16 April, 2025; originally announced April 2025.

Comments: B.C.K. and S.K. contributed equally to this work. 23 pages, 8 figures, and 1 table

Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems (Full Version)

Authors: Barbara König, Arend Rensink, Lara Stoltenow, Fabian Urrigshardt

Abstract: This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing… ▽ More This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems. △ Less

Submitted 11 April, 2025; originally announced April 2025.

More on setwise climbability properties

Authors: Bernhard König, Yasuo Yoshinobu

Abstract: We introduce two types of variations of setwise climbability properties, which have been introduced by the second author as fragments of Jensen's square principles. We show that variations of the first type are equivalent to known principles and that they are consistent with the Proper Forcing Axiom(PFA). On the other hand, those of the second type can be characterized as Martin-type axioms for so… ▽ More We introduce two types of variations of setwise climbability properties, which have been introduced by the second author as fragments of Jensen's square principles. We show that variations of the first type are equivalent to known principles and that they are consistent with the Proper Forcing Axiom(PFA). On the other hand, those of the second type can be characterized as Martin-type axioms for some classes of posets defined in terms of a new variation of generalized Banach-Mazur games, and they are no longer consistent with PFA. We also study how large fragments of PFA are consistent with these principles. △ Less

Submitted 26 March, 2025; originally announced March 2025.

Comments: 27 pages

LeanKAN: A Parameter-Lean Kolmogorov-Arnold Network Layer with Improved Memory Efficiency and Convergence Behavior

Authors: Benjamin C. Koenig, Suyong Kim, Sili Deng

Abstract: The recently proposed Kolmogorov-Arnold network (KAN) is a promising alternative to multi-layer perceptrons (MLPs) for data-driven modeling. While original KAN layers were only capable of representing the addition operator, the recently-proposed MultKAN layer combines addition and multiplication subnodes in an effort to improve representation performance. Here, we find that MultKAN layers suffer f… ▽ More The recently proposed Kolmogorov-Arnold network (KAN) is a promising alternative to multi-layer perceptrons (MLPs) for data-driven modeling. While original KAN layers were only capable of representing the addition operator, the recently-proposed MultKAN layer combines addition and multiplication subnodes in an effort to improve representation performance. Here, we find that MultKAN layers suffer from a few key drawbacks including limited applicability in output layers, bulky parameterizations with extraneous activations, and the inclusion of complex hyperparameters. To address these issues, we propose LeanKANs, a direct and modular replacement for MultKAN and traditional AddKAN layers. LeanKANs address these three drawbacks of MultKAN through general applicability as output layers, significantly reduced parameter counts for a given network structure, and a smaller set of hyperparameters. As a one-to-one layer replacement for standard AddKAN and MultKAN layers, LeanKAN is able to provide these benefits to traditional KAN learning problems as well as augmented KAN structures in which it serves as the backbone, such as KAN Ordinary Differential Equations (KAN-ODEs) or Deep Operator KANs (DeepOKAN). We demonstrate LeanKAN's simplicity and efficiency in a series of demonstrations carried out across both a standard KAN toy problem and a KAN-ODE dynamical system modeling problem, where we find that its sparser parameterization and compact structure serve to increase its expressivity and learning capability, leading it to outperform similar and even much larger MultKANs in various tasks. △ Less

Submitted 24 February, 2025; originally announced February 2025.

Comments: 15 pages, 5 figures, and 1 table

Computing Approximated Fixpoints via Dampened Mann Iteration

Authors: Paolo Baldan, Sebastian Gurke, Barbara König, Tommaso Padoan, Florian Wittbold

Abstract: Fixpoints are ubiquitous in computer science and when dealing with quantitative semantics and verification one is commonly led to consider least fixpoints of (higher-dimensional) functions over the nonnegative reals. We show how to approximate the least fixpoint of such functions, focusing on the case in which they are not known precisely, but represented by a sequence of approximating functions t… ▽ More Fixpoints are ubiquitous in computer science and when dealing with quantitative semantics and verification one is commonly led to consider least fixpoints of (higher-dimensional) functions over the nonnegative reals. We show how to approximate the least fixpoint of such functions, focusing on the case in which they are not known precisely, but represented by a sequence of approximating functions that converge to them. We concentrate on monotone and non-expansive functions, for which uniqueness of fixpoints is not guaranteed and standard fixpoint iteration schemes might get stuck at a fixpoint that is not the least. Our main contribution is the identification of an iteration scheme, a variation of Mann iteration with a dampening factor, which, under suitable conditions, is shown to guarantee convergence to the least fixpoint of the function of interest. We then argue that these results are relevant in the context of model-based reinforcement learning for Markov decision processes (MDPs), showing that the proposed iteration scheme instantiates to MDPs and allows us to derive convergence to the optimal expected return. More generally, we show that our results can be used to iterate to the least fixpoint almost surely for systems where the function of interest can be approximated with given probabilistic error bounds, as it happens for probabilistic systems, such as simple stochastic games, that can be explored via sampling. △ Less

Submitted 15 January, 2025; originally announced January 2025.

Yangian Form-alism for Planar Gauge Theories

Authors: Niklas Beisert, Benedikt König

Abstract: In this article, we reconsider the formulation of Yangian symmetry for planar N=4 supersymmetric Yang-Mills theory, and we investigate to what extent this symmetry lifts to the beta/gamma-deformation of the model. We first apply cohomology of variational forms towards a thorough derivation of the invariance statement for the undeformed action from covariance of the equations of motion under the Ya… ▽ More In this article, we reconsider the formulation of Yangian symmetry for planar N=4 supersymmetric Yang-Mills theory, and we investigate to what extent this symmetry lifts to the beta/gamma-deformation of the model. We first apply cohomology of variational forms towards a thorough derivation of the invariance statement for the undeformed action from covariance of the equations of motion under the Yangian algebra. We then apply a twist deformation to these statements paying particular attention to cyclicity aspects. We find that the equations of motion remain covariant while invariance of the action only holds for the Yangian subalgebra that is uncharged under the twist. △ Less

Submitted 25 November, 2024; originally announced November 2024.

Comments: 27 pages

$\mathfrak{k}$-structure of basic representation of affine algebras

Authors: Benedikt König

Abstract: This article presents a new relation between the basic representation of split real simply-laced affine Kac-Moody algebras and finite dimensional representations of its maximal compact subalgebra $\mathfrak{k}$. We provide infinitely many $\mathfrak{k}$-subrepresentations of the basic representation and we prove that these are all the finite dimensional $\mathfrak{k}$-subrepresentations of the bas… ▽ More This article presents a new relation between the basic representation of split real simply-laced affine Kac-Moody algebras and finite dimensional representations of its maximal compact subalgebra $\mathfrak{k}$. We provide infinitely many $\mathfrak{k}$-subrepresentations of the basic representation and we prove that these are all the finite dimensional $\mathfrak{k}$-subrepresentations of the basic representation such that the quotient of the basic representation by the subrepresentation is a finite dimensional representation of a certain parabolic algebra and of the maximal compact subalgebra. By this result we provide an infinite composition series with a cosocle filtration of the basic representation. Finally, we present examples of the results and applications to supergravity. △ Less

Submitted 17 July, 2024; originally announced July 2024.

Comments: 45 + 11 pages

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

Authors: Lara Stoltenow, Barbara König, Sven Schneider, Andrea Corradini, Leen Lambers, Fernando Orejas

Abstract: We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a… ▽ More We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus. △ Less

Submitted 9 July, 2024; originally announced July 2024.

KAN-ODEs: Kolmogorov-Arnold Network Ordinary Differential Equations for Learning Dynamical Systems and Hidden Physics

Authors: Benjamin C. Koenig, Suyong Kim, Sili Deng

Abstract: Kolmogorov-Arnold networks (KANs) as an alternative to multi-layer perceptrons (MLPs) are a recent development demonstrating strong potential for data-driven modeling. This work applies KANs as the backbone of a neural ordinary differential equation (ODE) framework, generalizing their use to the time-dependent and temporal grid-sensitive cases often seen in dynamical systems and scientific machine… ▽ More Kolmogorov-Arnold networks (KANs) as an alternative to multi-layer perceptrons (MLPs) are a recent development demonstrating strong potential for data-driven modeling. This work applies KANs as the backbone of a neural ordinary differential equation (ODE) framework, generalizing their use to the time-dependent and temporal grid-sensitive cases often seen in dynamical systems and scientific machine learning applications. The proposed KAN-ODEs retain the flexible dynamical system modeling framework of Neural ODEs while leveraging the many benefits of KANs compared to MLPs, including higher accuracy and faster neural scaling, stronger interpretability and generalizability, and lower parameter counts. First, we quantitatively demonstrated these improvements in a comprehensive study of the classical Lotka-Volterra predator-prey model. We then showcased the KAN-ODE framework's ability to learn symbolic source terms and complete solution profiles in higher-complexity and data-lean scenarios including wave propagation and shock formation, the complex Schrödinger equation, and the Allen-Cahn phase separation equation. The successful training of KAN-ODEs, and their improved performance compared to traditional Neural ODEs, implies significant potential in leveraging this novel network architecture in myriad scientific machine learning applications for discovering hidden physics and predicting dynamic evolution. △ Less

Submitted 19 September, 2024; v1 submitted 4 July, 2024; originally announced July 2024.

Comments: B.C.K. and S.K. contributed equally to this work. 21 pages, 10 figures, and 4 tables. Updated after acceptance to journal

ACM Class: I.6.5; G.1.7

Journal ref: Computer Methods in Applied Mechanics and Engineering 432 (2024) 117397

Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques

Authors: Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, Paul Wild

Abstract: Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition system… ▽ More Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the category theoretic generalization of the Kantorovich lifting from transportation theory to the case of lifting functors to quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition, we describe how to lift distributive laws in the case where one of the two functors is polynomial (with finite coproducts). These results are essential ingredients for adapting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We illustrate the results of our paper in two case studies. △ Less

Submitted 23 July, 2024; v1 submitted 30 April, 2024; originally announced April 2024.

Journal ref: Published at CONCUR 2024

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

Authors: Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, Paul Wild

Abstract: We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out… ▽ More We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances). △ Less

Submitted 31 January, 2024; v1 submitted 9 October, 2023; originally announced October 2023.

Quantitative Graded Semantics and Spectra of Behavioural Metrics

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing

Abstract: Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable… ▽ More Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems. △ Less

Submitted 27 January, 2025; v1 submitted 2 June, 2023; originally announced June 2023.

MSC Class: 03B45; 03B52; 68Q85 ACM Class: F.4.1

A Monoidal View on Fixpoint Checks

Authors: Paolo Baldan, Richard Eggert, Barbara König, Timo Matt, Tommaso Padoan

Abstract: Fixpoints are ubiquitous in computer science as they play a central role in providing a meaning to recursive and cyclic definitions. Bisimilarity, behavioural metrics, termination probabilities for Markov chains and stochastic games are defined in terms of least or greatest fixpoints. Here we show that our recent work which proposes a technique for checking whether the fixpoint of a function is th… ▽ More Fixpoints are ubiquitous in computer science as they play a central role in providing a meaning to recursive and cyclic definitions. Bisimilarity, behavioural metrics, termination probabilities for Markov chains and stochastic games are defined in terms of least or greatest fixpoints. Here we show that our recent work which proposes a technique for checking whether the fixpoint of a function is the least (or the largest) admits a natural categorical interpretation in terms of gs-monoidal categories. The technique is based on a construction that maps a function to a suitable approximation. We study the compositionality properties of this mapping and show that under some restrictions it can naturally be interpreted as a (lax) gs-monoidal functor. This guides the development of a tool, called UDEfix that allows us to build functions (and their approximations) like a circuit out of basic building blocks and subsequently perform the fixpoints checks. We also show that a slight generalisation of the theory allows one to treat a new relevant case study: coalgebraic behavioural metrics based on Wasserstein liftings. △ Less

Submitted 12 May, 2025; v1 submitted 4 May, 2023; originally announced May 2023.

Interpretable Anomaly Detection via Discrete Optimization

Authors: Simon Lutz, Florian Wittbold, Simon Dierl, Benedikt Böing, Falk Howar, Barbara König, Emmanuel Müller, Daniel Neider

Abstract: Anomaly detection is essential in many application domains, such as cyber security, law enforcement, medicine, and fraud protection. However, the decision-making of current deep learning approaches is notoriously hard to understand, which often limits their practical applicability. To overcome this limitation, we propose a framework for learning inherently interpretable anomaly detectors from sequ… ▽ More Anomaly detection is essential in many application domains, such as cyber security, law enforcement, medicine, and fraud protection. However, the decision-making of current deep learning approaches is notoriously hard to understand, which often limits their practical applicability. To overcome this limitation, we propose a framework for learning inherently interpretable anomaly detectors from sequential data. More specifically, we consider the task of learning a deterministic finite automaton (DFA) from a given multi-set of unlabeled sequences. We show that this problem is computationally hard and develop two learning algorithms based on constraint optimization. Moreover, we introduce novel regularization schemes for our optimization problems that improve the overall interpretability of our DFAs. Using a prototype implementation, we demonstrate that our approach shows promising results in terms of accuracy and F1 score. △ Less

Submitted 24 March, 2023; originally announced March 2023.

ACM Class: F.4.3; I.2.6

Stochastic Decision Petri Nets

Authors: Florian Wittbold, Rebecca Bernemann, Reiko Heckel, Tobias Heindel, Barbara König

Abstract: We introduce stochastic decision Petri nets (SDPNs), which are a form of stochastic Petri nets equipped with rewards and a control mechanism via the deactivation of controllable transitions. Such nets can be translated into Markov decision processes (MDPs), potentially leading to a combinatorial explosion in the number of states due to concurrency. Hence we restrict ourselves to instances where ne… ▽ More We introduce stochastic decision Petri nets (SDPNs), which are a form of stochastic Petri nets equipped with rewards and a control mechanism via the deactivation of controllable transitions. Such nets can be translated into Markov decision processes (MDPs), potentially leading to a combinatorial explosion in the number of states due to concurrency. Hence we restrict ourselves to instances where nets are either safe, free-choice and acyclic nets (SAFC nets) or even occurrence nets and policies are defined by a constant deactivation pattern. We obtain complexity-theoretic results for such cases via a close connection to Bayesian networks, in particular we show that for SAFC nets the question whether there is a policy guaranteeing a reward above a certain threshold is $\mathsf{NP}^\mathsf{PP}$-complete. We also introduce a partial-order procedure which uses an SMT solver to address this problem. △ Less

Submitted 23 March, 2023; originally announced March 2023.

ACM Class: F.3.1

A Lattice-Theoretical View of Strategy Iteration

Authors: Paolo Baldan, Richard Eggert, Barbara König, Tommaso Padoan

Abstract: Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of compl… ▽ More Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min-, respectively, max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata. △ Less

Submitted 13 December, 2022; v1 submitted 20 July, 2022; originally announced July 2022.

Hennessy-Milner Theorems via Galois Connections

Authors: Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing

Abstract: We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of… ▽ More We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular this framework allows us to derive a new fixpoint characterization of directed trace metrics. △ Less

Submitted 14 January, 2023; v1 submitted 12 July, 2022; originally announced July 2022.

Probabilistic Systems with Hidden State and Unobservable Transitions

Authors: Rebecca Bernemann, Barbara König, Matthias Schaffeld, Torben Weis

Abstract: We consider probabilistic systems with hidden state and unobservable transitions, an extension of Hidden Markov Models (HMMs) that in particular admits unobservable ε-transitions (also called null transitions), allowing state changes of which the observer is unaware. Due to the presence of ε-loops this additional feature complicates the theory and requires to carefully set up the corresponding pro… ▽ More We consider probabilistic systems with hidden state and unobservable transitions, an extension of Hidden Markov Models (HMMs) that in particular admits unobservable ε-transitions (also called null transitions), allowing state changes of which the observer is unaware. Due to the presence of ε-loops this additional feature complicates the theory and requires to carefully set up the corresponding probability space and random variables. In particular we present an algorithm for determining the most probable explanation given an observation (a generalization of the Viterbi algorithm for HMMs) and a method for parameter learning that adapts the probabilities of a given model based on an observation (a generalization of the Baum-Welch algorithm). The latter algorithm guarantees that the given observation has a higher (or equal) probability after adjustment of the parameters and its correctness can be derived directly from the so-called EM algorithm. △ Less

Submitted 27 May, 2022; originally announced May 2022.

ACM Class: G.3

Graded Monads and Behavioural Equivalence Games

Authors: Chase Ford, Harsh Beohar, Barbara König, Stefan Milius, Lutz Schröder

Abstract: The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pe… ▽ More The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand. △ Less

Submitted 7 May, 2024; v1 submitted 29 March, 2022; originally announced March 2022.

Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic

Authors: H. Beohar, B. König, S. Küpper, C. Mika-Michalski

Abstract: We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an Eilenberg-Moore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from… ▽ More We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an Eilenberg-Moore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from a relation lifting (a special kind of indexed morphism) and we give a general recipe to construct such liftings in the above three cases. Lastly, we apply this framework to derive logical characterisations for (weighted) language equivalence and conditional bisimilarity. △ Less

Submitted 4 February, 2022; v1 submitted 19 October, 2021; originally announced October 2021.

Two-dimensional Cahn-Hilliard simulations for coarsening kinetics of spinodal decomposition in binary mixtures

Authors: Björn König, Olivier J. J. Ronsin, Jens Harting

Abstract: The evolution of the microstructure due to spinodal decomposition in phase separated mixtures has a strong impact on the final material properties. In the late stage of coarsening, the system is characterized by the growth of a single characteristic length scale $L\sim C t^α$. To understand the structure-property relationship, the knowledge of the coarsening exponent $α$ and the coarsening rate co… ▽ More The evolution of the microstructure due to spinodal decomposition in phase separated mixtures has a strong impact on the final material properties. In the late stage of coarsening, the system is characterized by the growth of a single characteristic length scale $L\sim C t^α$. To understand the structure-property relationship, the knowledge of the coarsening exponent $α$ and the coarsening rate constant $C$ is mandatory. Since the existing literature is not entirely consistent, we perform phase field simulations based on the Cahn-Hilliard equation. We restrict ourselves to binary mixtures using a symmetric Flory-Huggins free energy and a constant mobility term and show that the coarsening for off-critical mixtures is slower than the expected $t^{1/3}$-growth. Instead, we find $α$ to be dependent on the mixture composition and thus from the morphology. Finally, we propose a model to describe the complete coarsening kinetics including the rate constant $C$. △ Less

Submitted 15 July, 2021; originally announced July 2021.

Journal ref: Phys. Chem. Chem. Phys., 2021,23, 24823-24833

Fixpoint Theory -- Upside Down

Authors: Paolo Baldan, Richard Eggert, Barbara König, Tommaso Padoan

Abstract: Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related… ▽ More Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. In this paper we provide proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form $\mathbb{M}^Y$, where $Y$ is a finite set and $\mathbb{M}$ an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, metric transition systems, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games. △ Less

Submitted 6 June, 2023; v1 submitted 20 January, 2021; originally announced January 2021.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 2 (June 7, 2023) lmcs:8382

Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks

Authors: Rebecca Bernemann, Benjamin Cabrera, Reiko Heckel, Barbara König

Abstract: This paper exploits extended Bayesian networks for uncertainty reasoning on Petri nets, where firing of transitions is probabilistic. In particular, Bayesian networks are used as symbolic representations of probability distributions, modelling the observer's knowledge about the tokens in the net. The observer can study the net by monitoring successful and failed steps. An update mechanism for Ba… ▽ More This paper exploits extended Bayesian networks for uncertainty reasoning on Petri nets, where firing of transitions is probabilistic. In particular, Bayesian networks are used as symbolic representations of probability distributions, modelling the observer's knowledge about the tokens in the net. The observer can study the net by monitoring successful and failed steps. An update mechanism for Bayesian nets is enabled by relaxing some of their restrictions, leading to modular Bayesian nets that can conveniently be represented and modified. As for every symbolic representation, the question is how to derive information - in this case marginal probability distributions - from a modular Bayesian net. We show how to do this by generalizing the known method of variable elimination. The approach is illustrated by examples about the spreading of diseases (SIR model) and information diffusion in social networks. We have implemented our approach and provide runtime results. △ Less

Submitted 30 September, 2020; originally announced September 2020.

ACM Class: I.2.3; D.2.2

Conditional Bisimilarity for Reactive Systems

Authors: Mathias Hülsbusch, Barbara König, Sebastian Küpper, Lara Stoltenow

Abstract: Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with… ▽ More Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We consider examples based on DPO graph rewriting, an instantiation of reactive systems. △ Less

Submitted 11 January, 2022; v1 submitted 24 April, 2020; originally announced April 2020.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 12, 2022) lmcs:6937

Abstraction, Up-to Techniques and Games for Systems of Fixpoint Equations

Authors: Paolo Baldan, Barbara König, Tommaso Padoan

Abstract: Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express a number of verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract int… ▽ More Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express a number of verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract interpretation: a system over some concrete domain is abstracted to a system in a suitable abstract domain, with conditions ensuring that the abstract solution represents a sound/complete overapproximation of the concrete solution. Interestingly, up-to techniques, a classical approach used in coinductive settings to obtain easier or feasible proofs, can be interpreted as abstractions in a way that they naturally fit in our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can provide a characterisation of the solution of systems of fixpoint equations over complete lattices in terms of a suitable parity game, generalising some recent work that was restricted to continuous lattices. The game view opens the way to the development of on-the-fly algorithms for characterising the solution of such equation systems. △ Less

Submitted 18 June, 2021; v1 submitted 19 March, 2020; originally announced March 2020.

Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas

Authors: Barbara König, Christina Mika-Michalski, Lutz Schröder

Abstract: Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-… ▽ More Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-bisimilar states. The modalities required for the formula are also synthesized on-the-fly, and we present a recipe for re-coding the formula with different modalities, given by a separating set of predicate liftings. Both the game and the generation of the distinguishing formulas have been implemented in a tool called T-BEG. △ Less

Submitted 14 October, 2020; v1 submitted 26 February, 2020; originally announced February 2020.

Comments: Long version of CMCS 2020 paper

MSC Class: 03B70 ACM Class: F.4.1

A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

Authors: Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

Abstract: The fuzzy modality `probably` is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this ob… ▽ More The fuzzy modality `probably` is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that every formula in probabilistic fuzzy first-order logic that is non-expansive wrt. behavioural distance can be approximated by concepts of bounded rank in probabilistic fuzzy description logic. For a modal logic perspective on the same result, see arXiv:1810.04722. △ Less

Submitted 4 June, 2019; v1 submitted 31 May, 2019; originally announced June 2019.

Comments: arXiv admin note: text overlap with arXiv:1810.04722

MSC Class: 60A66; 68Q85; 03B45; 03B52 ACM Class: F.4.1; I.2.4

Rewriting Abstract Structures: Materialization Explained Categorically

Authors: Andrea Corradini, Tobias Heindel, Barbara König, Dennis Nolte, Arend Rensink

Abstract: The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in p… ▽ More The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in particular partial map classifiers, in a topos. Second, we introduce an extension by enriching objects with annotations and give a precise characterization of strongest post-conditions, which are effectively computable under certain assumptions. △ Less

Submitted 13 February, 2019; originally announced February 2019.

ACM Class: F.3.1; F.4.2

Fixpoint Games on Continuous Lattices

Authors: Paolo Baldan, Barbara König, Tommaso Padoan, Christina Mika-Michalski

Abstract: Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress measures, we develop a game-theoretical approach to the solution of systems of monotone equations over lattices, where for each single equation either the least or g… ▽ More Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress measures, we develop a game-theoretical approach to the solution of systems of monotone equations over lattices, where for each single equation either the least or greatest solution is taken. A simple parity game, referred to as fixpoint game, is defined that provides a correct and complete characterisation of the solution of equation systems over continuous lattices, a quite general class of lattices widely used in semantics. For powerset lattices the fixpoint game is intimately connected with classical parity games for $μ$-calculus model-checking, whose solution can exploit as a key tool Jurdziński's small progress measures. We show how the notion of progress measure can be naturally generalised to fixpoint games over continuous lattices and we prove the existence of small progress measures. Our results lead to a constructive formulation of progress measures as (least) fixpoints. We refine this characterisation by introducing the notion of selection that allows one to constrain the plays in the parity game, enabling an effective (and possibly efficient) solution of the game, and thus of the associated verification problem. We also propose a logic for specifying the moves of the existential player that can be used to systematically derive simplified equations for efficiently computing progress measures. We discuss potential applications to the model-checking of latticed $μ$-calculi and to the solution of fixpoint equations systems over the reals. △ Less

Submitted 19 April, 2021; v1 submitted 26 October, 2018; originally announced October 2018.

ACM Class: D.2.4; F.3.1; F.3.2

A van Benthem Theorem for Quantitative Probabilistic Modal Logic

Authors: Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

Abstract: In probabilistic transition systems, behavioural metrics provide a more fine-grained and stable measure of system equivalence than crisp notions of bisimilarity. They correlate strongly to quantitative probabilistic logics, and in fact the distance induced by a probabilistic modal logic taking values in the real unit interval has been shown to coincide with behavioural distance. For probabilistic… ▽ More In probabilistic transition systems, behavioural metrics provide a more fine-grained and stable measure of system equivalence than crisp notions of bisimilarity. They correlate strongly to quantitative probabilistic logics, and in fact the distance induced by a probabilistic modal logic taking values in the real unit interval has been shown to coincide with behavioural distance. For probabilistic systems, probabilistic modal logic thus plays an analogous role to that of Hennessy-Milner logic on classical labelled transition systems. In the quantitative setting, invariance of modal logic under bisimilarity becomes non-expansivity of formula evaluation w.r.t. behavioural distance. In the present paper, we provide a characterization of the expressive power of probabilistic modal logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that quantitative probabilistic modal logic lies dense in the bisimulation-invariant fragment, in the indicated sense of non-expansive formula evaluation, of quantitative probabilistic first-order logic; more precisely, bisimulation-invariant first-order formulas are approximable by modal formulas of bounded rank. For a description logic perspective on the same result, see arXiv:1906.00784. △ Less

Submitted 4 June, 2019; v1 submitted 10 October, 2018; originally announced October 2018.

MSC Class: 60A66; 68Q85; 03B45; 03B52 ACM Class: F.4.1; I.2.4

Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks

Authors: Benjamin Cabrera, Tobias Heindel, Reiko Heckel, Barbara König

Abstract: The paper extends Bayesian networks (BNs) by a mechanism for dynamic changes to the probability distributions represented by BNs. One application scenario is the process of knowledge acquisition of an observer interacting with a system. In particular, the paper considers condition/event nets where the observer's knowledge about the current marking is a probability distribution over markings. The o… ▽ More The paper extends Bayesian networks (BNs) by a mechanism for dynamic changes to the probability distributions represented by BNs. One application scenario is the process of knowledge acquisition of an observer interacting with a system. In particular, the paper considers condition/event nets where the observer's knowledge about the current marking is a probability distribution over markings. The observer can interact with the net to deduce information about the marking by requesting certain transitions to fire and observing their success or failure. Aiming for an efficient implementation of dynamic changes to probability distributions of BNs, we consider a modular form of networks that form the arrows of a free PROP with a commutative comonoid structure, also known as term graphs. The algebraic structure of such PROPs supplies us with a compositional semantics that functorially maps BNs to their underlying probability distribution and, in particular, it provides a convenient means to describe structural updates of networks. △ Less

Submitted 29 June, 2018; originally announced July 2018.

Comments: Accepted at CONCUR '18

Up-To Techniques for Behavioural Metrics via Fibrations

Authors: Filippo Bonchi, Barbara König, Daniela Petrisan

Abstract: Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their oundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of… ▽ More Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their oundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages. △ Less

Submitted 28 June, 2018; originally announced June 2018.

Comments: long version of our CONCUR 2018 paper

A van Benthem Theorem for Fuzzy Modal Logic

Authors: Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König

Abstract: We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with its modal fragment, and show that the fuzzy first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exac… ▽ More We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with its modal fragment, and show that the fuzzy first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exactly those that can be approximated by fuzzy modal formulas. △ Less

Submitted 5 February, 2018; v1 submitted 1 February, 2018; originally announced February 2018.

MSC Class: 03B45; 03B52; 03B70 ACM Class: F.4.1; I.2.4

Coalgebraic Behavioral Metrics

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, Barbara König

Abstract: We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $α\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$… ▽ More We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $α\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a functor $\overline{H}$ on the category $\mathrm{PMet}$ of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model linear-time metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction. △ Less

Submitted 15 July, 2024; v1 submitted 20 December, 2017; originally announced December 2017.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 3 (September 14, 2018) lmcs:4715

PAWS: A Tool for the Analysis of Weighted Systems

Authors: Barbara König, Sebastian Küpper, Christina Mika

Abstract: PAWS is a tool to analyse the behaviour of weighted automata and conditional transition systems. At its core PAWS is based on a generic implementation of algorithms for checking language equivalence in weighted automata and bisimulation in conditional transition systems. This architecture allows for the use of arbitrary user-defined semirings. New semirings can be generated during run-time and the… ▽ More PAWS is a tool to analyse the behaviour of weighted automata and conditional transition systems. At its core PAWS is based on a generic implementation of algorithms for checking language equivalence in weighted automata and bisimulation in conditional transition systems. This architecture allows for the use of arbitrary user-defined semirings. New semirings can be generated during run-time and the user can rely on numerous automatisation techniques to create new semiring structures for PAWS' algorithms. Basic semirings such as distributive complete lattices and fields of fractions can be defined by specifying few parameters, more exotic semirings can be generated from other semirings or defined from scratch using a built-in semiring generator. In the most general case, users can define new semirings by programming (in C#) the base operations of the semiring and a procedure to solve linear equations and use their newly generated semiring in the analysis tools that PAWS offers. △ Less

Submitted 13 July, 2017; originally announced July 2017.

Comments: In Proceedings QAPL 2017, arXiv:1707.03668

ACM Class: F.1.1; F.3.1; F.4.3

Journal ref: EPTCS 250, 2017, pp. 75-91

Conditional Transition Systems with Upgrades

Authors: Harsh Beohar, Barbara König, Sebastian Küpper, Alexandra Silva

Abstract: We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transiti… ▽ More We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transition systems (LaTS), where transitions are labelled with the elements from a distributive lattice. We define equivalent notions of bisimilarity for both variants and characterise them via a bisimulation game. We explain how conditional transition systems are related to featured transition systems for the modelling of software product lines. Furthermore, we show how to compute bisimilarity symbolically via BDDs by defining an operation on BDDs that approximates an element of a Boolean algebra into a lattice. We have implemented our procedure and provide runtime results. △ Less

Submitted 8 June, 2017; originally announced June 2017.

ACM Class: D.2.4; F.3.1

(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras

Authors: Barbara König, Christina Mika-Michalski

Abstract: Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics). Our fi… ▽ More Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics). Our first contribution is to introduce a spoiler-defender bisimulation game for coalgebras in the classical case. Second, we introduce such games for the metric case and furthermore define a real-valued modal coalgebraic logic, from which we can derive the strategy of the spoiler. For this logic we show a quantitative version of the Hennessy-Milner theorem. △ Less

Submitted 19 April, 2021; v1 submitted 29 May, 2017; originally announced May 2017.

Comments: CONCUR 2018

Specifying Graph Languages with Type Graphs

Authors: Andrea Corradini, Barbara König, Dennis Nolte

Abstract: We investigate three formalisms to specify graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basi… ▽ More We investigate three formalisms to specify graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basic approach to a type graph logic and, third, to type graphs with annotations. We present decidability results and closure properties for each of the formalisms. △ Less

Submitted 21 April, 2017; v1 submitted 18 April, 2017; originally announced April 2017.

Comments: (v2): -Fixed some typos -Added more references

Up-To Techniques for Weighted Systems (Extended Version)

Authors: Filippo Bonchi, Barbara König, Sebastian Küpper

Abstract: We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (o… ▽ More We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (over a semiring) is in the congruence closure of a given relation of vectors. This problem is considered for rings and l-monoids, for the latter we provide a rewriting algorithm and show its confluence and termination. We then explain how to apply these up-to techniques to weighted automata and provide runtime results. △ Less

Submitted 23 January, 2017; v1 submitted 18 January, 2017; originally announced January 2017.

ACM Class: F.1.1; F.3.1; D.2.4

A coalgebraic treatment of conditional transition systems with upgrades

Authors: Harsh Beohar, Barbara König, Sebastian Küpper, Alexandra Silva, Thorsten Wißmann

Abstract: We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branch… ▽ More We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branching type of the coalgebra and investigate the resulting behavioural equivalence. Furthermore we show how an existing algorithm for coalgebra minimisation can be instantiated to derive behavioural equivalences in this setting. △ Less

Submitted 15 December, 2018; v1 submitted 15 December, 2016; originally announced December 2016.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 1 (February 28, 2018) lmcs:2604

Towards Trace Metrics via Functor Lifting

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, Barbara König

Abstract: We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, showing under which conditions also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determiniza… ▽ More We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, showing under which conditions also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra on Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata. △ Less

Submitted 29 May, 2015; originally announced May 2015.

Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings

Authors: H. J. Sander Bruggink, Barbara König, Dennis Nolte, Hans Zantema

Abstract: We introduce techniques for proving uniform termination of graph transformation systems, based on matrix interpretations for string rewriting. We generalize this technique by adapting it to graph rewriting instead of string rewriting and by generalizing to ordered semirings. In this way we obtain a framework which is inspired by the tropical and arctic type graphs of [5] and introduces a new varia… ▽ More We introduce techniques for proving uniform termination of graph transformation systems, based on matrix interpretations for string rewriting. We generalize this technique by adapting it to graph rewriting instead of string rewriting and by generalizing to ordered semirings. In this way we obtain a framework which is inspired by the tropical and arctic type graphs of [5] and introduces a new variant of arithmetic type graphs. These type graphs can be used to assign weights to graphs and to show that these weights decrease in every rewriting step in order to prove termination. We present an example involving counters and discuss the implementation in the tool Grez. △ Less

Submitted 11 October, 2023; v1 submitted 7 May, 2015; originally announced May 2015.

Preliminary Report of the AMS analysis of tsunami deposits in Tohoku -- Japan -- 18th to the 21st Century

Authors: P. Wassmer, C. Gomez, D. E. Hart, T. Hiraishi, R. Azuma, B. Koenig, M. Trautmann

Abstract: Sedimentary records of tsunamis are a precious tool to assess the occurrence of past events, as attested by an abundant literature, which has seen a particular 'boom' in the aftermath of the 2004 Indian Ocean tsunami and the 2011 Tohoku tsunami. Despite an extensive literature, there is very little to no understanding of the role that the changing coastal environment is playing on the record of a… ▽ More Sedimentary records of tsunamis are a precious tool to assess the occurrence of past events, as attested by an abundant literature, which has seen a particular 'boom' in the aftermath of the 2004 Indian Ocean tsunami and the 2011 Tohoku tsunami. Despite an extensive literature, there is very little to no understanding of the role that the changing coastal environment is playing on the record of a tsunami, and for a given location, it is still unclear whether the largest tsunamis leave the largest amount of deposits. To research this question, the present study took place in Japan, in the Tohoku Region at Agawa-pond, because the pond act as a sediment trap. Using a sediment-slicer, a 1 m thick deposit was retrieved, from which 4 tsunami sequences were identified, including the latest 2011 tsunami. Using a series of sedimentary proxies: the AMS (Anisotropy of Magnetic Susceptibility), grain size analysis, quartz morphoscopy (morphology and surface characteristics) and the analysis of microfossils, disparities between the tsunami deposits were identified and most importantly a clear thinning of the tsunami deposit towards the top. Provided the present evidences, the authors discuss that the upward fining is due to at least two components that are seldom assessed in tsunami research (1) a modification of the depositional environment, with the progressive anthropization of the coast, providing less sediments to remobilize; and (2) a progressive filling of the Agawa pond, which progressively loses its ability to trap tsunami materials. △ Less

Submitted 24 February, 2015; originally announced February 2015.

Behavioral Metrics via Functor Lifting

Authors: Paolo Baldan, Filippo Bonchi, Henning Kerstan, Barbara König

Abstract: We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha: X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states. A first crucial step is the lifting of the functor F on Set to a functor in the category PMet of pseudometric spaces. We present two differe… ▽ More We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha: X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states. A first crucial step is the lifting of the functor F on Set to a functor in the category PMet of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. Then a final coalgebra for F in Set can be endowed with a behavioral distance resulting as the smallest solution of a fixed-point equation, yielding the final coalgebra in PMet. The same technique, applied to an arbitrary coalgebra alpha: X -> FX in Set, provides the behavioral distance on X. Under some constraints we can prove that two states are at distance 0 if and only if they are behaviorally equivalent. △ Less

Submitted 13 October, 2014; originally announced October 2014.

Comments: to be published in: Proceedings of FSTTCS 2014

A General Framework for Well-Structured Graph Transformation Systems

Authors: Barbara König, Jan Stückrath

Abstract: Graph transformation systems (GTSs) can be seen as wellstructured transition systems (WSTSs), thus obtaining decidability results for certain classes of GTSs. In earlier work it was shown that wellstructuredness can be obtained using the minor ordering as a well-quasiorder. In this paper we extend this idea to obtain a general framework in which several types of GTSs can be seen as (restricted) WS… ▽ More Graph transformation systems (GTSs) can be seen as wellstructured transition systems (WSTSs), thus obtaining decidability results for certain classes of GTSs. In earlier work it was shown that wellstructuredness can be obtained using the minor ordering as a well-quasiorder. In this paper we extend this idea to obtain a general framework in which several types of GTSs can be seen as (restricted) WSTSs. We instantiate this framework with the subgraph ordering and the induced subgraph ordering and apply it to analyse a simple access rights management system. △ Less

Submitted 18 June, 2014; originally announced June 2014.

Comments: Extended version (including proofs) of a paper accepted at CONCUR 2014

Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems

Authors: Henning Kerstan, Barbara König

Abstract: Coalgebras in a Kleisli category yield a generic definition of trace semantics for various types of labelled transition systems. In this paper we apply this generic theory to generative probabilistic transition systems, short PTS, with arbitrary (possibly uncountable) state spaces. We consider the sub-probability monad and the probability monad (Giry monad) on the category of measurable spaces and… ▽ More Coalgebras in a Kleisli category yield a generic definition of trace semantics for various types of labelled transition systems. In this paper we apply this generic theory to generative probabilistic transition systems, short PTS, with arbitrary (possibly uncountable) state spaces. We consider the sub-probability monad and the probability monad (Giry monad) on the category of measurable spaces and measurable functions. Our main contribution is that the existence of a final coalgebra in the Kleisli category of these monads is closely connected to the measure-theoretic extension theorem for sigma-finite pre-measures. In fact, we obtain a practical definition of the trace measure for both finite and infinite traces of PTS that subsumes a well-known result for discrete probabilistic transition systems. Finally we consider two example systems with uncountable state spaces and apply our theory to calculate their trace measures. △ Less

Submitted 3 December, 2013; v1 submitted 28 October, 2013; originally announced October 2013.

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 4 (December 4, 2013) lmcs:859

A stochastic model of social interaction in wild house mice

Authors: Nicolas Perony, Barbara König, Frank Schweitzer

Abstract: We investigate to what extent the interaction dynamics of a population of wild house mouse (Mus musculus domesticus) in their environment can be explained by a simple stochastic model. We use a Markov chain model to describe the transitions of mice in a discrete space of nestboxes, and implement a multi-agent simulation of the model. We find that some important features of our behavioural dataset… ▽ More We investigate to what extent the interaction dynamics of a population of wild house mouse (Mus musculus domesticus) in their environment can be explained by a simple stochastic model. We use a Markov chain model to describe the transitions of mice in a discrete space of nestboxes, and implement a multi-agent simulation of the model. We find that some important features of our behavioural dataset can be reproduced using this simplified stochastic representation, and discuss the improvements that could be made to our model in order to increase the accuracy of its predictions. Our findings have implications for the understanding of the complexity underlying social behaviour in the animal kingdom and the cognitive requirements of such behaviour. △ Less

Submitted 4 December, 2012; originally announced December 2012.

Comments: 12 pages, 5 figures, 2 tables. Originally published in the Proceedings of the European Conference on Complex Systems 2010 (ECCS'10), Lisbon, September 13-17, 2010

Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets

Authors: Paolo Baldan, Andrea Corradini, Hartmut Ehrig, Reiko Heckel, Barbara König

Abstract: We propose a framework for the specification of behaviour-preserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of ordinary Place/Transition nets suited to model open systems which might interact with the surrounding environment and endowed with a colimit-based composition operation. We show that natural notions of bisimilarity… ▽ More We propose a framework for the specification of behaviour-preserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of ordinary Place/Transition nets suited to model open systems which might interact with the surrounding environment and endowed with a colimit-based composition operation. We show that natural notions of bisimilarity over open nets are congruences with respect to the composition operation. The considered behavioural equivalences differ for the choice of the observations, which can be single firings or parallel steps. Additionally, we consider weak forms of such equivalences, arising in the presence of unobservable actions. We also provide an up-to technique for facilitating bisimilarity proofs. The theory is used to identify suitable classes of reconfiguration rules (in the double-pushout approach to rewriting) whose application preserves the observational semantics of the net. △ Less

Submitted 21 October, 2008; v1 submitted 24 September, 2008; originally announced September 2008.

Comments: To appear in "Logical Methods in Computer Science", 41 pages

ACM Class: F.4.1, D.2.2, D.3.1

Journal ref: Logical Methods in Computer Science, Volume 4, Issue 4 (October 21, 2008) lmcs:1165

Kurepa-trees and Namba-forcing

Authors: Bernhard Koenig, Yasuo Yoshinobu

Abstract: We show that compact cardinals and {\rm MM} are sensitive to $λ$-closed forcings for arbitrarily large $λ$. This is done by adding 'regressive' $λ$-Kurepa-trees in either case. We argue that the destruction of regressive Kurepa-trees with {\rm MM} requires the use of Namba forcing. We show that compact cardinals and {\rm MM} are sensitive to $λ$-closed forcings for arbitrarily large $λ$. This is done by adding 'regressive' $λ$-Kurepa-trees in either case. We argue that the destruction of regressive Kurepa-trees with {\rm MM} requires the use of Namba forcing. △ Less

Submitted 4 May, 2006; originally announced May 2006.

Forcing indestructibility of set-theoretic axioms

Authors: Bernhard Koenig

Abstract: Various theorems for the preservation of set-theoretic axioms under forcing are proved, regarding both forcing axioms and axioms true in the Levy-Collapse. These show in particular that certain applications of forcing axioms require to add generic countable sequences high up in the set-theoretic hierarchy even before collapsing everything down to $\aleph\_1$. Later we give applications, among th… ▽ More Various theorems for the preservation of set-theoretic axioms under forcing are proved, regarding both forcing axioms and axioms true in the Levy-Collapse. These show in particular that certain applications of forcing axioms require to add generic countable sequences high up in the set-theoretic hierarchy even before collapsing everything down to $\aleph\_1$. Later we give applications, among them the consistency of ${\rm MM}$ with $\aleph\_ω$ not being Jonsson which answers a question raised during Oberwolfach 2005. △ Less

Submitted 4 May, 2006; originally announced May 2006.