arXiv subjects

Barbara König

Publications and source records attributed to Barbara König.

At least 37 records · Page 2Linked to original sources

arXiv2022

A Lattice-Theoretical View of Strategy Iteration

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.

cs.LO↗

arXiv2022

Probabilistic Systems with Hidden State and Unobservable Transitions

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.

cs.LG↗

arXiv2022

Conditional Bisimilarity for Reactive Systems

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.

cs.LO↗

arXiv2021

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

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.

cs.LO↗

arXiv2021

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

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.

cs.LO↗

arXiv2021

Fixpoint Games on Continuous Lattices

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.

cs.LO↗

arXiv2020

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

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.

cs.LO↗

arXiv2020

Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks

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.

cs.AI↗

arXiv2019

A van Benthem Theorem for Quantitative Probabilistic Modal Logic

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.

cs.LO↗

arXiv2019

A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

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.

cs.LO↗

arXiv2019

Rewriting Abstract Structures: Materialization Explained Categorically

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.

cs.LO↗

arXiv2018

A coalgebraic treatment of conditional transition systems with upgrades

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.

cs.LO↗

arXiv2018

Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks

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.

cs.LO↗

arXiv2018

Up-To Techniques for Behavioural Metrics via Fibrations

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.

cs.LO↗

arXiv2018

A van Benthem Theorem for Fuzzy Modal Logic

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.

cs.LO↗

arXiv2017

PAWS: A Tool for the Analysis of Weighted Systems

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.

cs.FL↗

arXiv2017

Conditional Transition Systems with Upgrades

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.

cs.SE↗

arXiv2017

Specifying Graph Languages with Type Graphs

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.

cs.FL↗