arXiv ScienceSearch

arXiv subjects

Francesco Di Cosmo

Publications and source records attributed to Francesco Di Cosmo.

4 recordsLinked to original sources

The Complexity of Coverability-Like Problems in Elementary Object Systems: Data-Nets to the Rescue

Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of coverability-like problems, including termination and boundedness, over EOSs. Since coverability and boundedness are undecidable in general on EOSs, we focus on the relevant fragment of conservative EOSs (cEOSs). Our technique interprets cEOSs into the framework of data nets, whose tokens carry data from an infinite domain, thus bridging the nesting and the data-aware paradigms. Specifically, we show that cEOS coverability-like problems are equivalent to the coverability-like problems over an interesting fragment, called channel-$\nu$PNs (c-$\nu$PNs), of data nets that extends $\nu$PN (featuring globally fresh name creation) with restricted forms of transfers with renaming. c-$\nu$PNs remain less expressive than Unordered Data Nets, which feature lossy name creation as well as powerful forms of whole-place operations and broadcasts. These reductions allow us to analyze cEOS coverability taking advantage of known results on data nets. We conclude that the complexity of cEOS coverability is double-Ackermanian, $\mathcal{F}_{\omega 2}$-complete, while termination and boundedness are non-primitive recursive.

cs.CC

Nets-within-Nets through the Lens of Data Nets

Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of the reachability problem of EOSs when subjected to non-deterministic token losses. It is known that this problem is equivalent to the coverability problem with no lossiness of conservative EOSs (cEOSs). We precisely characterize cEOS coverability into the framework of data nets, whose tokens carry data from an infinite domain. Specifically, we show that cEOS coverability is equivalent to the coverability of an interesting fragment of data nets that extends beyond $\nu$PNs (featuring globally fresh name creation), yet remains less expressive than Unordered Data Nets (featuring lossy name creation as well as powerful forms of whole-place operations and broadcasts). This insight bridges two apparently orthogonal approaches to PN extensions, namely data nets and NWNs. At the same time, it enables us to analyze cEOS coverability taking advantage of known results on data nets. As a byproduct, we immediately get that the complexity of cEOS coverability lies between $\mathbf{F}_{\omega 2}$ and $\mathbf{F}_{\omega^\omega}$, two classes beyond Primitive Recursive.

cs.CC

A Lower Bound on Conservative Elementary Object Systems Coverability

Elementary Object Systems (EOS) are a form of Petri Net (PN) where tokens carry internal PN. This model has been recently proposed for analysis of robustness of Multi Agent Systems. While EOS reachability is known to be undecidable, the decidability of coverability of its conservative fragment (where the type of internal PN cannot be completely deleted and, thus, is conserved) was proved a decade ago, no study charted its complexity. Here, we take a first step in this direction, by showing how to encode $\nu$PNs, a well studied form of PN enriched with data, into conservative EOS (cEOS). This yields a non-Primitive Recursive, $F_{\omega2}$ lower-bound on cEOS coverability.

cs.CC