Atig, Mohamed Faouzi ;
Ganty, Pierre
Approximating Petri Net Reachability Along Contextfree Traces
Abstract
We investigate the problem asking whether the intersection of a contextfree language (CFL) and a Petri net language (PNL) (with reachability as acceptance condition) is empty. Our contribution to solve this longstanding problem which relates, for instance, to the reachability analysis of recursive programs over unbounded data domain, is to identify a class of CFLs called the finiteindex CFLs for which the problem is decidable. The kindex approximation of a CFL can be obtained by discarding all the words that cannot be derived within a budget k on the number of occurrences of nonterminals. A finiteindex CFL is thus a CFL which coincides with its kindex approximation for some k. We decide whether the intersection of a finiteindex CFL and a PNL is empty by reducing it to the reachability problem of Petri nets with weak inhibitor arcs, a class of systems with infinitely many states for which reachability is known to be decidable. Conversely, we show that the reachability problem for a Petri net with weak inhibitor arcs reduces to the emptiness problem of a finiteindex CFL intersected with a PNL.
BibTeX  Entry
@InProceedings{atig_et_al:LIPIcs:2011:3344,
author = {Mohamed Faouzi Atig and Pierre Ganty},
title = {{Approximating Petri Net Reachability Along Contextfree Traces}},
booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
pages = {152163},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897347},
ISSN = {18688969},
year = {2011},
volume = {13},
editor = {Supratik Chakraborty and Amit Kumar},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3344},
URN = {urn:nbn:de:0030drops33448},
doi = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2011.152},
annote = {Keywords: Petri nets, Contextfree Grammars, Reachability Problem}
}
Keywords: 

Petri nets, Contextfree Grammars, Reachability Problem 
Seminar: 

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Issue date: 

2011 
Date of publication: 

2011 