Selected Papers of the Conference "Algebraic and Coalgebraic Methods in Computer Science 2007"

2007 Editor: Till Mossakowski

This special issue collects extended versions of five papers presented at the second CALCO 2007 in Bergen, Norway. CALCO, the Conference "Algebraic and Coalgebraic Methods in Computer Science", has been founded by joining forces of WADT, the International Workshop on Algebraic Development Techniques, and CMCS, the International Workshop on Coalgebraic Methods in Computer Science. CALCO 2007 received 57 submissions (including four tool papers), out of which 26 (including two tool papers) were selected for presentation at the conference and for publication in Springer Lecture Notes in Computer Science 4624. The five papers of this special issue underwent a new and thorough reviewing process.

The present volume starts with a survey article by Jan Rutten, who is one of the co-founders of the field of coalgebra. *Rational streams coalgebraically* gives an equivalence proof for four representations of infinite streams at an elementary level, illustrating the benefit of coinduction, the central coalgebraic proof method.

The paper *Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets* by Paolo Baldan, Andrea Corradini, Hartmut Ehrig, Reiko Heckel and Barbara König studies open Petri nets, a reactive extension of standard Petri nets. Central to this work is the identification of several different notions of bisimilarity, proofs that these are congruences, and the development of methods for bisimilarity proofs. Although no explicit reference to the notion of coalgebra is made, the questions and methods of this paper are clearly coalgebraic.

Lutz Schröoder continues with an interplay of algebra and coalgebra: *Bootstrapping Inductive and Coinductive Types in HasCASL* addresses the construction of inductive data-types and coinductive process types over an arbitrary quasitopos with natural numbers object, and examines under which conditions these constructions are conservative.

While the natural logic of algebra is equational logic, the natural logic of coalgebra is modal logic. Consequently, the semantics of non-normal modal logics given by neighbourhood structures (generalising normal modal logics with Kripke semantics) is best studied in a coalgebraic setting. In their paper *Neighbourhood Structures: Bisimilarity and Basic Model Theory*, Helle Hvid Hansen, Clemens Kupke and Eric Pacuit complement the standard notion of bisimilarity and behavioural equivalence with a notion of precocongruence that better captures the intuition of behavioural equivalence. With this, the authors prove a Hennessy-Milner theorem and an analogue of Van Benthem's characterisation theorem.

Finally, in *Applications of Metric Coinduction*, Dexter Kozen and Nicholas Ruozzi again address coinduction, which is here specialised to metric coinduction, which is a kind of fixed-point theorem for eventually contractive maps on metric spaces. The authors illustrate the use of metric coinduction in such diverse areas as infinite streams, Markov chains, Markov decision processes, and non-well-founded sets.

We thank the authors for their contributions, and the reviewers for their valuable feedback. We also thank the members of the Program Committee of CALCO 2007 and their sub-referees who contributed to the selection and the refereeing process.

Till Mossakowski and Ugo Montanari
Guest Editors

1. Rational streams coalgebraically

J. J. M. M. Rutten.

We study rational streams (over a field) from a coalgebraic perspective. Exploiting the finality of the set of streams, we present an elementary and uniform proof of the equivalence of four notions of representability of rational streams: by finite dimensional linear systems; by finite stream circuits; by finite weighted stream automata; and by finite dimensional subsystems of the set of streams.

2. Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets

Paolo Baldan ; Andrea Corradini ; Hartmut Ehrig ; Reiko Heckel ; Barbara König.

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.

3. Bootstrapping Inductive and Coinductive Types in HasCASL

Lutz Schröder.

We discuss the treatment of initial datatypes and final process types in the wide-spectrum language HasCASL. In particular, we present specifications that illustrate how datatypes and process types arise as bootstrapped concepts using HasCASL's type class mechanism, and we describe constructions of types of finite and infinite trees that establish the conservativity of datatype and process type declarations adhering to certain reasonable formats. The latter amounts to modifying known constructions from HOL to avoid unique choice; in categorical terminology, this means that we establish that quasitoposes with an internal natural numbers object support initial algebras and final coalgebras for a range of polynomial functors, thereby partially generalising corresponding results from topos theory. Moreover, we present similar constructions in categories of internal complete partial orders in quasitoposes.

4. Neighbourhood Structures: Bisimilarity and Basic Model Theory

Helle Hvid Hansen ; Clemens Kupke ; Eric Pacuit.

Neighbourhood structures are the standard semantic tool used to reason about non-normal modal logics. The logic of all neighbourhood models is called classical modal logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, denoted by 2^2. We use this coalgebraic modelling to derive notions of equivalence between neighbourhood structures. 2^2-bisimilarity and behavioural equivalence are well known coalgebraic concepts, and they are distinct, since 2^2 does not preserve weak pullbacks. We introduce a third, intermediate notion whose witnessing relations we call precocongruences (based on pushouts). We give back-and-forth style characterisations for 2^2-bisimulations and precocongruences, we show that on a single coalgebra, precocongruences capture behavioural equivalence, and that between neighbourhood structures, precocongruences are a better approximation of behavioural equivalence than 2^2-bisimulations. We also introduce a notion of modal saturation for neighbourhood models, and investigate its relationship with definability and image-finiteness. We prove a Hennessy-Milner theorem for modally saturated and for image-finite neighbourhood models. Our main results are an analogue of Van Benthem's characterisation theorem and a model-theoretic proof of Craig interpolation for classical modal logic.

5. Applications of Metric Coinduction

Dexter Kozen ; Nicholas Ruozzi.

Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some property is preserved by one step of the approximation process, then automatically infer by the coinduction principle that the property holds of the limit object. This can often be used to avoid complicated analytic arguments involving limits and convergence, replacing them with simpler algebraic arguments. This paper examines the application of this principle in a variety of areas, including infinite streams, Markov chains, Markov decision processes, and non-well-founded sets. These results point to the usefulness of coinduction as a general proof technique.