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
|