Generator of Petri nets which count double exponent 2^2^k after R.J.Lipton & J.Esparza constructs
C
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
LICENSE
README.md
depn
depn.c
depn.exe
depnz
depnz.c
depnz.exe
pn_de_3.ndr
pn_de_3.pdf
z3p.ndr
z3p.pdf

README.md

depn

Generator of Petri nets which count double exponent 2^2^k after R.J.Lipton & J.Esparza constructs

Description:

The generated net counts 2^2^k as a strong computer after Richard J. Lipton [1].

Well-structured net programs of Javier Esparza [2] have been encoded by Petri nets.

The following marking belongs to the reachability space: fin-INC_k=1; x_0=2, y_0=2, s'_0=2; x_1=4, y_1=4, s'_1=4; ...; x_k=2^2^k, y_k=2^2^k, s'_k=2^2^k. It is the only marking with fin-INC_k>0.

For a given k, the resulting net is composed of a single Block_0 and repeated (k-1) times Block_i.

Block_i includes subnets INC_{i+1}, TST-y_i, TST-x_i, DEC_i and variables (places) x_i, x'_i, y_i, y'_i, s_i, s'_i.

Connections of neighboring blocks reflect initialization of the next variables x_{i+1}, y_{i+1}, s'_{i+1} and recursive calls of the previous block's TST-y_{i-1}, TST-x_{i-1}:

                                                 x_{i+1}
                                       +----->   y_{i+1}
                                       |        s'_{i+1} 
                                       |
    +-------------+             +------+------+
+---| INC_i       |============>| INC_{i+1}   |---+
|   +-------------+             +-------------+   |
|                                                 |
|   +-------------+             +-------------+   |
+-->| TST-y_{i-1} |<------+     | TST-y_i     |<--+
|   +-------------+       |     +-------------+   |
|          |              |            |          |
|          v              |            V          |
|   +-------------+       |     +-------------+   |
|   | DEC_{i-1}   |       +-----| DEC_i       |   |
|   +-------------+       |     +-------------+   |
|          ^              |            ^          |
|          |              |            |          |
|   +-------------+       |     +-------------+   |
+-->| TST-x_{i-1} |<------+     | TST-x_i     |<--+
    +-------------+             +-------------+

Peculiarities of generating Petri nets in logical (.net) and graphical (.ndr) formats of system Tina are described in [3].

Command line formats:

depn k > pn_de_k.ndr

Parameters:

k an exponent to count 2^2^k (k>0).

Output (file) format:

.ndr "Time Petri nets graphic format" according to http://www.laas.fr/tina

Tools to display, edit, visualize, and analyze generated models:

Tina Toolbox for analysis of Petri nets and Time Petri nets http://www.laas.fr/tina

Small nets (k<=3) can be analyzed in graphical tool nd. For bigger nets we recommend using command line tools: sift - to build the marking graph and muse - to find required marking.

Exported from Tina, models are opened with other tools for Petri nets listed at http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/quick.html

Examples:

A. Graphical environment

depn 2 > pn_de_2.ndr

  • Generate Petri net to count 2^2^2=16

nd pn_de_2.ndr

  • Load the net into graphical environment of Tina.

Menue: "Tools - reachability analysis - verbose - OK"

  • Create marking graph

  • Save marking graph into file pn_de_2-tina-R.txt

  • Find the only marking having a token in place fin-INC_2 (p72): p8*2 p10*2 p13*2 p55*4 p56*4 p57*4 p108*16 p109*16 p110*16 p72

B. Command line tools

depn 3 > pn_de_3.ndr

  • Generate Petri net to count 2^2^3=256

sift pn_de_3.ndr -f "-p125"

  • Build the marking graph and search on-fly for markings which contain a token in p125 (fin-INC_3).

To start a search in a marking graph, we can determine the place number n (for the label fin-INC_k) either from graphical representation of the net in nd or via textual search on .ndr file for a given label or using the following expression based on the number of places in Block_0 and Block_i and offsets of the place in question within blocks: if k=1 then n=25 else n=54+(k-2)*53+18=53k-34. Note that marking graphs are rather big to tackle with them for k>4.

References:

  1. Richard J. Lipton, The Reachability Problem Requires Exponential Space, Technical Report 63, Yale University, 1976. http://www.cs.yale.edu/publications/techreports/tr63.pdf

  2. Javier Esparza, Decidability and Complexity of Petri Net Problems - An Introduction. LNCS 1491, 1996, 374-428. http://www7.in.tum.de/um/bibdb/esparza/course.pdf

  3. Dmitry A. Zaitsev, Generators of Petri Net Models. Computer Communication & Collaboration, Vol. 2, Issue 2, 2014, 12-25. http://www.bapress.ca/ccc/ccc2014_2/2_14011024.pdf


http://member.acm.org/~daze