
We consider conditional transition systems, that model software product lines
with upgrades, in a coalgebraic setting. By using Birkhoff's duality for
distributive lattices, we derive two equivalent Kleisli categories in which
these coalgebras live: Kleisli categories based on the reader and on the
socalled lattice monad over $\mathsf{Poset}$. We study two different functors
describing the branching type of the coalgebra and investigate the resulting
behavioural equivalence. Furthermore we show how an existing algorithm for
coalgebra minimisation can be instantiated to derive behavioural equivalences
in this setting.

We present an Angluinstyle algorithm to learn nominal automata, which are
acceptors of languages over infinite (structured) alphabets. The abstract
approach we take allows us to seamlessly extend known variations of the
algorithm to this new setting. In particular we can learn a subclass of nominal
nondeterministic automata. An implementation using a recently developed
Haskell library for nominal computation is provided for preliminary
experiments.

ProbNetKAT is a probabilistic extension of NetKAT with a denotational
semantics based on Markov kernels. The language is expressive enough to
generate continuous distributions, which raises the question of how to compute
effectively in the language. This paper gives an new characterization of
ProbNetKAT's semantics using domain theory, which provides the foundation
needed to build a practical implementation. We show how to use the semantics to
approximate the behavior of arbitrary ProbNetKAT programs using distributions
with finite support. We develop a prototype implementation and show how to use
it to solve a variety of problems including characterizing the expected
congestion induced by different routing schemes and reasoning probabilistically
about reachability in a network.

Using recent developments on coalgebraic and monadbased semantics, we
present a uniform study of various notions of machines, e.g.~finite state
machines, multistack machines, Turing machines, valence automata, and weighted
automata. They are instances of Jacobs' notion of a $\mathbf T$automaton,
where $\mathbf T$ is a monad. We show that the generic language semantics for
$\mathbf T$automata correctly instantiates the usual language semantics for a
number of known classes of machines/languages, including~regular, contextfree,
recursivelyenumerable and various subclasses of context free languages (e.g.
deterministic and realtime ones). Moreover, our approach provides new generic
techniques for studying the expressivity power of various machinebased models.

Automata learning has been successfully applied in the verification of
hardware and software. The size of the automaton model learned is a bottleneck
for scalability, and hence optimizations that enable learning of compact
representations are important. This paper exploits monads, both as a
mathematical structure and a programming construct, to design, prove correct,
and implement a wide class of such optimizations. The former perspective on
monads allows us to develop a new algorithm and accompanying correctness
proofs, building upon a general framework for automata learning based on
category theory. The new algorithm is parametric on a monad, which provides a
rich algebraic structure to capture nondeterminism and other sideeffects. We
show that our approach allows us to uniformly capture existing algorithms,
develop new ones, and add optimizations. The latter perspective allows us to
effortlessly translate the theory into practice: we provide a Haskell library
implementing our general framework, and we show experimental results for two
specific instances: nondeterministic and weighted automata.

We develop a method to incrementally construct programming languages. Our
approach is categorical: each layer of the language is described as a monad.
Our method either (i) concretely builds a distributive law between two monads,
i.e. layers of the language, which then provides a monad structure to the
composition of layers, or (ii) identifies precisely the algebraic obstacles to
the existence of a distributive law and gives a best approximant language. The
running example will involve three layers: a basic imperative language enriched
first by adding nondeterminism and then probabilistic choice. The first
extension works seamlessly, but the second encounters an obstacle, which
results in a best approximant language structurally very similar to the
probabilistic network specification language ProbNetKAT.

We tackle the problem of deciding whether two probabilistic programs are
equivalent in Probabilistic NetKAT, a formal language for specifying and
reasoning about the behavior of packetswitched networks. We show that the
problem is decidable for the historyfree fragment of the language by
developing an effective decision procedure based on stochastic matrices. The
main challenge lies in reasoning about iteration, which we address by designing
an encoding of the program semantics as a finitestate absorbing Markov chain,
whose limiting distribution can be computed exactly. In an extended case study
on a realworld data center network, we automatically verify various
quantitative properties of interest, including resilience in the presence of
failures, by analyzing the Markov chain semantics.

This paper introduces a categorical framework to study the exact and
approximate semantics of probabilistic programs. We construct a dagger
symmetric monoidal category of Borel kernels where the daggerstructure is
given by Bayesian inversion. We show functorial bridges between this category
and categories of Banach lattices which formalize the move from kernelbased
semantics to predicate transformer (backward) or state transformer (forward)
semantics. These bridges are related by natural transformations, and we show in
particular that the RadonNikodym and Riesz representation theorems  two
pillars of probability theory  define natural transformations.
With the mathematical infrastructure in place, we present a generic and
endogenous approach to approximating kernels on standard Borel spaces which
exploits the involutive structure of our category of kernels. The approximation
can be formulated in several equivalent ways by using the functorial bridges
and natural transformations described above. Finally, we show that for sensible
discretization schemes, every Borel kernel can be approximated by kernels on
finite spaces, and that these approximations converge for a natural choice of
topology.
We illustrate the theory by showing two examples of how approximation can
effectively be used in practice: Bayesian inference and the Kleene star
operation of ProbNetKAT.

Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and
Wehrman in 2009 as a framework to reason about concurrent programs. We prove
that the axioms for CKA with bounded parallelism are complete for the semantics
proposed in the original paper; consequently, these semantics are the free
model for this fragment. This result settles a conjecture of Hoare and
collaborators. Moreover, the techniques developed along the way are reusable;
in particular, they allow us to establish pomset automata as an operational
model for CKA.

We define Almost Sure Productivity (ASP), a probabilistic generalization of
the productivity condition for coinductively defined structures. Intuitively, a
probabilistic coinductive stream or tree is ASP if it produces infinitely many
outputs with probability 1. Formally, we define almost sure productivity using
a final coalgebra semantics of programs inspired from Kerstan and K\"onig.
Then, we introduce a core language for probabilistic streams and trees, and
provide two approaches to verify ASP: a sufficient syntactic criterion, and a
reduction to modelchecking pCTL* formulas on probabilistic pushdown automata.
The reduction shows that ASP is decidable for our core language.

We present a coinductive framework for defining and reasoning about the
infinitary analogues of equational logic and term rewriting in a uniform,
coinductive way. The setup captures rewrite sequences of arbitrary ordinal
length, but it has neither the need for ordinals nor for metric convergence.
This makes the framework especially suitable for formalizations in theorem
provers.

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs
that exhibit concurrent behaviour. As with previous extensions of Kleene
Algebra, characterizing the free model is crucial in order to develop the
foundations of the theory and potential applications. For CKA, this has been an
open question for a few years and this paper makes an important step towards an
answer. We present a new automaton model and a Kleenelike theorem that relates
a relaxed version of CKA to seriesparallel pomset languages, which are a
natural candidate for the free model. There are two substantial differences
with previous work: from expressions to automata, we use Brzozowski
derivatives, which enable a direct construction of the automaton; from automata
to expressions, we provide a syntactic characterization of the automata that
denote valid CKA behaviours.

Probabilistic automata (PA) combine probability and nondeterminism. They can
be given different semantics, like strong bisimilarity, convex bisimilarity, or
(more recently) distribution bisimilarity. The latter is based on the view of
PA as transformers of probability distributions, also called belief states, and
promotes distributions to firstclass citizens.
We give a coalgebraic account of the latter semantics, and explain the
genesis of the beliefstate transformer from a PA. To do so, we make explicit
the convex algebraic structure present in PA and identify beliefstate
transformers as transition systems with state space that carries a convex
algebra. As a consequence of our abstract approach, we can give a sound proof
technique which we call bisimulation upto convex hull.

Automata learning is a technique that has successfully been applied in
verification, with the automaton type varying depending on the application
domain. Adaptations of automata learning algorithms for increasingly complex
types of automata have to be developed from scratch because there was no
abstract theory offering guidelines. This makes it hard to devise such
algorithms, and it obscures their correctness proofs. We introduce a simple
categorytheoretic formalism that provides an appropriately abstract foundation
for studying automata learning. Furthermore, our framework establishes formal
relations between algorithms for learning, testing, and minimization. We
illustrate its generality with two examples: deterministic and weighted
automata.

We introduce a variant of transition systems, where activation of transitions
depends on conditions of the environment and upgrades during runtime
potentially create additional transitions. Using a cornerstone result in
lattice theory, we show that such transition systems can be modelled in two
ways: as conditional transition systems (CTS) with a partial order on
conditions, or as lattice transition systems (LaTS), where transitions are
labelled with the elements from a distributive lattice. We define equivalent
notions of bisimilarity for both variants and characterise them via a
bisimulation game.
We explain how conditional transition systems are related to featured
transition systems for the modelling of software product lines. Furthermore, we
show how to compute bisimilarity symbolically via BDDs by defining an operation
on BDDs that approximates an element of a Boolean algebra into a lattice. We
have implemented our procedure and provide runtime results.

Coalgebras provide a uniform framework to study dynamical systems, including
several types of automata. In this paper, we make use of the coalgebraic view
on systems to investigate, in a uniform way, under which conditions calculi
that are sound and complete with respect to behavioral equivalence can be
extended to a coarser coalgebraic language equivalence, which arises from a
generalised powerset construction that determinises coalgebras. We show that
soundness and completeness are established by proving that expressions modulo
axioms of a calculus form the rational fixpoint of the given type functor. Our
main result is that the rational fixpoint of the functor $FT$, where $T$ is a
monad describing the branching of the systems (e.g. nondeterminism, weights,
probability etc.), has as a quotient the rational fixpoint of the
"determinised" type functor $\bar F$, a lifting of $F$ to the category of
$T$algebras. We apply our framework to the concrete example of weighted
automata, for which we present a new sound and complete calculus for weighted
language equivalence. As a special case, we obtain nondeterministic automata,
where we recover Rabinovich's sound and complete calculus for language
equivalence.

We present a coinductive framework for defining infinitary analogues of
equational reasoning and rewriting in a uniform way. We define the relation
=^infty, notion of infinitary equational reasoning, and >^infty, the standard
notion of infinitary rewriting as follows:
=^infty := nu R. ( <_root + >_root + lift(R) )^*
>^infty := mu R. nu S. ( >_root + lift(R) )^* ; lift(S)
where
lift(R) := { (f(s_1,...,s_n), f(t_1,...,t_n))  s_1 R t_1,...,s_n R t_n } +
id ,
and where mu is the least fixed point operator and nu is the greatest fixed
point operator.
The setup captures rewrite sequences of arbitrary ordinal length, but it has
neither the need for ordinals nor for metric convergence. This makes the
framework especially suitable for formalizations in theorem provers.

We introduce a coinductive definition of infinitary term rewriting. The setup
is surprisingly simple, and has in contrast to the usual definitions of
infinitary rewriting, neither need for ordinals nor for metric convergence.
While the idea of a coinductive treatment of infinitary rewriting is not new,
all previous approaches were limited to reductions of length at most omega. The
approach presented in this paper is the first to capture the full infinitary
term rewriting with reductions of arbitrary ordinal length. Apart from an
elegant reformulation of known concepts, our approach gives rise, in a very
natural way, to a novel notion of infinitary equational reasoning.

We propose an abstract framework for modeling statebased systems with
internal behavior as e.g. given by silent or $\epsilon$transitions. Our
approach employs monads with a parametrized fixpoint operator $\dagger$ 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
statebased 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.

A notion of generalized regular expressions for a large class of systems
modeled as coalgebras, and an analogue of Kleene's theorem and Kleene algebra,
were recently proposed by a subset of the authors of this paper. Examples of
the systems covered include infinite streams, deterministic automata, Mealy
machines and labelled transition systems. In this paper, we present a novel
algorithm to decide whether two expressions are bisimilar or not. The procedure
is implemented in the automatic theorem prover CIRC, by reducing coinduction to
an entailment relation between an algebraic specification and an appropriate
set of equations. We illustrate the generality of the tool with three examples:
infinite streams of real numbers, Mealy machines and labelled transition
systems.

This volume contains the proceedings of ICE'12, the 5th Interaction and
Concurrency Experience workshop, which was held in Stockholm, Sweden on the
16th of June 2012 as a satellite event of DisCoTec'12. The topic of ICE'12 was
Distributed Coordination, Execution Models, and Resilient Interaction. The ICE
procedure for paper selection allows for PC members to interact, anonymously,
with authors. During the review phase, each submitted paper is published on a
Wiki and associated with a discussion forum whose access is restricted to the
authors and to all the PC members not declaring a conflict of interests. The PC
members post comments and questions that the authors reply to. Each paper was
reviewed by four PC members, and altogether 8 papers were accepted for
publication. We were proud to host two invited talks, Marcello Bonsangue and
Ichiro Hasuo, whose abstracts are included in this volume together with the
regular papers.

This volume contains the preproceedings of ICE'11, the 4th Interaction and
Concurrency Experience workshop, which was held in Reykjavik, Iceland on the
9th of June 2011 as a satellite event of DisCoTec'11.
The topic of ICE'11 was Reliable and Contractbased Interaction. Reliable
interactions are, e.g., those enjoying suitable logical, behavioural, or
security properties, or adhering to certain QoS standards. Contractbased
interactions are, e.g., those where the interacting entities are committed to
give certain guarantees whenever certain assumptions are met by their operating
environment.
The ICE procedure for paper selection allows for PC members to interact,
anonymously, with authors. During the review phase, each submitted paper is
published on a Wiki and associated with a discussion forum whose access is
restricted to the authors and to all the PC members not declaring a conflict of
interests. The PC members post comments and questions that the authors reply
to. Each paper was reviewed by four PC members, and altogether 8 papers (out of
12) were accepted for publication.
We were proud to host three invited talks by Rocco De Nicola (joint with
PACO), Simon Gay and Prakash Panangaden, whose abstracts are included in this
volume together with the regular papers.

This volume contains the proceedings of the 3rd Interaction and Concurrency
Experience (ICE 2010) workshop, which was held in Amsterdam, Netherlands on
10th of June 2010 as a satellite event of DisCoTec'10. Each year, the workshop
focuses on a specific topic: the topic of ICE 2010 was Guaranteed Interactions,
by which we mean, for example, guaranteeing safety, reactivity, quality of
service or satisfaction of analysis hypotheses.

In this paper, we present a systematic way of deriving (1) languages of
(generalised) regular expressions, and (2) sound and complete axiomatizations
thereof, for a wide variety of systems. This generalizes both the results of
Kleene (on regular languages and deterministic finite automata) and Milner (on
regular behaviours and finite labelled transition systems), and includes many
other systems such as Mealy and Moore machines.

In this paper we present a compositional semantics for the channelbased
coordination language Reo which enables the analysis of quality of service
(QoS) properties of service compositions. For this purpose, we annotate Reo
channels with stochastic delay rates and explicitly model dataarrival rates at
the boundary of a connector, to capture its interaction with the services that
comprise its environment. We propose Stochastic Reo automata as an extension of
Reo automata, in order to compositionally derive a QoSaware semantics for Reo.
We further present a translation of Stochastic Reo automata to ContinuousTime
Markov Chains (CTMCs). This translation enables us to use thirdparty CTMC
verification tools to do an endtoend performance analysis of service
compositions.