1. Motivation

One goal of the Model Checking Contest (MCC) is to progress the capabilities of verification tools for concurrent systems by assessing them on benchmarks of increasing complexity.

In this respect, one must notice that there exist instances of certain MCC benchmarks that have not been successfully handled by any tool so far.

There may be various explanations for this situation. One plausible explanation is based on the following observations:

Many models represent distributed agents that execute in parallel, synchronize, and communicate together. Such Petri net models can be often expressed in terms of communicating automata, or are automatically generated from higher-level concurrent languages, such as process calculi.

The current PNML standard does not allow to easily express the structure of such models. There exists a notion of page in PNML, but it is oriented towards graphical rather than semantic representation.

It is therefore highly desirable to provide the MCC competing tools with information about the concurrent structure of MCC benchmarks when such information is available, which is the case for those models obtained from higher-level specifications.

Clearly, such additional information should remain optional, so that competing tools are free to use it or not. To use a metaphor, the situation would be similar in a matrix-computation contest, where matrices would be provided as the central information, together with additional information on zero blocks, which certain tools may wish to take advantage of to improve their performance and scale to larger problems.

2. Nested-Unit Petri Nets (NUPN)

At present, information about the concurrent structure of MCC benchmarks is only provided for P/T nets that are ordinary (i.e., all arc weights are equal to one) and one-safe. Colored models and non-ordinary or non-safe P/T nets are not concerned.

To represent the concurrent structure, we rely of on the concept of Nested-Unit Petri Nets (NUPN) proposed in [Gar15] (see also [Gar89] [GS90] [GS06]). This approach is an upward-compatible extension of P/T nets and relies on a reduced number of definitions:

unit: in its simplest form, a unit is a set of places that belong to the same sequential process. Contrary to other approaches (e.g., "boxes"), units only encapsulate places and do not encapsulate transitions, which are left entirely independent from and orthogonal to units.

unit nesting: units can be nested hierarchically, so as to form a tree-like hierarchy of units nested within units. In many cases, it would be sufficient to have a flat set of units to model concurrent processes (p1 || p2 || ... || pn). However, hierarchical nesting is required for a compositional representation of process calculi terms that freely mix sequential and parallel composition, such as p1 ; (p2 || p3) ; p4.

root unit: at the top level, there is always one single unit, called the "root unit", which contains all other units.

sub-unit: the units directly (and not transitively) contained into a given unit are called the "sub-units" of that unit. A unit may have zero sub-units if it models a fully sequential process (i.e., without any internal concurrency).

local place: the places directly (and not transitively) contained into a given unit are called the "local places" of that unit. Each unit (possibly excepted the root unit) must have at least one local place. The local places of all units (possibly excepted the root unit) determine a partition of the set of places. Local places are sometimes also called "proper places".

firing rules: the existence of units has no effect on the transition firing rules, which remain those of standard Petri nets.

unit-safe property: a NUPN model is said to be unit-safe iff, for any reachable marking M and for any unit U:
- at most one local place of U has a token in M (this expresses the sequential character of units);
and
- if a local place of U has a token in M, then there is no token in any local place of any other unit U' different from U and containing U or contained in U (said differently, if a unit is active, all its ancestors and descendents are not active).
Therefore, if a net is unit-safe, units express linear inequality invariants on reachable markings, and tools may take advantage of such invariants to perform logarithmic reductions in the size of marking encodings.

3. Definition of the NUPN-toolspecific section

For MCC benchmarks with known information about their concurrent structure, this information is made available in a "toolspecific" section of the PNML file, i.e., an XML element enclosed between:

   <toolspecific tool="nupn" version="1.1">

and:

   </toolspecific>

that is located either inside the "net" element or inside the (supposedly unique) "page" element of the PNML file.

According to the conventions of the PNML format, all "toolspecific" sections (including the NUPN one) are optional, so that tools are free to process or ignore these sections.

To indicate which MCC models provide such additional information, a new structural property has been added to the MCC model forms. This property corresponds to the LaTeX macro \HasModelNestedUnits and is displayed as "nested units" in the PDF model forms. It is set to True if and only if the PNML file(s) of the model instance(s) has(ve) a NUPN-toolspecific section.

Note: there also exists an alternative, non-PNML, text-based format for representing Nested-Unit Petri Nets (see here for a definition of this format). MCC benchmarks for which \HasModelNestedUnits is True could be also provided in this format if some tools, which are not based on Petri net theory and do not embedd a PNML parser, want to participate to MCC.

The reminder of this section concisely defines the syntax and semantic constraints for NUPN-toolspecific sections. This presentation is mostly intended to users interested in quickly grasping how NUPN-toolspecific sections are organized, and to users who want to write or read such sections using hand-written generators or parsers. To also support XML-based automatic code generation, standardized definitions of the NUPN-toolspecific format using XSD (XML Schema Definition), DTD (Document Type Definitions), and RELAX NG are given in Section 5 below.

The contents of a NUPN-toolspecific section can be defined in five main steps, numbered from (a) to (e).

(a) The section should start with the following first line:
```
   <toolspecific tool="nupn" version="1.1">
```

(b) The section should continue with the following second line:
```
   <size places="P" transitions="T" arcs="A"/>
```
where P, T, and A respectively denote the number of places, transitions, and arcs contained in the Petri net. All numbers should be written in decimal form, without sign nor leading zeros.

Note: Such size information is not explicitly displayed as such in the PNML format, so it is convenient for human readers to find it at one single place in the NUPN-toolspecific section.

(c) The section should continue with the following third line:
```
   <structure units="U" root="R" safe="S">
```
where U is the number of units (including the root unit), R is the unique identifier of the root unit (see below), and S is either true if the author of the PNML file guarantees that the net satisfies the unit-safe property (this is often known by construction when the net is generated from higher-level languages), or false if the unit-safe property does not hold or if the author is unsure about it.

(d) Then, for each unit (units being enumerated in some unspecified order), the section should contain a sequence of four lines of the following form:
```
   <unit id="I">
      <places>PL</places>
      <subunits>UL</subunits>
   </unit>
```
where I is the (unique) identifier of the unit, PL is a space-separated list of place identifiers enumerating (in an unspecified order) the local places of unit I, and UL is a space-separated list of unit identifiers enumerating (in an unspecified order) the sub-units of unit I.

Unit identifiers obey the same lexical conventions as place and transition identifiers in PNML. They should have the XSD type ID. In absence of any obvious way of giving meaningful names to units, it is suggested to name them u0, u1, u2, etc.

The following XML-like shorthands are possible and even recommended:
- if PL is the empty list, <places></places> can be abbreviated as <places/>
- if UL is the empty list, <subunits></subunits> can be abbreviated as <subunits/>

(e) The section should end with the two following lines:
```
   </structure>
   </toolspecific>
```

4. Example of a NUPN-toolspecific section

At present (December 2014), the six following benchmarks have a NUPN-toolspecific section: ARMCacheCoherence, EnergyBus, MultiwaySync, ProductionCell, UtahNoC, and Vasy2003. However, this list is expected to grow with the introduction of new "surprise" models and with the addition of NUPN-toolspecific sections for already known benchmarks.

The following fragment taken from the PNML file of the MCC model ARMCacheCoherence (2014) illustrates the syntax of a NUPN-toolspecific section; this model has the typical "communicating automata" structure, as it consists of 12 concurrent units, all nested in a root unit "u0", which has no local places; noticeably, the number of units remains small, even when the numbers of arcs and transitions get large:

   <toolspecific tool="nupn" version="1.1">
      <size places="87" transitions="33676" arcs="246935"/>
      <structure units="13" root="u0" safe="true">
         <unit id="u0">
            <places>p0</places>
            <subunits>u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12</subunits>
         </unit>
         <unit id="u1">
            <places>p1 p2 p3 p4 p5</places>
            <subunits/>
         </unit>
         <unit id="u2">
            <places>p6 p7</places>
            <subunits/>
         </unit>
         <unit id="u3">
            <places>p8 p9</places>
            <subunits/>
         </unit>
         <unit id="u4">
            <places>p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24</places>
            <subunits/>
         </unit>
         <unit id="u5">
            <places>p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39</places>
            <subunits/>
         </unit>
         <unit id="u6">
            <places>p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50 p51 p52 p53 p54</places>
            <subunits/>
         </unit>
         <unit id="u7">
            <places>p55 p56 p57 p58 p59 p60 p61 p62 p63 p64 p65 p66 p67 p68 p69</places>
            <subunits/>
         </unit>
         <unit id="u8">
            <places>p70 p71</places>
            <subunits/>
         </unit>
         <unit id="u9">
            <places>p72 p73 p74</places>
            <subunits/>
         </unit>
         <unit id="u10">
            <places>p75 p76 p77 p78</places>
            <subunits/>
         </unit>
         <unit id="u11">
            <places>p79 p80 p81 p82</places>
            <subunits/>
         </unit>
         <unit id="u12">
            <places>p83 p84 p85 p86</places>
            <subunits/>
         </unit>
      </structure>
   </toolspecific>

5. Grammars for the NUPN-toolspecific section

5.1. XML Schema Definition (XSD)

This is an XSD description of the NUPN-toolspecific section:

   <?xml version="1.0" encoding="utf-8"?>
   <xsd:schema elementFormDefault="qualified" xmlns:xsd="http://www.w3.org/2001/XMLSchema">

   <xsd:element name="toolspecific">
      <xsd:complexType>
         <xsd:sequence>
            <xsd:element name="size" type="sizeType"/>
            <xsd:element name="structure" type="structureType"/>
         </xsd:sequence>
         <xsd:attribute name="tool" type="xsd:string" fixed="nupn"/>
         <xsd:attribute name="version" type="xsd:decimal" fixed="1.1"/>
      </xsd:complexType>
   </xsd:element>

   <xsd:complexType name="sizeType">
      <xsd:attribute name="places" type="xsd:positiveInteger" use="required"/>
      <xsd:attribute name="transitions" type="xsd:nonNegativeInteger" use="required"/>
      <xsd:attribute name="arcs" type="xsd:nonNegativeInteger" use="required"/>
   </xsd:complexType>

   <xsd:complexType name="structureType">
      <xsd:sequence>
         <xsd:element name="unit" type="unitType" maxOccurs="unbounded"/>
      </xsd:sequence>
      <xsd:attribute name="units" type="xsd:positiveInteger" use="required"/>
      <xsd:attribute name="root" type="xsd:IDREF" use="required"/>
      <xsd:attribute name="safe" type="xsd:boolean" use="required"/>
   </xsd:complexType>

   <xsd:complexType name="unitType">
      <xsd:sequence>
         <xsd:element name="places" type="placeList"/>
         <xsd:element name="subunits" type="unitList"/>
      </xsd:sequence>
      <xsd:attribute name="id" type="xsd:ID" use="required"/>
   </xsd:complexType>

   <xsd:simpleType name="placeList">
      <xsd:list itemType="xsd:IDREF"/>
   </xsd:simpleType>

   <xsd:simpleType name="unitList">
      <xsd:list itemType="xsd:IDREF"/>
   </xsd:simpleType>

   </xsd:schema>

There are additional syntactic and semantics constraints that are not captured by this XSD specification:

The order in which attributes occur should be respected, although attribute order is not significant in XML.
Only the canonical representation of positiveInteger and nonNegativeInteger is allowed, meaning that numbers should neither be preceded by leading zeros, nor by a "+" or "-" sign (the latter being meaningful only for zero).
In placeList and unitList, elements must be pairwise distinct; more generally, all constraints related to the correct partitioning of places and units are not expressed in XSD.

5.2. Document Type Definition (DTD)

This is a DTD description of the NUPN-toolspecific section:

   <!ELEMENT toolspecific (size, structure)>
   <!ATTLIST toolspecific
       tool NMTOKEN #FIXED "nupn" 
       version NMTOKEN #FIXED "1.1">
   <!ELEMENT size EMPTY>
   <!ATTLIST size
      places      NMTOKEN #REQUIRED
      transitions NMTOKEN #REQUIRED
      arcs        NMTOKEN #REQUIRED>
   <!ELEMENT structure (unit)+>
   <!ATTLIST structure
      units NMTOKEN #REQUIRED
      root  IDREF #REQUIRED
      safe  (true | false) #REQUIRED>
   <!ELEMENT unit (places, subunits)>
   <!ATTLIST unit
      id ID #REQUIRED>
   <!ELEMENT places (#PCDATA)*>
   <!ELEMENT subunits (#PCDATA)*>

This DTD is shorter but less stringent than the XSD specification above. These are additional restrictions that cannot be expressed in the DTD framework:

In the attributes of "size" and "structure", each NMTOKEN is expected to be an unsigned integer.
In the definition of "places", each #PCDATA is expected to be a place name, i.e., to match the IDREF type (as in PNML).
In the definition of "subunits", each #PCDATA is expected to be a unit name, i.e., to match the IDREF type.

5.3. RELAX NG (Compact Syntax) Schema Definition (RNC)

This is a RNC description of the NUPN-toolspecific section:

   element toolspecific {
      attribute tool { "nupn" },
      attribute version { "1.1" },
      element size {
         attribute places { xsd:positiveInteger },
         attribute transitions { xsd:nonNegativeInteger },
         attribute arcs { xsd:nonNegativeInteger },
         empty
      },
      element structure {
         attribute units { xsd:positiveInteger },
         attribute root { xsd:IDREF },
         attribute safe { xsd:boolean },
         element unit {
            attribute id { xsd:ID },
            element places {
               list { xsd:IDREF* }
            },
            element subunits {
               list { xsd:IDREF* }
            }
         }+
      }
   }

5.4. RELAX NG (XML Syntax) Schema Definition (RNG)

This is a RNG description of the NUPN-toolspecific section:

   <?xml version="1.0" encoding="UTF-8"?>
   <element name="toolspecific"
            xmlns="http://relaxng.org/ns/structure/1.0"
            datatypeLibrary="http://www.w3.org/2001/XMLSchema-datatypes">
      <attribute name="tool">
         <value>nupn</value>
      </attribute>
      <attribute name="version">
         <value>1.1</value>
      </attribute>
      <element name="size">
         <attribute name="places">
            <data type="positiveInteger"/>
         </attribute>
         <attribute name="transitions">
            <data type="nonNegativeInteger"/>
         </attribute>
         <attribute name="arcs">
            <data type="nonNegativeInteger"/>
         </attribute>
         <empty/>
      </element>
      <element name="structure">
         <attribute name="units">
            <data type="positiveInteger"/>
         </attribute>
         <attribute name="root">
            <data type="IDREF"/>
         </attribute>
         <attribute name="safe">
            <data type="boolean"/>
         </attribute>
         <oneOrMore>
            <element name="unit">
               <attribute name="id">
                  <data type="ID"/>
               </attribute>
               <element name="places">
                  <list>
                     <zeroOrMore>
                        <data type="IDREF"/>
                     </zeroOrMore>
                  </list>
               </element>
               <element name="subunits">
                  <list>
                     <zeroOrMore>
                        <data type="IDREF"/>
                     </zeroOrMore>
                  </list>
               </element>
            </element>
         </oneOrMore>
      </element>
   </element>

6. References

[Gar89] Hubert Garavel. Compilation et Vérification de Programmes LOTOS. Thèse de Doctorat, Université Joseph Fourier (Grenoble), November 1989.

[GS90] Hubert Garavel and Joseph Sifakis. Compilation and Verification of LOTOS Specifications. Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), pages 379-394, June 1990.

[GS06] Hubert Garavel and Wendelin Serwe. State Space Reduction for Process Algebra Specifications. Theoretical Computer Science, 351(2) 131-145, February 2006.

[GS15] Hubert Garavel. Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets. Proceedings of the 36th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'15), Brussels, Belgium, June 2015.

For more information about Nested-Unit Petri Nets, see the definition of the NUPN file format and the manual pages of the PNML2NUPN and CAESAR.BDD tools. Notice that these tools do not compete against other tools in the MCC but are used by the MCC team to automatically fill in and validate model forms.

Hubert Garavel. Version 1.1 (Sept. 30, 2015).