Barbara König

TACAS Conference 2026 Conference Paper

Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games

• Paolo Baldan
• Sebastian Gurke
• Barbara König
• Florian Wittbold

I&C Journal 2024 Journal Article

Systems of fixpoint equations: Abstraction, games, up-to techniques and local algorithms

• Paolo Baldan
• Barbara König
• Tommaso Padoan

Systems of fixpoint equations over complete lattices, which combine least and greatest fixpoints, often arise from verification tasks such as model checking and behavioural equivalence checking. In this paper we develop a theory of approximation in the style of abstract interpretation, where a system over some concrete domain is abstracted into a system on a suitable abstract domain, ensuring sound and possibly complete over-approximations of the solutions. We also show how up-to techniques, commonly used to simplify coinductive proofs, fit into this framework, interpreted as abstractions. Additionally, we characterise the solution of fixpoint equation systems through parity games, extending prior work limited to continuous lattices. This game-based approach allows for local algorithms that verify system properties, such as determining whether a state satisfies a formula or two states are behaviourally equivalent. We describe a local algorithm, that can be combined with abstraction and up-to techniques to speed up the computation.

Highlights Conference 2024 Conference Abstract

Up-To Techniques for Language Equivalence and Behavioural Metrics

• Barbara König

Up-To Techniques are coinductive proof techniques that provide small witnesses for lower bounds for greatest fixpoints (respectively upper bounds for least fixpoints). They have been introduced for bisimilarity checks, but can also be fruitfully be used for language equivalence or behavioural metrics, typically by exploiting an algebraic structure on the state space. This talk will start by introducing the lattice-theoretic foundations of up-to techniques and review results by Bonchi and Pous on checking language equivalence for NFAs. We will then generalize these results to a coalgebraic setting and to behavioural metrics, where the use of up-to techniques sometimes allows to resort to finite witnesses (rather than infinite ones). This is joint work with Filippo Bonchi, Daniela Petrisan, Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Matina Najafi, Wojciech Rozowski and Paul Wild.

IJCAI Conference 2019 Conference Paper

A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic

• Paul Wild
• Lutz Schröder
• Dirk Pattinson
• Barbara König

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.

I&C Journal 2017 Journal Article

Well-structured graph transformation systems

• Barbara König
• Jan Stückrath

Graph transformation systems (GTSs) can be seen as well-structured transition systems (WSTSs) and via well-structuredness it is possible to obtain decidability results for certain classes of GTSs. We present a generic framework, parameterized over the well-quasi-order (wqo), in which several types of GTSs can be seen as (restricted) WSTSs. We instantiate this framework with three orders: the minor ordering, the subgraph ordering and the induced subgraph ordering. Furthermore we consider two case studies where we apply the theory to analyze a leader election protocol and a simple access rights management system with our tool Uncover.

TCS Journal 2012 Journal Article

Efficient unfolding of contextual Petri nets

• Paolo Baldan
• Alessandro Bruni
• Andrea Corradini
• Barbara König
• César Rodríguez
• Stefan Schwoon

A contextual net is a Petri net extended with read arcs, which allows transitions to check for tokens without consuming them. Contextual nets allow for better modelling of concurrent read access than Petri nets, and their unfoldings can be exponentially more compact than those of a corresponding Petri net. A constructive but abstract procedure for generating those unfoldings was proposed in previous work. However, it remained unclear whether the approach was useful in practice and which data structures and algorithms would be appropriate to implement it. Here, we address this question. We provide two concrete methods for computing contextual unfoldings, with a view to efficiency. We report on experiments carried out on a number of benchmarks. These show that not only are contextual unfoldings more compact than Petri net unfoldings, but they can be computed with the same or better efficiency, in particular with respect to alternative approaches based on encodings of contextual nets into Petri nets.

I&C Journal 2010 Journal Article

Unfolding-based diagnosis of systems with an evolving topology

• Paolo Baldan
• Thomas Chatain
• Stefan Haar
• Barbara König

We propose a framework for model-based diagnosis of systems with mobility and variable topologies, modelled as graph transformation systems. Generally speaking, model-based diagnosis is aimed at constructing explanations of observed faulty behaviours on the basis of a given model of the system. Since the number of possible explanations may be huge, we exploit the unfolding as a compact data structure to store them, along the lines of previous work dealing with Petri net models. Given a model of a system and an observation, the explanations can be constructed by unfolding the model constrained by the observation, and then removing incomplete explanations in a pruning phase. The theory is formalised in a general categorical setting: constraining the system by the observation corresponds to taking a product in the chosen category of graph grammars, so that the correctness of the procedure can be proved by using the fact that the unfolding is a right adjoint and thus it preserves products. The theory should hence be easily applicable to a wide class of system models, including graph grammars and Petri nets.

I&C Journal 2009 Journal Article

Synthesising CCS bisimulation using graph rewriting

• Filippo Bonchi
• Fabio Gadducci
• Barbara König

The paper presents a case study on the synthesis of labelled transition systems (ltss) for process calculi, choosing as testbed Milner’s Calculus of Communicating System (ccs). The proposal is based on a graphical encoding: each ccs process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence. Graphs with interfaces are amenable to the synthesis mechanism proposed by Ehrig and König and based on borrowed contexts (bcs), an instance of relative pushouts originally introduced by Milner and Leifer. The bc mechanism allows the effective construction of an lts that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. Our paper focuses on the analysis of the lts distilled by exploiting the encoding of ccs processes: besides offering major technical contributions towards the simplification of the bc mechanism, a key result of our work is the proof that the bisimilarity on processes obtained via bcs coincides with the standard strong bisimilarity for ccs.

I&C Journal 2008 Journal Article

A framework for the verification of infinite-state graph transformation systems

• Paolo Baldan
• Andrea Corradini
• Barbara König

We propose a technique for the analysis of infinite-state graph transformation systems, based on the construction of finite structures approximating their behaviour. Following a classical approach, one can construct a chain of finite under-approximations (k-truncations) of the Winskel style unfolding of a graph grammar. More interestingly, also a chain of finite over-approximations (k-coverings) of the unfolding can be constructed. The fact that k-truncations and k-coverings approximate the unfolding with arbitrary accuracy is formalised by showing that both chains converge (in a categorical sense) to the full unfolding. We discuss how the finite over- and under-approximations can be used to check properties of systems modelled by graph transformation systems, illustrating this with some small examples. We also describe the Augur tool, which provides a partial implementation of the proposed constructions, and has been used for the verification of larger case studies.

TCS Journal 2004 Journal Article

On deterministic finite automata and syntactic monoid size

• Markus Holzer
• Barbara König

We investigate the relationship between regular languages and syntactic monoid size. In particular, we consider the transformation monoids of n-state (minimal) deterministic finite automata. We show tight upper and lower bounds on the syntactic monoid size depending on the number of generators (input alphabet size) used. It turns out, that the two generator case is the most involved one. There we show a lower bound of n n 1 - 2 n for the size of the syntactic monoid of a language accepted by an n-state deterministic finite automaton with binary input alphabet. Moreover, we prove that for every prime n ⩾ 7, the maximal size semigroup w. r. t. its size among all (transformation) semigroups which can be generated with two generators, is generated by a permutation with two cycles (of appropriate lengths) and a non-bijective mapping merging elements from these two cycles. As a by-product of our investigations we determine the maximal size among all semigroups generated by two transformations, where one is a permutation with a single cycle and the other is a non-bijective mapping.