
We study different behavioral metrics, such as those arising from both
branching and lineartime semantics, in a coalgebraic setting. Given a
coalgebra $\alpha\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to
\mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which
measure the behavioral distance of states.
A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a
functor $\overline{H}$ on the category $\mathrm{PMet}$ of pseudometric spaces.
We present two different approaches which can be viewed as generalizations of
the Kantorovich and Wasserstein pseudometrics for probability measures. We show
that the pseudometrics provided by the two approaches coincide on several
natural examples, but in general they differ.
If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a
canonical way a behavioral distance which is usually branchingtime, i.e., it
generalizes bisimilarity. In order to model lineartime metrics (generalizing
trace equivalences), we show sufficient conditions for lifting distributive
laws and monads. These results enable us to employ the generalized powerset
construction.

Event structures are a widely accepted model of concurrency. In a seminal
paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge
between the theory of domains and the approach to concurrency proposed by
Petri. A basic role is played by an unfolding construction that maps (safe)
Petri nets into a subclass of event structures where each event has a uniquely
determined set of causes, called prime event structures, which in turn can be
identified with their domain of configurations. At a categorical level, this is
nicely formalised by Winskel as a chain of coreflections. Contrary to prime
event structures, general event structures allow for the presence of
disjunctive causes, i.e., events can be enabled by distinct minimal sets of
events. In this paper, we extend the connection between Petri nets and event
structures in order to include disjunctive causes. In particular, we show that,
at the level of nets, disjunctive causes are well accounted for by persistent
places. These are places where tokens, once generated, can be used several
times without being consumed and where multiple tokens are interpreted
collectively, i.e., their histories are inessential. Generalising the work on
ordinary nets, Petri nets with persistence are related to a new class of event
structures, called locally connected, by means of a chain of coreflection
relying on an unfolding construction.

Stable event structures, and their duality with prime algebraic domains
(arising as partial orders of configurations), are a landmark of concurrency
theory, providing a clear characterisation of causality in computations. They
have been used for defining a concurrent semantics of several formalisms, from
Petri nets to linear graph rewriting systems, which in turn lay at the basis of
many visual frameworks. Stability however is restrictive for dealing with
formalisms where a computational step can merge parts of the state, like graph
rewriting systems with nonlinear rules, which are needed to cover some
relevant applications (such as the graphical encoding of calculi with name
passing). We characterise, as a natural generalisation of prime algebraic
domains, a class of domains that is wellsuited to model the semantics of
formalisms with fusions. We then identify a corresponding class of event
structures, that we call connected event structures, via a duality result
formalised as an equivalence of categories. Connected event structures are
exactly the class of event structures the arise as the semantics of nonlinear
graph rewriting systems. Interestingly, the category of general unstable event
structures coreflects into our category of domains, so that our result provides
a characterisation of the partial orders of configurations of such event
structures.

We investigate the possibility of deriving metric trace semantics in a
coalgebraic framework. First, we generalize a technique for systematically
lifting functors from the category Set of sets to the category PMet of
pseudometric spaces, showing under which conditions also natural
transformations, monads and distributive laws can be lifted. By exploiting some
recent work on an abstract determinization, these results enable the derivation
of trace metrics starting from coalgebras in Set. More precisely, for a
coalgebra on Set we determinize it, thus obtaining a coalgebra in the
EilenbergMoore category of a monad. When the monad can be lifted to PMet, we
can equip the final coalgebra with a behavioral distance. The trace distance
between two states of the original coalgebra is the distance between their
images in the determinized coalgebra through the unit of the monad. We show how
our framework applies to nondeterministic automata and probabilistic automata.

We study behavioral metrics in an abstract coalgebraic setting. Given a
coalgebra alpha: X > FX in Set, where the functor F specifies the branching
type, we define a framework for deriving pseudometrics on X which measure the
behavioral distance of states.
A first crucial step is the lifting of the functor F on Set to a functor in
the category PMet of pseudometric spaces. We present two different approaches
which can be viewed as generalizations of the Kantorovich and Wasserstein
pseudometrics for probability measures. We show that the pseudometrics provided
by the two approaches coincide on several natural examples, but in general they
differ.
Then a final coalgebra for F in Set can be endowed with a behavioral distance
resulting as the smallest solution of a fixedpoint equation, yielding the
final coalgebra in PMet. The same technique, applied to an arbitrary coalgebra
alpha: X > FX in Set, provides the behavioral distance on X. Under some
constraints we can prove that two states are at distance 0 if and only if they
are behaviorally equivalent.

Event structures represent concurrent processes in terms of events and
dependencies between events modelling behavioural relations like causality and
conflict. Since the introduction of prime event structures, many variants of
event structures have been proposed with different behavioural relations and,
hence, with differences in their expressive power. One of the possible benefits
of using a more expressive event structure is that of having a more compact
representation for the same behaviour when considering the number of events
used in a prime event structure. Therefore, this article addresses the problem
of reducing the size of an event structure while preserving behaviour under a
wellknown notion of equivalence, namely history preserving bisimulation. In
particular, we investigate this problem on two generalisations of the prime
event structures. The first one, known as asymmetric event structure, relies on
a asymmetric form of the conflict relation. The second one, known as flow event
structure, supports a form of disjunctive causality. More specifically, we
describe the conditions under which a set of events in an event structure can
be folded into a single event while preserving the original behaviour. The
successive application of this folding operation leads to a minimal size event
structure. However, the order on which the folding operation is applied may
lead to different minimal size event structures. The latter has a negative
implication on the potential use of a minimal size event structure as a
canonical representation for behaviour.

We propose a logic for true concurrency whose formulae predicate about events
in computations and their causal dependencies. The induced logical equivalence
is hereditary history preserving bisimilarity, and fragments of the logic can
be identified which correspond to other true concurrent behavioural
equivalences in the literature: step, pomset and history preserving
bisimilarity. Standard HennessyMilner logic, and thus (interleaving)
bisimilarity, is also recovered as a fragment. We also propose an extension of
the logic with fixpoint operators, thus allowing to describe causal and
concurrency properties of infinite computations. We believe that this work
contributes to a rational presentation of the true concurrent spectrum and to a
deeper understanding of the relations between the involved behavioural
equivalences.

We propose a framework for the specification of behaviourpreserving
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 colimitbased 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 upto technique for
facilitating bisimilarity proofs. The theory is used to identify suitable
classes of reconfiguration rules (in the doublepushout approach to rewriting)
whose application preserves the observational semantics of the net.