A coalgebraic semantics for causality in Petri nets

DOI10.1016/J.JLAMP.2015.07.003zbMATH Open1330.68196OpenAlexW3098906682MaRDI QIDQ890619FDOQ890619

Authors Roberto Bruni, Ugo Montanari, Matteo Sammartino

Publication date 10 November 2015

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.06462

Petri nets presheaves coalgebras behavior structures causal case graphs HD-automata

Categorical semantics of formal languages (18C50) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: In this paper we revisit some pioneering efforts 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 firings of the net, respectively, and are equipped with causal information. Most importantly, each state has a poset representing causal dependencies among past events. Our first result shows the correspondence with behavior structure semantics as proposed by Trakhtenbrot and Rabinovich. Causal case graphs may be infinitely-branching and have infinitely many states, but we show how they can be refined to get an equivalent finitely-branching model. In it, states are equipped with symmetries, which are essential for the existence of a minimal, often finite-state, model. 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: 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. Then we define a well-behaved category of coalgebras. Our coalgebraic model is still infinite-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.

Recommendations

Cites Work

Cited In (9)

This page was built for publication: A coalgebraic semantics for causality in Petri nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q890619)