In this paper we revisit some pioneering eorts to equip Petri nets with compact operational models for expressing causality. The models we propose have a bisimilarity relation and a minimal representative for each equivalence class, and they can be fully explained as coalgebras on a presheaf category on an index category of partial orders. First, we provide a set-theoretic model in the form of a a causal case graph, that is a labeled transition system where states and transitions represent markings and rings of the net, respectively, and are equipped with causal information. Most importantly, each state has a poset representing causal dependencies among past events. Our rst result shows the correspondence with behavior structure semantics as proposed by Trakhtenbrot and Rabinovich. Causal case graphs may be innitely-branchi ng and have innitely many states, but we show how they can be rened to get an equivalent nitely-branching model. In it, states only keep the most recent causes for each token, are up to isomorphism, and are equipped with a symmetry, i.e., a group of poset isomorphisms. Symmetries are essential for the existence of a minimal, often nite-state, model. This rst part requires no knowledge of category theory. The next step is constructing a coalgebraic model. We exploit the fact that events can be represented as names, and event generation as name generation. Thus we can apply the Fiore-Turi framework, where the semantics of nominal calculi are modeled as coalgebras over presheaves. We model causal relations as a suitable category of posets with action labels, and generation of new events with causal dependencies as an endofunctor on this category. Presheaves indexed by labeled posets represent the functorial association between states and their causal information. Then we dene a well-behaved category of coalgebras. Our coalgebraic model is still innite-state, but we exploit the equivalence between coalgebras over a class of presheaves and History Dependent automata to derive a compact representation, which is equivalent to our set-theoretical compact model. Remarkably, state reduction is automatically performed along the equivalence.
We can cite @cite_8 for the introduction of transitions systems for causality whose states are elements of presheaves, intended to model the causal semantics of the @math -calculus as defined in @cite_9 . However, the index of a state is a set of names, without any information about events and causal relations. The advantage of our index category is that it allows reducing the state-space in an automatic way, exploiting a standard categorical construction. This cannot be done in the framework of @cite_8 . Finally, an HD-automaton for causality has been described in @cite_2 , but it is derived as a direct translation of causal automata and its states do not take into account causal relations.
@cite_9 @cite_2 @cite_8
2048909687 2053839461 2037276526
We examine the meaning of causality in calculi for mobile processes like the π-calculus, and we investigate the relationship between interleaving and causal semantics for such calculi. We separate two forms of causal dependencies on actions of π-calculus processes, called subject and object dependencies: The former originate from the nesting of prefixes and are propagated through interactions among processes (they are the only form of causal dependencies present in CCS-like languages); the latter originate from the binding mechanisms on names. We propose a notion of causal bisimulation which distinguishes processes which differ for the subject or for the object dependencies. We show that this causal equivalence can be reconducted to, or implemented into, the ordinary interleaving observation equivalence. We prove that our encoding is fully abstract w.r.t. the two behavioural equivalences. This allows us to exploit the simpler theory of the interleaving semantics to reason about the causal one. In [San94b] a similar programme is carried out for location bisimulation [BCHK91], a non-interleaving spatial-sensitive (as opposed to causal-sensitive) behavioural equivalence. The comparison between the encodings of causal bisimulation in this paper, and of location bisimulation in [San94b], evidences the similarities and the differences between these two equivalences. The semantics of name-passing calculi is often defined employing coalgebraic models over presheaf categories. This elegant theory lacks finiteness properties, hence it is not apt to implementation. Coalgebras over named sets, called history-dependent automata, are better suited for the purpose due to locality of names. A theory of behavioural functors for named sets is still lacking: the semantics of each language has been given in an ad-hoc way, and algorithms were implemented only for the @p-calculus. Existence of the final coalgebra for the @p-calculus was never proved. We introduce a language of accessible functors to specify history-dependent automata in a modular way, leading to a clean formulation and a generalisation of previous results, and to the proof of existence of a final coalgebra in a wide range of cases. We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.