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

Guest Editors

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 […]

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 […]

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 […]

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, […]

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 […]