Bi-reachability in Petri nets with data

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Kamiński, Łukasz, Lasota, Sławomir
Format: Preprint
Published: 2024
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866916319729811456
author Kamiński, Łukasz
Lasota, Sławomir
author_facet Kamiński, Łukasz
Lasota, Sławomir
contents We investigate Petri nets with data, an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. We provide a decision procedure for the bi-reachability problem: given a Petri net and its two configurations, we ask if each of the configurations is reachable from the other. This pushes forward the decidability borderline, as the bi-reachability problem subsumes the coverability problem (which is known to be decidable) and is subsumed by the reachability problem (whose decidability status is unknown).
format Preprint
id arxiv_https___arxiv_org_abs_2405_16176
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Bi-reachability in Petri nets with data
Kamiński, Łukasz
Lasota, Sławomir
Computation and Language
Formal Languages and Automata Theory
Logic in Computer Science
We investigate Petri nets with data, an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. We provide a decision procedure for the bi-reachability problem: given a Petri net and its two configurations, we ask if each of the configurations is reachable from the other. This pushes forward the decidability borderline, as the bi-reachability problem subsumes the coverability problem (which is known to be decidable) and is subsumed by the reachability problem (whose decidability status is unknown).
title Bi-reachability in Petri nets with data
topic Computation and Language
Formal Languages and Automata Theory
Logic in Computer Science
url https://arxiv.org/abs/2405.16176