• Coalgebraic Behavioral Metrics(1712.07511)

May 11, 2018 cs.LO
We study different behavioral metrics, such as those arising from both branching and linear-time 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 branching-time, i.e., it generalizes bisimilarity. In order to model linear-time 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 for Petri nets with Persistence(1802.03726)

Feb. 11, 2018 cs.LO
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.
• Domains and Event Structures for Fusions(1701.02394)

Jan. 26, 2018 cs.LO
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 non-linear 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 well-suited 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 non-linear 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.
• Towards Trace Metrics via Functor Lifting(1505.08105)

May 29, 2015 cs.LO
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 Eilenberg-Moore 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.
• Behavioral Metrics via Functor Lifting(1410.3385)

Oct. 13, 2014 cs.LO
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 fixed-point 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.
• Reduction of Event Structures under History Preserving Bisimulation(1403.7181)

June 30, 2014 cs.LO
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 well-known 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.
• A Logic for True Concurrency(1110.4094)

Jan. 17, 2014 cs.LO
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 Hennessy-Milner 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.
• Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets(0809.4115)

Oct. 21, 2008 cs.LO
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.