Jan Rutten

I&C Journal 2016 Journal Article

Proving language inclusion and equivalence by coinduction

• Jurriaan Rot
• Marcello Bonsangue
• Jan Rutten

Language equivalence and inclusion can be checked coinductively by establishing a (bi)simulation on suitable deterministic automata. In this paper we present an enhancement of this technique called (bi)simulation-up-to. We give general conditions on language operations for which bisimulation-up-to is sound. These results are illustrated by a large number of examples, giving new proofs of classical results such as Arden's rule, and involving the regular operations of union, concatenation and Kleene star as well as language equations with complement and intersection, and shuffle (closure).

Highlights Conference 2013 Conference Abstract

A final coalgebra for k-regular and k-automatic sequences

• Joost Winter
• Helle Hvid Hansen
• Clemens Kupke
• Jan Rutten

We offer a coalgebraic perspective on the k-regular sequences. For any k >= 1 and semiring S, the set of sequences with output in S is the carrier of a final coalgebra. This allows us to give a coalgebraic characterization of the k-regular sequences. Using an isomorphism based on a bijective numeration system, we thus obtain a structural correspondence between S-rational series over k nonterminals, and k-regular sequences with output in S. We will furthermore discuss a connection with sequences definable by divide and conquer recurrences.

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.

I&C Journal 2010 Journal Article

Complete sets of cooperations

• Clemens Kupke
• Jan Rutten

The structure map turning a set into the carrier of a final coalgebra is not unique. This fact is well known, but commonly elided. In this paper, we argue that any such concrete representation of a set as a final coalgebra is potentially interesting on its own. We discuss several examples, in particular, we consider different coalgebra structures that turn the set of infinite streams into the carrier of a final coalgebra. After that we focus on coalgebra structures that are made up using so-called cooperations. We say that a collection of cooperations is complete for a given set X if it gives rise to a coalgebra structure that turns X into the carrier set of a subcoalgebra of a final coalgebra. Any complete set of cooperations yields a coalgebraic proof and definition principle. We exploit this fact and devise a general definition scheme for constants and functions on a set X that is parametrical in the choice of the complete set of cooperations for X.

TCS Journal 2006 Journal Article

Preface

• José Fiadeiro
• Jan Rutten

TCS Journal 2002 Journal Article

Foreword

• Bart Jacobs
• Jan Rutten

TCS Journal 2001 Journal Article

Foreword

• Bart Jacobs
• Larry Moss
• Horst Reichel
• Jan Rutten

TCS Journal 1995 Journal Article

Preface

• Paul Gastin
• Jan Rutten

I&C Journal 1989 Journal Article

Denotational semantics of a parallel object-oriented language

• Pierre America
• Jaco de Bakker
• Joost N. Kok
• Jan Rutten

A denotational model is presented for the language POOL, a parallel object-oriented language. It is a syntactically simplified version of POOL-T, a language that is actually used to write programs for a parallel machine. The most important aspect of this language is that it describes a system as a collection of communicating objects that all have internal activities which are executed in parallel. To describe the semantics of this language we construct a mathematical domain of processes. This domain is obtained as a solution of a reflexive domain equation over a category of complete metric spaces. A new technique is developed to solve a wide class of such equations, including function space constructions. The desired domain is obtained as the fixed point of a contracting functor implicit in the equation. The domain is sufficiently rich to allow a fully compositional definition of the language constructs in POOL, including concepts such as object creation and method invocation by messages. The semantic equations give a meaning to each syntactic construct depending on the POOL object executing the construct, the environment constituted by the declarations, and a continuation, representing the actions to be performed after the execution of the current construct. After the process representing the execution of an entire program is constructed, a yield function can extract the set of possible execution sequences from it. A preliminary discussion is provided on how to deal with fairness. Full mathematical details are supplied, with the exception of the general domain construction, which is described elsewhere.