Alexandra Silva

TCS Journal 2025 Journal Article

Convex language semantics for nondeterministic probabilistic automata

• Gerco van Heerdt
• Justin Hsu
• Joël Ouaknine
• Alexandra Silva

We explore language semantics for automata combining probabilistic and nondeterministic behaviors. We first show that there are precisely two natural semantics for probabilistic automata with nondeterminism. For both choices, we show that these automata are strictly more expressive than deterministic probabilistic automata, and we prove that the problem of checking language equivalence is undecidable by reduction from the threshold problem. However, we provide a discounted metric that can be computed to arbitrarily high precision.

GandALF Workshop 2023 Workshop Paper

Conflict-Aware Active Automata Learning

• Tiago Ferreira
• Léo Henry
• Raquel Fernandes da Silva
• Alexandra Silva

Active automata learning algorithms cannot easily handle conflict in the observation data (different outputs observed for the same inputs). This inherent inability to recover after a conflict impairs their effective applicability in scenarios where noise is present or the system under learning is mutating. We propose the Conflict-Aware Active Automata Learning (C3AL) framework to enable handling conflicting information during the learning process. The core idea is to consider the so-called observation tree as a first-class citizen in the learning process. Though this idea is explored in recent work, we take it to its full effect by enabling its use with any existing learner and minimizing the number of tests performed on the system under learning, specially in the face of conflicts. We evaluate C3AL in a large set of benchmarks, covering over 30 different realistic targets, and over 18, 000 different scenarios. The results of the evaluation show that C3AL is a suitable alternative framework for closed-box learning that can better handle noise and mutations.

TCS Journal 2020 Journal Article

Left-handed completeness

• Dexter Kozen
• Alexandra Silva

We give a new proof of the completeness of the left-handed star rule of Kleene algebra. The proof is significantly shorter than previous proofs and exposes the rich interaction of algebra and coalgebra in the theory of Kleene algebra.

TCS Journal 2015 Journal Article

Killing epsilons with a dagger: A coalgebraic study of systems with algebraic label structure

• Filippo Bonchi
• Stefan Milius
• Alexandra Silva
• Fabio Zanasi

We propose an abstract framework for modelling state-based systems with internal behaviour as e. g. given by silent or ϵ-transitions. Our approach employs monads with a parametrized fixpoint operator † to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems and non-deterministic transducers.

I&C Journal 2012 Journal Article

A coalgebraic perspective on linear weighted automata

• Filippo Bonchi
• Marcello Bonsangue
• Michele Boreale
• Jan Rutten
• Alexandra Silva

Weighted automata are a generalisation of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e. g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence. Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours. In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on Set (the category of sets and functions) characterise weighted bisimilarity, while coalgebras on Vect (the category of vector spaces and linear maps) characterise weighted language equivalence. Relying on the second characterisation, we show three different procedures for computing weighted language equivalence. The first one consists in a generalisation of the usual partition refinement algorithm for ordinary automata. The second one is the backward version of the first one. The third procedure relies on a syntactic representation of rational weighted languages.

TCS Journal 2011 Journal Article

Preface

• Bart Jacobs
• Milad Niqui
• Jan Rutten
• Alexandra Silva

I&C Journal 2011 Journal Article

Quantitative Kleene coalgebras

• Alexandra Silva
• Filippo Bonchi
• Marcello Bonsangue
• Jan Rutten

We present a systematic way to generate (1) languages of (generalised) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of quantitative systems. Our quantitative systems include weighted versions of automata and transition systems, in which transitions are assigned a value in a monoid that represents cost, duration, probability, etc. Such systems are represented as coalgebras and (1) and (2) above are derived in a modular fashion from the underlying (functor) type of these coalgebras. In previous work, we applied a similar approach to a class of systems (without weights) that generalizes both the results of Kleene (on rational languages and DFA’s) and Milner (on regular behaviours and finite LTS’s), and includes many other systems such as Mealy and Moore machines. In the present paper, we extend this framework to deal with quantitative systems. As a consequence, our results now include languages and axiomatizations, both existing and new ones, for many different kinds of probabilistic systems.

I&C Journal 2010 Journal Article

A coinductive calculus of binary trees

• Alexandra Silva
• Jan Rutten

We study the set T A of infinite binary trees with nodes labelled in a semiring A from a coalgebraic perspective. We present coinductive definition and proof principles based on the fact that T A carries a final coalgebra structure. By viewing trees as formal power series, we develop a calculus where definitions are presented as behavioural differential equations. We present a general format for these equations that guarantees the existence and uniqueness of solutions. Although technically not very difficult, the resulting framework has surprisingly nice applications, which is illustrated by various concrete examples.