Achraf Ghorbel
email: achraf.ghorbel@irisa.fr

Eric Anquetil
email: eric.anquetil@irisa.fr

Aurélie Lemaitre
email: aurelie.lemaitre@irisa.fr

Optimization analysis based on a breadth-first exploration for a structural approach of sketches interpretation

Keywords: Sketch recognition, breadth-first exploration, interactive recognition, 2D architectural floor plans

In this paper, we present an optimized approach, based on a competitive breadth-first exploration of the analysis tree, for an interactive interpretation of off-line sketch. The competitive breadth-first exploration of the analysis tree, allows to compare several hypotheses of interpretation to deal with confusion. Unfortunately, in practice these methods are rarely used because they often induce a large combinatory. This paper presents an optimization strategy to minimize the combinatory. The aim is to demonstrate the relevance of a competitive breadth-first exploration in off-line document analysis, in particular when the approach is interactive, ie the user is involved into the loop analysis. This paper demonstrates this optimized interactive analysis method on off-line handwritten 2D architectural floor plans.

I. INTRODUCTION

We generally identified two major approaches to document analysis: syntactic and statistical approaches. The syntactic approaches [START_REF] Fitzgerald | Mathpad: A fuzzy logic-based recognition system for handwritten mathematics[END_REF] [2] lean on prior knowledge of the document structure to drive the analysis. They are often based on visual languages for describing this knowledge and generate the analyzer. The statistical approaches [START_REF] Lemaitre | Preliminary experiments in layout analysis of handwritten letters based on textural and spatial information and a 2d markovian approach[END_REF] [START_REF] Montreuil | Unconstrained handwritten document layout extraction using 2d conditional random fields[END_REF] usually lack the ability to convey the hierarchical structure of the document and need a wide learning on a homogeneous and labeled base. While syntactic approaches can bring out the structural elements of the analysis document, statistical approaches provide a better ability to incorporate uncertainty. Our recent work [START_REF] Ghorbel | Interactive competitive breadth-first exploration for sketch interpretation[END_REF] is focused on designing a new approach for interpreting documents, described as interactive. While most syntactic approaches are based on a depthfirst exploration for interpreting structured document [START_REF] Coüasnon | Dmos, a generic document recognition method: Application to table structure analysis in a general and in a specific way[END_REF], we focused on the development of a breadth-first exploration allowing a confrontation, between several competitive hypotheses of interpretation for targeted context analysis. This strategy explicitly incorporate, if necessary, the user in the loop of analysis to raise ambiguities recognition [START_REF] Ghorbel | Interactive competitive breadth-first exploration for sketch interpretation[END_REF], or to enrich the a priori knowledge of the system [START_REF] Ghorbel | Incremental learning for interactive for sketch reconition[END_REF]. The user integration in the recognition loop avoids a fastidious a posteriori correction of errors recognition while allowing to have an auto-evolving system for interpreting sketches. Like all analysis methods based in breadth-first exploration, this approach induces a large combinatory.

In this paper, we focus on the optimization of the analysis strategy to reduce the engendered combinatory to obtain an analyzer that is really exploitable in the context of an interactive analysis; ie the user may be solicited by the analyzer during the interpretation phase to select the right hypothesis if the analyzer detects an ambiguity. This optimization is based on a dynamic limitation of the analysis tree branches depth. The analysis tree is optimally built at each stage of the document exploration. We validated this approach on the interactive analysis system for interpreting structured document (referred IMISketch) described in [START_REF] Ghorbel | Interactive competitive breadth-first exploration for sketch interpretation[END_REF]. The experiments are made on off-line handwritten 2D architectural floor plans.

The remaining of the paper is organized as follows. In the section II, we introduce principles of our existing interactive analysis method for interpreting sketches "IMISketch". The optimization strategy of breadth-first exploration is described in section III. Experimental results are reported in section IV and finally, section V concludes the paper.

II. PRINCIPLES OF THE RECOGNITION SYSTEM

IMISKETCH In this section, we summarize the principles of our interactive method "IMISketch". This analyzer is based on the following characteristics:

• a priori structural knowledge of the document are expressed through a visual language based on production rules; • a bidimensional descending breadth first analysis;

• the uncertainty is formalized by the attribution of scores to each hypothesis represented by the tree analysis branch; • a spatial contextual focus of the exploration to limit the combinatory; • if the ambiguities can not be resolved in the local context in an automatic manner, the user will be solicited by the analyzer to resolve the ambiguity. These characteristics have been defined to ensure better interaction between the process of analysis and the user. This interactivity allows in particular to avoid a posteriori the verification phase, which can become fastidious on complex

User intervention

Defining the local context

Building the analysis tree

Making the decision

Starting analysis : document to analyze

End of analysis : document analyzed Figure 1. Analysis process documents. Indeed, by appropriately soliciting the user on the critical phases of the analysis of the document, we avoid a cascade propagation of recognition error, which are very heavy to be a posteriori corrected. Figure 1 shows the complete process of analysis and the relationship between the three parts of the analyzer. The analyzer begins by defining a spatial contextual focus that aims to limit the combinatory exploration due to the breadth-first exploration of tree analysis. Once the context is well defined, the analyzer goes to build the analysis tree. In this stage, the analyzer develops all possible hypotheses of interpretation in the spatial context using a set of bidimensional rules that describe the structure of the document. These production rules are described by the context-driven constraint multiset grammars (CD-CMG) [START_REF] Macé | Eager interpretation of on-line handdrawn structured documents: The dali methodology[END_REF]. Each primitive can be interpreted in several ways. Each node or leaf is the application of a production rule deduced from the previous node. Every leaf or node of the tree has a score calculated from both its local score and the score obtained from the preceding nodes. Every score determines the adequacy degree to validate a production. The score calculated by each production is due to preconditions and constraints of the rule production (Equation 1). The use of the square root is a normalization using a geometric average. The production score can also be deduced from a classifier. A score is associated with each branch (hypothesis). Equation 2determines the degree of adequacy (score) of a hypothesis. |PS| is the number of production in the considered branch (referred as PS).

ρ P = √ µ preconditions .µ constraints (1)
ρ P S = ( Pi∈P S ρ Pi ) 1 |P S| (2)
The analysis tree then contains a set of complete or incomplete objects. An object is called complete if and only if this object can be in the final result of the document interpretation. For example, in the case of the architectural plan analysis, the complete object can be walls, doors, windows... An incomplete objects are intermediate objects that can not exist in the final result of the analysis. In the case of the architectural plan analysis, we can find incomplete objects such as segment representing the beginning of an opening. Once tree analysis is explored, the analyzer starts the final phase: the decision making phase. The role of the decision process is to validate the right hypothesis among a set of competing hypotheses generated with a descending breadth first analysis. Sometimes the decision process is not sure to make the right decision by validating the best hypothesis (because it has a score too low or it enters into confusion with the other hypotheses). In this case, it solicits the user. In practice, if the difference of scores between the top two branches is below a threshold of confidence and if these two branches are contradictory (at least one joint primitive is not consumed by the same rule production). When the correct root is validated, other roots are put on hold and the new roots are either the sons of this root if exists, or the waiting roots otherwise and the analyzer takes the first step (defining the local context step). The analysis is complete when no production rule is applicable. To assimilate this approach, we present in the following paragraph an example of interpretation of an architectural plan part.

A. Example of interactive breadth-first exploration

We present an example of image recognition of handwritten architectural plans consisting of walls, doors and windows. For this, we consider a set of production rules modeling architectural plans. These rules are illustrated in Figure 2. These rules express that at the end of a wall, we can find either a wall or an opening (door or window). An opening is located between two collinear walls. A sequence means an incomplete opening. We find in these rules, three complete objects: wall, door and window, and two incomplete objects: sequence and opening. In this example, the analysis is run on a set of primitives extracted from an architectural plan. After the segment extraction phase, the analysis defines the local context. The placement of this context in the document depends on the element consumed by the root interpretation. Figure 3 shows the movement of the local context between two phases of successive placement of the context. The construction phases of the tree deducted at this move are shown in Figure 4. The analyzer develops the tree as long as the following conditions (referred to as "IMISketch Conditions") are verified:

1) the newly consumed element is in the local context of research; 2) the number of consumed elements in each case (branch) is below a threshold; Despite the use of local context in IMISkech, the problem of combinatory and therefore computing time, is an important problem that must be addressed to meet the criteria for acceptability and usability of this type of interactive analysis with a user. This problem is mainly due to the number of applied production rules in the local context. We note that the development of certain nodes in tree analysis is useless. We propose in the following section the different optimization strategies in the analysis process to solve the combinatory problem due to the development the tree analysis.

III. STRATEGIES FOR REDUCING THE COMBINATORY

The construction of the tree based on a breadth-first exploration allows to have several competitive hypotheses. Unfortunately some production rules applied in a tree are invalidated by the system. In this section, we propose a new algorithm applied in the construction of tree analysis in order to develop the useful nodes for the right decision making. This algorithm is described below:

• If the number of analysis tree root is equal to 1:

1) limit the development of direct son of the root.

If the root to develop is unique, we can say that only one interpretation is possible for the consumed element. The process of decision making is then sure to validate the right root (because it is unique). In this case, since we know the root to be validated, we consider unnecessary to build all tree analysis, and we can limit the tree development to direct son nodes. After validation of this root, theses direct sons will be the new roots to build.

• If the number of analysis tree root is greater than 1: 1) regroup the roots by consumed elements. We will not build all roots but only those that share the same elements. We want to find the right interpretation for consumed the element within the root. 2) order these groups by their scores. Each group has a score derived from the roots within it. This score is the score of the best hypothesis (branch) located in the group. 3) develop only roots belonging to the group having the best score. 4) build analysis tree as long as the following conditions are verified:

the newly consumed element is in the local context of research (already used by IMISketch); the number of consumed elements in each hypothesis (branch) is below a threshold (already used by IMISketch); the number of complete elements belonging to a branch is less than a second threshold. We can fix a threshold to 3 for the architectural plans. The local context is not only limited to the distance between primitives but also to the number of complete elements in hypothesis. This optimization can generate a lack of information on hypotheses and therefore a possible ambiguity. But thanks to interactivity, this insufficiency does not influence on the final result as far as the user may be solicited to validate the right hypothesis. All these optimizations allow to develop an interactive analysis of structured documents based on a in breadth-first exploration of the tree analysis, by reducing the major problem of the breadth-first exploration: combinatoriy problem.

A. Comparison: IMISketch Vs optimized IMISketch

In this example, the aim is to show the improvements deduced from the new algorithm for building analysis trees. To facilitate this comparison, we present an example of an artificial tree analysis. The goal is to compare, for each step, the number of nodes developed by IMISketch and one induced by the new algorithm to build analysis tree.

IV. EXPERIMENTAL RESULTS

In this section we report results obtained from the different optimizations described in section III on the interactive method of document analysis. The aim of this optimization is to reduce the analysis time of the document to meet the criteria for acceptability and usability of the system. The experiments were carried on 80 architectural plans of varying complexity drawn by around ten different people. Each architectural plan is composed of a set of walls, doors, windows and sliding windows. Figure 7 shows the total (a) Construction method of the analysis tree using IMISketch (b) Construction method of the analysis tree using optimized IMISketch. The roots (n1, n2) belonging to the same group (Group 1) (same consumed elements) result of the interpretation, we find that the optimizations performed do not affect the system performance. Indeed, we observe a very light difference between IMISketch and optimized IMISketch in terms of recognition. We attain a recognition rate (without user solicitation) 95.25% with IMISketch and 96.17% with optimized IMISketch (see Figure 9). The user solicitation, during the analysis phase, can improve the recognition performance. Then, we attain 97.15% with IMISketch and 97.31% with optimized IMISketch (see Figure 10). Figure 11 shows the solicitation percentage of users during the analysis loop versus the total number of interpreted roots and the useful solicitations percentage compared to the total solicitation, ie solicitations that allow improving recognition. Each element interpretation, the hypotheses proposed by the two methods (IMISketch and optimized IMISketch) are not the same (Figures 5 and6). IMISketch produces more hypotheses than optimized IMISketch (see section III-A). The number of competing hypotheses is more important in IMISketch than optimized IMISketch, this might suggest that there have been more chance to have the right hypothesis with IMISketch, but the generated confusions are also potentially more numerous. In the end, one in the other, the results in terms of performance are very comparable. The found errors (about 3%) are due either to poor calibration of the local context, or the badly drawing of certain symbols. Figure 12 shows the difference of the computing time between IMISketch and optimized IMISketch for each architecture plan analysis. Depending on the complexity of the plans, the gain of computing time can reach 86% per image (image of index 62). We went from 16 hours and 22 minutes of accumulated computing time to 7 hours and one minute. This representing a gain of 57%. The experimental results are very encouraging. They suggest that it is possible to introduce descending breadth first analysis by controlling the generated combinatory. This supports the idea of conceiving an interactive systems for the document recognition. User solicitations, driven by analyzer, guarantee the obtaining of very high rate of reliability even when considering the complex documents treatment. V. CONCULSION In this paper, we have presented an optimizating strategy for solving combinatory generated by an interactive analysis based on breadth-first exploration for the sketch recognition. This strategy is based on a dynamic construction of analysis tree by controlling the depth of each branch following a set of criteria specified in the current zone of interest of document. This optimization strategy has been validated and tested on an interactive analyzer for interpreting architectural plans. Note that this optimization approach is generic Future work will focus on extending the experimental results on large image databases containing more complex architectural plans (integration of furniture, quotes, etc.)... We will also validate the criteria of acceptability and usability of the system by doing usage tests that will be conducted in collaboration with experts from the laboratory uses "Loustic" (http ://www.loustic.net/rennes).

Figure 2 .

 2 Figure 2. Example of production rules used for the architectural plans

Figure 3 .

 3 Figure 3. Document being analyzed and position of the local context (box) during the analysis

Figure 4 .

 4 Figure 4. The analysis trees associated with Figures 3(a) et 3(b). (-) and (+) designate respectively the consumed elements and the created elements.

Figure 5 (

 5 a) shows the result of the exploration according to the IMISketch method. The number of interpretation (nodes) is equal to 80 interpretations. The tree construction based on the new algorithm generates only 6 interpretations (Figure 5(b)). Figures 6(a) et 6(b) illustrate the new analysis trees by moving the local context. After two successive construction stages of analysis trees, we went from 111 interpretations (IMISketch) to 28 interpretations (optimized IMISketch), which has a gain of about 75% of computation time. These optimizations are generic and do not depend on the category of structured document to analyze. The following section presents the results quantified from a lot of 80 images of handwritten architectural plans.

Figure 5 .

 5 Figure 5. Analysis tree at step n. Nodes modeled by circles refer to complete object. Nodes modeled by triangles refer to incomplete objects.

Figure 6 .Figure 7 .Figure 8 .

 678 Figure 6. Analysis tree at step n+1. Nodes modeled by circles refer to complete object. Nodes modeled by triangles refer to incomplete objects. The grayed leaves indicate the new applied production rules in movement the local context. Number of architectural plans 80 Number of walls 3179 Number of doors 681 Number of windows 439 Number of sliding windows 509 Figure 7. Architectural plans symbolsnumber of symbols found within the 80 plans. Figure8shows some examples of analyzed architectural plans. We launched the analysis process on the 80 plans twice. The first time with the basic method (IMISketch) and the second time with optimizations presented in section III. For each architectural plan, we compare the final result of the interpretation and the obtained computing time. At the final

Figure 12 .

 12 Figure 12. Gain of computing time per image

ACKNOWLEDGMENT

The authors would like to thank all the people who took part in the experiments. This work partially benefits from the financial support of the ANR Project Mobisketch.


Serge Haddad
email: haddad@lsv.ens-cachan.fr

Jean Mairesse
email: mairesse@liafa.jussieu.fr

Hoang-Thach Nguyen

Synthesis and Analysis of Product-form Petri Nets

Keywords: Petri nets, product-form, synthesis, complexity analysis, reachability, normalising constant

For a large Markovian model, a "product form" is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1) we provide a sound and complete set of rules for the synthesis; (2) we characterise the exact complexity of classical problems like reachability;

(3) we introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed.

Introduction

Product-form for stochastic models. Markovian models of discrete events systems are powerful formalisms for modelling and evaluating the performances of such systems. The main goal is the equilibrium performance analysis. It requires to compute the stationary distribution of a continuous time Markov process derived from the model. Unfortunately the potentially huge (sometimes infinite) state space of the models often prevents the modeller from computing explicitly this distribution. To cope with the issue, one can forget about exact solutions and settle for approximations, bounds, or even simulations. The other possibility is to focus on subclasses for which some kind of explicit description is indeed possible. In this direction, the most efficient and satisfactory approach may be the product-form method: for a model composed of modules, the stationary probability of a global state may be expressed as a product of quantities depending only on local states divided by a normalising constant.

Such a method is applicable when the interactions between the modules are "weak". This is the case for queueing networks where the interactions between queues are described by a random routing of clients. Various classes of queueing networks with product-form solutions have been exhibited [START_REF] Jackson | Jobshop-like Queueing Systems[END_REF][START_REF] Baskett | Open, closed and mixed networks of queues with different classes of customers[END_REF][START_REF] Kelly | Reversibility and Stochastic Networks[END_REF]. Moreover efficient algorithms have been designed for the computation of the normalising constant [START_REF] Reiser | Mean Value Analysis of Closed Multichain Queueing Networks[END_REF]. Product-form Petri nets. Due to the explicit modelling of competition and synchronisation, the Markovian Petri nets formalism [START_REF] Ajmone Marsan | Modelling with Generalized Stochastic Petri Nets[END_REF] is an attractive modelling paradigm. Similarly to queueing networks, product-form Markovian Petri Nets were introduced to cope with the combinatorial explosion of the state space. Historically, works started with purely behavioural properties (i.e. by an analysis of the reachability graph) as in [START_REF] Lazar | Markovian Petri Net Protocols with Product Form Solution[END_REF], and then progressively moved to more and more structural characterisations [START_REF] Li | Parametric Analysis of Stochastic Petri Nets[END_REF][START_REF] Henderson | A net level performance analysis of stochastic Petri nets[END_REF]. Building on the work of [START_REF] Henderson | A net level performance analysis of stochastic Petri nets[END_REF], the authors of [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF] establish the first purely structural condition for which a product form exists and propose a polynomial time algorithm to check for the condition, see also [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF] for an alternative characterisation. These nets are called Π 2 -nets.

Product-form Petri nets have been applied for the specification and analysis of complex systems. From a modelling point of view, compositional approaches have been proposed [START_REF] Balsamo | Methodological construction of product-form stochastic Petri nets for performance evaluation Journal of Systems and Software[END_REF][START_REF] Balsamo | Composition of product-form Generalized Stochastic Petri Nets: a modular approach[END_REF] as well as hierarchical ones [START_REF] Harrison | Catalina Hierarchically constructed Petrinets and product-forms[END_REF]. Application fields have also been identified like [START_REF] Ajmone Marsan | Modelling with Generalized Stochastic Petri Nets[END_REF] hardware design and more particularly RAID storage [START_REF] Harrison | Catalina Hierarchically constructed Petrinets and product-forms[END_REF] and (2) software architectures [START_REF] Balsamo | Performance engineering with product-form models: efficient solutions and applications Proceedings of the second joint WOSP/SIPEW international conference on Performance engineering[END_REF]. Open issues related to product-form Petri nets.

• From a modelling point of view, it is more interesting to design specific types of Petri nets by modular constructions rather than checking a posteriori whether a net satisfies the specification. For instance, in [START_REF] Esparza | Reduction and Synthesis of Live and Bounded Free Choice Petri Nets[END_REF], a sound and complete set of rules is proposed for the synthesis of live and bounded free-choice nets. Is it possible to get an analog for product-form Petri nets? • From a qualitative analysis point of view, it is interesting to know the complexity of classical problems (reachability, coverability, liveness, etc.) for a given subclass of Petri nets and to compare it with that of general Petri nets. For product-form Petri nets, partial results were presented in [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF] but several questions were left open. For instance, the reachability problem is PSPACE-complete for safe Petri nets but in safe product-form Petri nets it is only proved to be NP-hard in [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF]. • From a quantitative analysis point of view, an important and difficult issue is the computation of the normalising constant. Indeed, in product-form Petri nets, one can directly compute relative probabilities (e.g. available versus unavailable service), but determining absolute probabilities requires to compute the normalising constant (i.e. the sum over reachable states of the relative probabilities). In models of queueing networks, this can be efficiently performed using dynamic programming. In Petri nets, it has been proved that the efficient computation is possible when the linear invariants characterise the set of reachable markings [START_REF] Coleman | Product form equilibrium distributions and a convolution algorithm for stochastic Petri nets[END_REF]. Unfortunately, all the known subclasses of product-form nets that fulfill this characterisation are models of queueing networks! Our contribution. Here we address the three above issues. In Section 3, we provide a set of sound and complete rules for generating any Π 2net. We also use these rules for transforming a general Petri net into a related product-form Petri net. In Section 4, we solve relevant complexity issues. More precisely, we show that the reachability and liveness problems are PSPACE-complete for safe product-form nets and that the coverability problem is EXPSPACE-complete for general product-form nets. From these complexity results, we conjecture that the problem of computing the normalising constant does not admit an efficient solution for the general class of product-form Petri nets. However, in Section 5, we introduce a large subclass of product-form Petri nets, denoted Π 3 -nets, for which the normalising constant can be efficiently computed. We emphasise that contrary to all subclasses related to queueing networks, Π 3 -nets may admit spurious markings (i.e. that fufill the invariants while being unreachable).

The above results may change our perspective on product-form Petri nets. It is proved in [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF] that the intersection of free-choice and productform Petri nets is the class of Jackson networks [START_REF] Jackson | Jobshop-like Queueing Systems[END_REF]. This may suggest that the class of product-form Petri nets is somehow included in the class of product-form queueing networks. In the present paper, we refute this belief in two ways. First by showing that some classical problems are as complex for product-form Petri nets as for general Petri nets whereas they become very simple for product-form queueing networks. Second by exhibiting the large class of Π 3 -nets which can model complex behaviours (e.g. illustrated by the presence of spurious markings).

A conference version of the paper appeared in [START_REF] Haddad | Nguyen Synthesis and analysis of product-form Petri nets[END_REF]. The present version includes additional results (Subsection 2.2) together with full proofs of the results. (There is one exception, Proposition 4.3, for which the proof can be found in the arXiv version of the paper available at http://arxiv.org/ abs/1104.0291) Notations. We often denote a vector u ∈ R S by s u(s)s. The support of vector u is the subset

S ′ ≡ {s ∈ S | u(s) = 0}.
2 Petri nets, product-form nets, and Π 2 -nets Definition 2.1 (Petri net). A Petri net is a 5-tuple N = (P, T, W -, W + , m 0 ) where:

• P is a finite set of places;

• T is a finite set of transitions, disjoint from P ;

• W -, resp. W + , is a P × T matrix with coefficients in N;

• m 0 ∈ N P is the initial marking.

Below, we also call Petri net the unmarked quadruple (P, T, W -, W + ). The presence or absence of a marking will depend on the context.

A Petri net is represented in Figure 1. The following graphical conventions are used: places are represented by circles and transitions by rectangles. There is an arc from p ∈ P to t ∈ T (resp. from t ∈ T to p ∈ P ) if W + (p, t) > 0 (resp. W -(p, t) > 0), and the weight W + (p, t) (resp. W -(p, t)) is written above the corresponding arc except when it is equal to 1 in which case it is omitted. The initial marking is materialised: if m 0 (p) = k, then k tokens are drawn inside the circle p. Let P ′ ⊂ P and m be a marking then m(P ′ ) is defined by m(P ′ ) ≡ p∈P ′ m(p).

The matrix W = W + -W -is the incidence matrix of the Petri net. The input bag • t (resp. output bag t • ) of the transition t is the column vector of W -(resp. W + ) indexed by t. For a place p, we define • p and A marking m ′ is reachable from the marking m if there exists a firing sequence σ = t 1 . . . t k (k ≥ 0) and a sequence of markings m 1 , . . . , m k-1

p • similarly. A T-semi-flow (resp. S-semi-flow) is a Q-valued vector v such that W.v = (0, . . . , 0) (resp. v.W = (0, . . . , 0)). A symmetric Petri net is a Petri net such that: ∀t ∈ T, ∃t -∈ T, • t = (t -) • , t • = • t -. A free-choice net is a Petri net such that: ∀t, t ′ ∈ T , either • t ∩ • t ′ = ∅, or • t = • t ′ . A state machine is a Petri net such that: ∀t ∈ T, | • t| = |t • | = 1. A marked graph is a Petri net such that: ∀p ∈ P, | • p| = |p • | = 1.
m -• t + t • , denoted by m t -→ m ′ = m -• t + t • . p 1 p 2 t 1 t 2 t 3 t 4 2 2 2 2 W = -2 -1 1 2 2 1 -1 -2 . m 0 = (2, 0) .
such that m t 1 -→ m 1 t 2 -→ • • • t k-1 ---→ m k-1 t k -→ m ′ . We write in a condensed way: m σ -→ m ′ .
We denote by R(m) the set of markings which are reachable from the marking m. The reachability graph of a Petri net with initial marking m 0 is the directed graph with nodes R(m 0 ) and arcs

{(m, m ′ )|∃t ∈ T : m t -→ m ′ }.
Given (N , m 0 ) and m 1 , the reachability problem is to decide if m 1 ∈ R(m 0 ), and the coverability problem is to decide if

∃m 2 ∈ R(m 0 ), m 2 ≥ m 1 .
A Petri net (N , m 0 ) is live if every transition can always be enabled again, that is:

∀m ∈ R(m 0 ), ∀t ∈ T, ∃m ′ ∈ R(m), m ′ t -→. A Petri net (N , m 0 ) is bounded if R(m 0 ) is finite. It is safe or 1-bounded if: ∀m ∈ R(m 0 ), ∀p ∈ P, m(p) ≤ 1.

Product-form Petri nets

There exist several ways to define timed models of Petri nets, see [START_REF] Baccelli | Synchronization and Linearity[END_REF]. We consider the model of Markovian Petri nets with race policy. Roughly, with each enabled transition is associated a "countdown clock" whose positive initial value is set at random according to an exponential distribution whose rate depends on the transition. The first transition to reach 0 fires, which may enable new transitions and start new clocks. We adopt here the singleserver policy which means that the rate of a transition does not depend on the enabling degree of the transition. In the more general definition of product-form Petri nets [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF]Definition 8], rates may depend on the current marking in a restricted way. For the sake of readability, we have chosen a simpler version. Results of sections 3 and 4 still hold with the general definition. On the other hand, it is well-known that the complexity of the computation of the normalisation constant highly increases even for the simple case of queuing networks. Here also the results of section 5 are only valid with constant rates.

Definition 2.3 (Markovian PN).

A Markovian Petri net (with race policy) is a Petri net equipped with a set of rates (µ t ) t∈T , µ t ∈ R * + . The firing time of an enabled transition t is exponentially distributed with parameter µ t . The marking evolves as a continuous-time jump Markov process with state space R(m 0 ) and infinitesimal generator Q = (q m,m ′ ) m,m ′ ∈R(m 0 ) , given by:

∀m, ∀m ′ = m, q m,m ′ = t such that m t -→m ′ µ t , ∀m, q m,m = - m ′ =m q m,m ′ .
(2.1) W.l.o.g., we assume that there is no transition t such that • t = t • . Indeed, the firing of such a transition does not modifiy the marking, so its removal does not modify the infinitesimal generator. We also assume that

( • t 1 , t • 1 ) = ( • t 2 , t •
2 ) for all transitions t 1 = t 2 . Indeed, if it is not the case, the two transitions may be replaced by a single one with the summed rate.

An invariant measure is a non-trivial solution ν to the balance equations: νQ = (0, . . . , 0). A stationary distribution π is an invariant probability measure: πQ = (0, . . . , 0), m π(m) = 1. Definition 2.4 (Product-form PN). A Petri net is a product-form Petri net if for all rates (µ t ) t∈T , the corresponding Markovian Petri net admits an invariant measure ν satisfying:

∃(u p ) p∈P , u p ∈ R + , ∀m ∈ R(m 0 ), ν(m) = p∈P u mp p . (2.
2)

The existence of ν satisfying (2.2) implies that the marking process is irreducible (in other words, the reachability graph is strongly connected). In (2.2), the mass of the measure, i.e. ν(R(m 0 )) = m ν(m), may be either finite or infinite. For a bounded Petri net, the mass is always finite. But for an unbounded Petri net, the typical situation will be as follows: structural conditions on the Petri net will ensure that the Petri net is a product-form one. Then, for some values of the rates, ν will have an infinite mass, and, for others, ν will have a finite mass. In the first situation, the marking process will be either transient or recurrent null (unstable case). In the second situation, the marking process will be positive recurrent (stable or ergodic case).

When the mass is finite, we call ν(R(m 0 )) the normalising constant. The probability measure π(•) = ν(R(m 0 )) -1 ν(•) is the unique stationary measure of the marking process. Computing explicitly the normalising constant is an important issue, see Section 5.

The goal is now to get sufficient conditions for a Petri net to be of product-form. To that purpose, we introduce three notions: weak reversibility, deficiency, and witnesses.

Let (N, m 0 ) be a Petri net. The set of complexes is defined by

C = { • t | t ∈ T } ∪ {t • | t ∈ T }.
The reaction graph is the directed graph whose set of nodes is C and whose set of arcs is {( • t, t • )|t ∈ T }. It can be viewed as a state machine. Definition 2.5 (Weak reversibility: Π-nets). A Petri net is weakly reversible (WR) if every connected component of its reaction graph is strongly connected. Weakly reversible Petri nets are also called Π-nets.

The notion and the name "WR" come from the chemical literature. In the Petri net context, it was introduced in [7, Assumption 3.2] under a different name and with a slightly different but equivalent formulation. WR is a strong constraint. It should not be confused with the classical notion of "reversibility" (the marking graph is strongly connected). In particular WR, a structural property, implies reversibility, a behavioural one! Observe that all symmetric Petri nets are WR.

The notion of deficiency is due to Feinberg [START_REF] Feinberg | Lectures on chemical reaction networks[END_REF].

Definition 2.6 (Deficiency). Consider a Petri net with incidence matrix W and set of complexes C. Let ℓ be the number of connected components of the reaction graph. The deficiency of the Petri net is defined by: |C|ℓrank(W ).

The notion of witnesses appears in [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF].

Definition 2.7 (Witness). Let c be a complex. A witness of c is a vector wit(c) ∈ Q P such that for all transition t:

     wit(c) • W (t) = -1 if • t = c wit(c) • W (t) = 1 if t • = c wit(c) • W (t) = 0 otherwise ,
where W (t) denotes the column vector of W indexed by t.

Examples. Consider the Petri net of Figure 1. First, it is WR. Indeed, the set of complexes is C = {p 1 , p 2 , 2p 1 , 2p 2 } and the reaction graph is:

p 1 ↔ p 2 , 2p 1 ↔ 2p 2 ,
with two connected components which are strongly connected. Second, the deficiency is 1 since |C| = 4, ℓ = 2, and rank(W ) = 1. Last, one can check that none of the complexes admit a witness. The Petri net of Figure 4 is WR and has deficiency 0. Note that the witnesses may not be unique. Possible witnesses are: wit(2p 1 + q 1 ) = q 1 , wit(p 1 + q 2 ) = q 2 , wit(p 2 + q 3 ) = q 3 , wit(2p 2 + q 4 ) = q 4 . Another possible set of witnesses is {q 1 , q 2 , -q 2 , -q 1 }. Proposition 2.8 (deficiency 0 ⇐⇒ witnesses, in [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF]Prop. 3.9]). A Petri net admits a witness for each complex iff it has deficiency 0.

Next Theorem is a combination of Feinberg's Deficiency zero Theorem [START_REF] Feinberg | Lectures on chemical reaction networks[END_REF] and Kelly's Theorem [START_REF] Kelly | Reversibility and Stochastic Networks[END_REF]Theorem 8.1]. (It is proved under this form in [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF]Theorem 3.8].) Theorem 2.9 (WR + deficiency 0 =⇒ product-form). Consider a Markovian Petri net with rates (µ t ) t∈T , µ t > 0, and assume that the underlying Petri net is WR and has deficiency 0. Then there exists (u p ) p∈P , u p > 0, satisfying the equations:

∀c ∈ C, p:cp =0 u cp p t: • t=c µ t = t:t • =c µ t p: • tp =0 u • tp p . (2.
3)

The marking process has an invariant measure ν such that:

∀m, ν(m) = Φ(m) -1 p∈P u mp p .
Checking the WR, computing the deficiency, determining the witnesses, and solving the equations (2.3), all of these operations can be performed in polynomial-time, see [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF][START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF].

Summing up the above, it seems worth to isolate and christen the class of nets which are WR and have deficiency 0. We adopt the terminology of [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF].

Definition 2.10 (Π 2 -net). A Π 2 -
net is a Petri net which is WR and has deficiency 0.

Some properties of WR and deficiency zero nets

Let N = (P, T, W -, W + ) be a Petri net. Let W = W + -W -be the incidence matrix of N and let A be the incidence matrix of the reaction graph.

Consider at first free-choice nets. It was shown in [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF]Section 4.3] that for free-choice nets, WR implies deficiency zero. The converse does not hold for general free-choice nets. For instance, state machines always have deficiency zero [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF]Prop. 3.2], and may not be WR. For marked graphs, however, the converse is true, and stated below.

Proposition 2.11. The deficiency of a connected marked graph is either 0 or 1. A marked graph has deficiency zero if and only if it is WR.

Proof. Let N be a marked graph. According to [START_REF] Desel | Free Choice Petri Nets[END_REF]Prop. 3.16], the only T-semi-flows of N are a(1,

• • • , 1), a ∈ Q, hence rank(W ) = |T | -1. Since A is a C × T matrix, rank(A) ≤ |T |. Hence δ = rank(A) -rank(W ) ≤ 1.
The "if" direction of the second claim is trivial since a marked graph is a free-choice net. Consider the "only if" direction. Let N be a deficiency zero marked graph. Let 1 be the column vector (1, . . . , 1) of size T . Since N is a marked graph, we have W • 1 = (0, . . . , 0). By Proposition 2.8, A = BW for some Q-valued matrix B. So we have A • 1 = BW • 1 = (0, . . . , 0). This implies that the connected components of the reaction graph must be strongly connected. Indeed pick a connected component which is not strongly connected. It admits a partition of its complexes into two subsets C 1 and C 2 such that there at least one transition t from C 1 to C 2 and no transition from C 2 to C 1 . Then vector x defined by x(c) = 0 for c ∈ C 1 and x(c) = 1 for c ∈ C 2 fulfills x.A ≥ 0 and x.A(t) > 0. Thus x.A.1 > 0 yields a contradiction. So N is WR. Proposition 2.12. For a live and bounded Petri net, deficiency zero implies weak reversibility.

Proof. Let m o be a marking such that (N , m 0 ) is live and bounded. We assume that N has deficiency 0 but is not WR. Then there exists a terminal strongly connected component C of the reaction graph and a transition t 0 such that t • 0 ∈ C and • t 0 / ∈ C. We claim that for every vector v ∈ Q T such that for all t ∈ T , v(t) ≥ 0 and v(t 0 ) > 0, we have Av = (0, . . . , 0). Indeed,

c∈C (Av)(c) = c∈C t∈T v(t) 1 t • =c -1• t=c = t∈T -{t 0 } v(t) c∈C 1 t • =c -1• t=c + v(t 0 ) . Since C is a terminal strongly connected component, c∈C 1 t • =c -1• t=c is either 0 or 1 for all t ∈ T . Hence c∈C (Av)(c) ≥ v(t 0 ) > 0. The claim is proved.
Since (N , m 0 ) is live and bounded, there exists a strictly positive T-semi-

flow v ∈ Q T [9, Theorem 2.38], that is: ∀t, v(t) > 0, W • v = (0, . . . , 0)
. Now recall that the deficiency of N is 0. According to Proposition 2.8, there exists a C ×P matrix B such that A = BW . We get Av = BW v = (0, . . . , 0). This contradicts the above claim.

A home marking is a marking which is reachable from every reachable marking. Having a home marking is an important property for Markovian Petri nets. Indeed, a Petri net has a home marking iff its reachability graph has only one terminal strongly connected component. And this last condition is required for the marking process to be ergodic. Proposition 2.13. Let N be a deficiency zero Petri net. Then N is WR iff there exists a marking m 0 such that (N , m 0 ) is live and m 0 is a home marking.

Proof. Suppose that N is WR. Let m 0 be a marking which enables every transition. The definition of weak reversibility implies that every arc of the reachability graph belongs to a cycle, so the reachability graph is strongly connected, that is m 0 is a home marking. The liveness follows trivially. Now suppose that there exists a marking m 0 such that (N , m 0 ) is live and m 0 is a home marking but N is not WR. We proceed as in the proof of Prop. 2.12. Let C be a terminal strongly connected component of the reaction graph and let t be a transition such that t • ∈ C and • t / ∈ C. Since (N , m 0 ) is live there is a path γ 1 in the reachability graph from m 0 to m 1 which enables t. Let m ′ 1 be the marking reached by the firing of t, since m 0 is a home marking there is a path γ 2 from m ′ 1 to m 0 . Thus γ = γ 1 tγ 2 is a (directed) cycle of the reachability graph of (N , m 0 ). Let v be the N T column vector such that: ∀u ∈ T , v(u) is the number of occurrences of u in γ. Clearly, v(t) > 0 and W.v = (0, . . . , 0). The end of the argument follows from the claim inside the proof of Prop. 2.12.

The interest of Prop. 2.13 is twofold. On the one hand, it connects weak reversibility and deficiency zero which are two independent properties ( [START_REF] Mairesse | Deficiency Zero Petri Nets and Product Form[END_REF]). On the other hand, it shows that the only deficiency zero and live Markovian Petri nets which are ergodic are the Π 2 -nets.

Figure 2 recapitulates the relations between deficiency and weak reversibility. The shaded cells correspond to impossibilities. For instance, no WR free-choice nets have strictly positive deficiency.

WR Not WR δ = 0 δ > 0 State machines WR Not WR δ = 0 δ > 0 Marked graphs WR Not WR δ = 0 δ > 0 Free-choice nets WR Not WR δ = 0 δ > 0
Live and bounded nets and nets which have a live home marking

Synthesis and regulation of Π 2 -nets

The reaction graph, defined in Section 2.1, may be viewed as a Petri net (state machine). Let us formalise this observation. The reaction Petri net of N is the Petri net A = (C, T, W -, W + ), with for every t ∈ T :

• W -( • t, t) = 1 and ∀u = • t, W -(u, t) = 0 • W + (t • , t) = 1 and ∀u = t • , W + (u, t) = 0

Synthesis

In this subsection, we consider unmarked nets. We define three rules that generate all the Π 2 -nets. The first rule adds a strongly connected state machine.

Definition 3.1 (State-machine insertion). Let N = (P N , T N , W - N , W + N ) be a net and M = (P M , T M , W - M , W + M ) be a strongly connected state machine disjoint from N . The rule S-add is always applicable and N ′ = S-add(N , M) is defined by:

• P ′ = P N ⊔ P M , T ′ = T N ⊔ T M ; • ∀p ∈ P N , ∀t ∈ T N , W ′-(p, t) = W - N (p, t), W ′+ (p, t) = W + N (p, t); • ∀p ∈ P M , ∀t ∈ T M , W ′-(p, t) = W - M (p, t), W ′+ (p, t) = W + M (p, t); • All other entries of W ′-and W ′+ are null.
The second rule consists in substituting to a complex c the complex c+λp. However in order to be applicable some conditions must be fulfilled. The first condition requires that c(p) + λ is non-negative. The second condition ensures that the substitution does not modify the reaction graph. The third condition preserves deficiency zero. Observe that the third condition can be checked in polynomial time, indeed it amounts to solving a system of linear equations in Q for every complex. Definition 3.2 (Complex update). Let N = (P, T, W -, W + ) be a Π 2 -net, c be a complex of N , p ∈ P , λ ∈ Z \ {0}. The rule C-update is applicable when:

1. λ + c(p) ≥ 0; 2. c + λp is not a complex of N ; 3. For every complex c ′ there exists a witness wit(c ′ ) s.t. wit(c ′ )(p) = 0. The resulting net N ′ = C-update(N , c, p, λ) is defined by:

• P ′ = P , T ′ = T ; • ∀t ∈ T s.t. W -(t) = c, W ′-(t) = W -(t), ∀t ∈ T s.t. W -(t) = c, W ′-(t) = c + λp • ∀t ∈ T s.t. W + (t) = c, W ′+ (t) = W -(t), ∀t ∈ T s.t. W + (t) = c, W ′+ (t) = c + λp.
The last rule "cleans" the net by deleting an isolated place. We call this operation P-delete. Definition 3.3 (Place deletion). Let N = (P, T, W -, W + ) be a net and let p be an isolated place of N , i.e. W -(p) = W + (p) = 0. Then the rule P-delete is applicable and N ′ = P-delete(N , p) is defined by:

• P ′ = P \ {p}, T ′ = T ; • ∀q ∈ P ′ , W ′-(q) = W -(q), W ′+ (q) = W + (q).
Proposition 3.4 shows the interest of the rules for synthesis of Π 2 -nets.

Proposition 3.4 (Soundness and Completeness). Let N be a Π 2 -net.

• If a rule S-add, C-update or P-delete is applicable on N then the resulting net is still a Π 2 -net. • The net N can be obtained by successive applications of the rules S-add, C-update, P-delete starting from the empty net.

Proof. Soundness. The case of P-delete is straightforward. Since we delete an isolated place, the reaction graph is unchanged. So the net is still WR. Assume that we delete an isolated place p and that p occurs in a witness wit(c) of some complex c. Then wit(c)wit(c)(p) is also a witness of c.

Let us examine the application of rule S-add(N , M). The state machine M constitutes a new component of the reaction graph. Since M is strongly connected, the new net is still WR. The witness of complexes associated with N are unchanged. Let q be a place of M; by definition of state machines this place is self-witnessing i.e. wit(q) = q. Thus the new net has deficiency zero.

Let us examine the application of the rule C-update(N , c, p, λ). By the second condition of its application the reaction graph of the new net is the same as the original one (with c + λp instead of c). So the new net is WR. Due to the third condition, the witness of c ′ = c is unchanged and the witness of c + λ • p is the one of c.

Completeness. Let N = (P, T, W -, W + ) be a Π 2 -net. We proceed as follows to generate N via our rules. At any stage of the generation, N cur denotes the current net. Initially N cur is the empty net.

First step. Let A 1 , . . . , A n be the strongly connected state machines corresponding to the components of the reaction net of N . Given a complex c of N , the corresponding place in the state machine is denoted q c . We apply the rules S-add(N cur , A i ) for i from 1 to n. At this stage, N cur has T for set of transitions and a place q c for every complex c of N . Furthermore, q c has for input (resp. output) transitions the input (resp. output) transitions of c in N . The complexes of N cur are the places q c and they are their own witnesses.

Second step. It consists in adding the places of P in such a way that the net N cur restricted to the places of P is N . At every stage of this step, given a complex c = p∈P c(p)p of N , there is a corresponding complex c ′ = q c + p∈P ∩Pcur c(p)p in N cur . For every place p ∈ P , we add p to N cur by rule S-add (an isolated place is a strongly connected state machine) and for every complex c of N such that c(p) > 0, we apply the rule C-update(N cur , c ′ , p, c(p)). Let us check that this rule is applicable. First, c ′ (p) + c(p) = c(p) is positive. Second, c ′ + c(p)p is not a complex of N cur by construction. Third, for every complex c ′ of N cur , there is a witness consisting in the single place q c which is in a state machine A i (thus different from p). At the end of this step, N cur is the net N enlarged with the places of the state machines A i . Otherwise stated, every complex c ′ of N cur is equal to c + q c . Third step. This step consists in deleting the places of the state machines. We observe that the place q c only occurs in the complex c + q c . The net N being a Π 2 -net, every complex c ′ has a witness wit(c ′ ) in N . Then wit(c ′ ) is a witness for c ′ + q c ′ in N cur whose support does not contain q c . Thus the rule C-update(N cur , c + q c , q c , -1) is applicable. After its application, q c becomes isolated and can be deleted by the rule P-delete(N cur , q c ). At the end, we have obtained N . Example. We illustrate the synthesis process using our rules on the net numbered 5 in Figure 3. We have also indicated on the right upper part of this figure, the four complexes and their witnesses. Since the reaction Petri graph of this net has two state machines, we start by creating it using twice the insertion of a state machine (net 1). Then we add the place p 1 (a particular state machine). We update the complex c 1 (the single one where p 1 appears in the original net) by adding 3p 1 (net 2). Iterating this process, we obtain the net 3. Observe that this net is a fusion (via T the set of transitions) of the original net and its reaction Petri net. We now iteratively update the complexes. The net 4 is the result of transforming c 1 + 3p 1 into 3p 1 . Once c 1 is isolated, we delete it. Iterating this process yields the original net.

For modelling purposes, we could define more general rules like the refinement of a place by a strongly connected state machine. Here the goal was to design a minimal set of rules.

From non Π 2 -nets to Π 2 -nets

Below we propose a procedure which takes as input any Petri net and returns a Π 2 -net. The important disclaimer is that the resulting net, although related to the original one, has a different structural and timed behaviour.

So it is up to the modeller to decide if the resulting net satisfies the desired specifications. In case of a positive answer, the clear gain is that all the associated Markovian Petri nets have a product form.

Consider a Petri net N = (P, T, W -, W + , m 0 ) with set of complexes C. Assume that N is not WR. For each transition t, add a reverse transition t - such that • t -= t • and (t -) • = • t (unless such a transition already exists). The resulting net is WR. In the Markovian Petri net, the added reverse transitions can be given very small rates, to approximate more closely the original net. However, there is no theoretical guarantee of the convergence of steady-state distributions and in fact counter-examples can be exhibited. Now, to enforce deficiency 0, the idea is to compose a general Petri net with its reaction graph as in the illustration of Proposition 3.4. Definition 3.5. Consider a Petri net N = (P, T, W -, W + , m 0 ). Let m 0 be an initial marking for the reaction Petri net A. The regulated Petri net associated with N is defined as follows: The behaviours of the original and regulated Petri nets are different. In particular, the regulated Petri net is bounded, even if the original Petri net is unbounded. Roughly, the regulation imposes some control on the firing sequences. Consider the example of Figures 1 (original net) and 4 (regulated net). The places q 1 , q 2 , q 3 , q 4 correspond to the complexes 2p 1 , p 1 , p 2 , 2p 2 , respectively. The transitions t 1 and t 4 belong to the same simple circuit in the reaction graph. Let w be an arbitrary firing sequence. The quantity |w| t1 -|w| t4 is unbounded for the original net, and bounded for the regulated net.

A⊙N = P ⊔C, T, W -, W + , (m 0 , m 0 ) , W -= W - W - , W + = W + W + . Proposition 3.6. The regulated Petri net A ⊙ N is WR iff N is
p 1 p 2 q 2 q 3 q 1 q 4 t 1 t 2 t 3 t 4 2

Complexity analysis of Π 2 -nets

All the nets that we build in this section are symmetric hence WR. For every depicted transition t, the reverse transition exists (sometimes implicitly) and is denoted t -. It is well known that reachability and liveness of safe Petri nets are PSPACE-complete [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF]. In [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF], it is proved that reachability and liveness are PSPACE-hard for safe Π-nets and NP-hard for safe Π 2 -nets. The next theorem and its corollary improve on these results by showing that the problem is not easier for safe Π 2 -nets than for general safe Petri nets. Proof. Our proof of PSPACE-hardness is based on a reduction from the QSAT problem [START_REF] Papadimitriou | Computational Complexity[END_REF]. QSAT consists in deciding whether the following formula is true ϕ ≡ ∀x n ∃y n ∀x n-1 ∃y n-1 . . . ∀x 1 ∃y 1 ψ where ψ is a propositional formula over {x 1 , y 1 . . . , x n , y n } in conjunctive normal form with at most three literals per clause. Observe that in order to check the truth of ϕ, one must check the truth of ψ w.r.t. the 2 n interpretations of x 1 , . . . , x n while the corresponding interpretation of any y i must only depend on the interpretation of {x n , . . . , x i }.

Counters modelling. First we design a Π 2 -net N cnt that "counts" from 0 to 2 k -1. This net is defined by:

• P = {p 0 , . . . , p k-1 , q 0 , . . . , q k-1 };

• T = {t 0 , . . . , t k-1 }; • For every 0 ≤ i < k, • t i = p i + j<i q j and t • i = q i + j<i p j ; • For every 0 ≤ i < k, m 0 (p i ) = 1 and m 0 (q i ) = 0. Observe that for every reachable marking m and every index i, we have m(p i ) + m(q i ) = 1. Therefore m can be coded by the binary word ω = ω k-1 . . . ω 0 in which ω i = m(q i ). The word ω is interpreted as the binary expansion of an integer between 0 and 2 k -1. We denote by val(ω) the integer value associated with w. Consider w ∈ {0 k , 1 k }, there are two markings reachable from w which are w+ and w-such that val(w-) = val(w) -1 and val(w+) = val(w) + 1.

The figure below represents the reachability graph of the 3-bit counter. For a k-bit counter, the shortest firing sequence from 0 k to 1 k is σ k defined inductively by: σ 1 = t 0 and σ i+1 = σ i t i σ i .

For every complex c ≡ p i + j<i q j (resp. c ≡ q i + j<i p j ), a possible witness is wit(c) ≡ p i + j>i 2 j-i-1 p j (resp. wit(c) ≡ q i + j>i 2 j-i-1 q j ). Thus this subnet has deficiency 0.

To manage transition firings between the update of counters, we duplicate the counter subnet and we synchronize the two subnets as indicated in the figure below. For a duplicated k-bit counter, the shortest firing sequence from the marking with the two counters set to 0 k and place go marked to the marking with the two counters set to 1 k and place go marked is obtained by: σ 1 = t 0 and σ n+1 = σ n t n σ n where t i = t i t ′ i .

This net has still deficiency 0 since the complexes are just enlarged by the places go or go ′ and their witnesses remain the same.

Variable modelling. For reasons that will become clear later on, the two counter subnets contain n + 3 bits indexed from 0 to n + 2. The bits 1, . . . , n of counter cnt correspond to the value of variables x 1 , . . . , x n . Managing the value of variables y 1 , . . . , y n is done as follows. For every variable y i , we add the subnet described below on the left (observe that s i = r - i ) and modify the two counter subnets as described on the right.

When place y i (resp. ny i ) is marked, this corresponds to interpreting variable y i as true (resp. false). Changes of the interpretation are possible when place u i is marked. This is the role of the modification done on the counter subnet: between a firing of t i and t ′ i places {u j } j≤i are marked. With this construction, we get the expected behaviour: interpretation of a variable i can only be modified when the interpretation of a variable x j with j ≥ i is modified. The complexes of the counter subnet are enlarged with places u i and their witnesses remain the same since places in the support of these witnesses are not modified by transitions s i and r i . The new complex y i + u i (resp. ny i + u i ) has for witness y i (resp. ny i ). Thus the new net has still deficiency 0.

Modelling the checking of the propositional formula. We now describe the subnet associated with the checking of propositional formula ψ ≡ j≤m C j where we assume w.l.o.g.: (1) that every clause C j ≡ l j,1 ∨ l j,2 ∨ l j,3 has exactly three literals (i.e. variables or negated variables); and (2) that every variable or negated variable occurs at least in one clause. The left upper part of Figure 6 shows the Petri net which describes clause C j of the formula ψ. Places ℓ j,k (k = 1, 2, 3) represent the literals while places nℓ j,k represent the literal used as a proof of the clause, the place mutex j avoids to choose several proofs of the clause (and thus ensuring safeness), and finally place success j can be marked if and only if the evaluation of the clause yields true for the current interpretation and one of its true literal is used as a proof.

The complexes of this subnet are mutex j + ℓ j,k (resp. success j + nℓ j,k ) with witness -nℓ j,k (resp. nℓ j,k ). So the subnet has deficiency 0.

We now synchronise the clause subnets with the previous subnet in order to obtain the final net. Observe that in the previous subnet, transition t 0 (and t ′ 0 ) must occur after every interpretation change. This is in fact the role of bit 0 of the counter. Thus we constrain its firing by requiring the places success j to be marked as presented in the right upper part of Figure 6. Adding loops simply enlarges the complexes associated with t 0 and does not modify the incidence matrix. So the net has still deficiency 0.

It remains to synchronise the value of the variables and the values of the literals where the variables occur either positively or negatively. This is done in two steps. First ℓ j,k is initially marked if the interpretation of the initial Figure 6: Clause C j (left), synchronisation with t 0 (right) and with variables (below) marking satisfies ℓ j,k . Then we synchronize the value changes as illustrated in the lower part of Figure 6. Once again the complexes are enlarged and the witnesses are still valid since the places ℓ j,k do not belong to the support of any witness.

Choice of the initial and final marking for the net. Let us develop a bit the sequence σ n+3 in the two counter subnet in order to explain the choice of initial marking for this subnet:

σ n+3 = σ n+1 t n+1 t ′ n+1 σ n+1 t n+2 t ′ n+2 σ n+1 t n+1 t ′ n+1 σ n+1
We want to check all the interpretations of x i 's guessing the appropriate values of y i 's (if they exist). We have already seen that changing from one interpretation to another one (i.e. a counter incrementation or decrementation) allows to perform the allowed updates of y i . However given the initial interpretation of the x i 's we need to make an initial guess of all the y i 's. So our initial marking restricted to the counter subnet will correspond to the marking reached after σ n+1 t n+1 , i.e. corresponding to cnt = 2 n+1 (i.e. word 010 . . . 0), cnt ′ = 2 n+1 -1 (i.e. word 001 . . . 1) with in addition places go ′ , u i 's, mutex j 's and y i 's 1-marked; places ℓ j,k are marked according to the initial marking of places x i 's and y i 's as explained before. All the other places are unmarked. This explains the role of bit n + 1.

Furthermore, if we have successfully checked all the interpretations of the x i 's, the counters will have reached the value 2 n+2 -1 (corresponding to a firing sequence obtained from t ′ n+1 σ n+1 with possible updates of y i during change of interpretations). However we do not know what is the final guess for the y i 's. So firing transition t n+2 allows to set the y i 's in such a way that the final marking will correspond to cnt = 2 n+2 (i.e. word 10 . . . 0), cnt ′ = 2 n+2 -1 (i.e. word 01 . . . 1) with in addition places go ′ , u i 's mutex j 's and y i 's 1-marked; places ℓ j,k are marked accordingly. All the other places are unmarked. This explains the role of bit n + 2.

By construction, the net reaches the final marking iff the formula is satisfied. Observe that the checking of clauses can be partially done concurrently with the change of interpretation. However as long as, in the net, a clause C j is "certified" by a literal ℓ j,k (i.e. marking place success j and unmarking place ℓ j,k ) the value of the variable associated with the literal cannot change, ensuring that when t 0 is fired, the marking of any place success j corresponds to the evaluation of clause C j with the current interpretation.

Corollary 4.2. The liveness problem for safe Π 2 -nets is PSPACE-complete.

Proof. Observe that the transitions of the net of the previous proof are fireable at least once and so live by reversibility, implied by weak reversibility iff ϕ is true.

Let us now consider general (non-safe) Petri nets. Reachability and coverability of symmetric nets is EXPSPACE-complete [START_REF] Mayr | The complexity of the word problem for commutative semigroups an polynomial ideals[END_REF]. In [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF], it is proved that both problems are EXPSPACE-complete for WR nets (which include symmetric Petri nets). The next proposition establishes the same result for the coverability of Π 2 -nets.

Proposition 4.3. The coverability problem for Π 2 -nets is EXPSPACE-complete.

Proof. Since we already know that coverability for Π-nets belongs to EX-PSPACE [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF], it remains to prove that coverability for Π 2 -nets is EXPSPACEhard. In order to establish this result, we slightly adapt the reduction given in [START_REF] Mayr | The complexity of the word problem for commutative semigroups an polynomial ideals[END_REF] of the termination problem for a three counter machine where the values of counters are bounded by e n ≡ 2 2 n with n the size of (a representation of) the machine. Thus we first depict the original reduction and then we describe our modifications and explain why the reduction is still valid.

For a uniform presentation of the proof we assume w.l.o.g. that the machine has four counters (these more powerful machines include the original ones). The key ingredient is the concise management of counters and more precisely the zero test. Indeed one models a counter c i with i ∈ {1, 2, 3, 4} by two complementary places A i,n and B i,n . When the counter has value x, place A i,n contains x tokens and place B i,n contains e nx tokens. Testing (and decrementing) that the counter c i is greater than 0 is done as usual by an arc with weight 1 starting from A i,n . However this approach does not work for the zero test as it would require a (double) arc from B i,n with weight e n thus implying a net representation of size at least 2 n which would not be valid.

Thus the zero test is managed by an inductive construction (w.r.t. n) of "nested" subnets N k leading to a subnet (the union of these subnets) with size in O(n). Let us describe this construction. The main places are: B i,k with i ∈ {1, 2, 3, 4}, 0 ≤ k ≤ n containing at most e k tokens and safe places C i,k , F k and S k . The inductive properties are the following ones:

• In subnet l≤k N l , starting from marking S k + C i,k one may reach marking F k + C i,k + e k B i,k .
• Furthermore any marking reachable from

S k +C i,k +α i 1 B i 1 ,k +α i 2 B i 2 ,k + α i 3 B i 3 ,k ({i 1 , i 2 , i 3 } = {1, 2, 3, 4} \ {i}) with S k or F k marked is either S k +C i,k +α i 1 B i 1 ,k +α i 2 B i 2 ,k +α i 3 B i 3 ,k or F k +C i,k +e k B i,k +α i 1 B i 1 ,k + α i 2 B i 2 ,k + α i 3 B i 3 ,k .
Basic case k = 0. This case is straightforward: N 0 consists in four transitions when transition corresponding to i is figured below.

Inductive case. Assume that the inductive properties holds for k. The net corresponding to N k+1 is described below with the following convention: S corresponds to S k+1 and s corresponds to S k . The same convention applies to all names. Furthermore for sake of readability we have duplicated some places in the figure.

We first exhibit the firing sequence σ i,k+1 from S + C i to F + C i + e k+1 B i :

• S + C i t a,i --→ Q 1,i + s + c 1 • Q 1,i + s + c 1 σ 1,k --→ Q 1,i + f + c 1 + e k b 1 using the inductive hypothesis • Q 1,i + f + c 1 + e k b 1 t b,i --→ Q 2,i + s + c 2 + (e k -1)b 1 We now describe a firing sequence from Q 2,i + s + c 2 + (e k -j)b 1 + (j -1)e k B i + (j -1)b 4 to Q 2,i + s + c 2 + (e k -j -1)b 1 + je k B i + jb 4 for 1 ≤ j ≤ e k -1 -Q2,i + s + c2 + (e k -j)b1 + (j -1)Bi + (j -1)b4 σ 2,k
---→ Q2,i +f +c2 +(e k -j)b1 +e k b2 +(j -1)b4 using the inductive hypothesis

-Q2,i + f + c2 + (e k -j)b1 + e k b2 + (j -1)b4 (t c,i ) e k -----→ Q2,i + f + c2 + (e k -j)b1 + e k b3 + (j + 1)e k Bi + (j -1)b4 -Q2,i + f + c2 + (e k -j)b1 + e k b3 + (j + 1)e k Bi + (j -1)b4 t d,i --→ Q3,i + f + c3 + (e k -j)b1 + e k b3 + (j + 1)e k Bi + (j -1)b4 -Q3,i + f + c3 + (e k -1)b1 + e k b3 + (j + 1)e k Bi + (j -1)b4 σ - 3,k ---→ Q3,i + s + c3 + (e k -j)b1 + (j + 1)e k Bi + (j -1)b4 -Q3,i + s + c3 + (e k -j)b1 + (j + 1)e k Bi + (j -1)b4 t e,i --→ Q2,i + s + c2 + (e k -j -1)b1 + (j + 1)e k Bi + jb4
• After the previous iterations, when reaching Q 2,i +s+c 2 +(e k -1)e k B i + (e k -1)b 4 , we perform all the steps of the iteration except the last one reaching

Q 3,i + s + c 3 + (e k ) 2 B i + (e k -1)b 4 = Q 3,i + s + c 3 + e k+1 B i + (e k -1)b 4 . • Q 3,i + s + c 3 + e k+1 B i + (e k -1)b 4 t f,i --→ Q 4,i + f + c 4 + e k+1 B i + e k b 4 • Q 4,i + f + c 4 + e k+1 B i + e k b 4 σ - 4,k --→ Q 4,i + s + c 4 + e k+1 B i • Q 4,i + s + c 4 + e k+1 B i t g,i --→ F + C i + e k+1 B i
Let us now prove that any marking reachable from

S k + C i,k + α i 1 B i 1 ,k + α i 2 B i 2 ,k + α i 3 B i 3 ,k ({i 1 , i 2 , i 3 } = {1, 2, 3, 4} \ {i}) with S k or F k marked is either S k + C i,k + α i 1 B i 1 ,k + α i 2 B i 2 ,k + α i 3 B i 3 ,k or F k + C i,k + e k B i,k + α i 1 B i 1 ,k + α i 2 B i 2 ,k + α i 3 B i 3 ,k .
We first observe on the net above that the tokens contained in a place B j,k are frozen except when place C j,k is marked. Thus w.l.o.g. we assume that α 1 = α 2 = α 3 = 0.

So it remains to show that when deviating from the exhibited sequence one cannot reach a marking with S k marked different from the initial marking or a marking with F k marked different from the final marking. This is proven by a case study (see [START_REF] Mayr | The complexity of the word problem for commutative semigroups an polynomial ideals[END_REF]). Here we just handle one case since all cases are similar. When reaching marking

Q 2,i +f +c 2 +(e-j)b 1 +e k b 3 +(j +1)e k B i + (j -1)b 4 with 0 ≤ e < e k , one can fire transition t d,i reaching marking Q 3,i + f + c 3 + (e -j)b 1 + eb 3 + (j + 1)e k B i + (j -1)b 4 .
From this marking due to the inductive hypothesis, it is not possible to mark place s in subnet N k-1 . Thus transitions t e,i and t f,i are not fireable. So the only possible way to "progress" in N k consists to fire the reverse transition t - d,i coming back to the marking

Q 2,i + f + c 2 + (e -j)b 1 + e k b 3 + (j + 1)e k B i + (j -1)b 4 .
The subnet below describes the initial behaviour of the simulating net consisting in filling places B i,n (with i ∈ {1, 2, 3, 4}) with e n tokens and putting a token in q 0 the place corresponding to the initial state of the counter machine.

The simulation of an instruction : ifc i > 0 then c i --; goto q ′ else goto q ′′ is now simply performed by the following subnet. The validity of the zero test is ensured by the assertions about the subnet l≤n N l . Furthermore it can be proved that reverse transitions of the ones simulating transitions cannot help to mark place q f where q f is the final state of the counter machine (see [START_REF] Mayr | The complexity of the word problem for commutative semigroups an polynomial ideals[END_REF] or proposition 12 in [START_REF] Haddad | Silva Product-form and stochastic Petri nets: a structural approach[END_REF] for a simple proof of this claim).

We are now ready to explain the modifications that we bring to the simulating net. For every pair of transitions t and t -, we add a place p t input of one of the transitions and output of the other. Thus by construction p t and -p t are witnesses for t and t -. More precisely p t is the witness of the transition for which it is an output and -p t is the output of the other transition. Let us examine how these additional places modify the behaviour of the net. Since there is no new transition, firing sequences of the enlarged net are firing sequences of the original one. Thus we only have to care whether the simulation firing sequence is still a firing sequence.

For the transitions not belonging to the subnet l≤n N l , p t is an output of t. As the reversed transitions of these transitions do not occur in the simulating sequence, such places cannot disable a transition in the simulating sequence. We now observe that the sequences σ i,n and σ - i,n alternate in the simulating sequence, always starting by σ i,n . Thus in subnet N n , place p t is the output of the transition t. Now observe that in sequence σ i,n there is an occurrence of sequence σ 1,n-1 , e n-1 occurrences of σ 2,n-1 followed by σ - 3,n-1 and then an occurrence of σ 4,n-1 . Thus in subnet N n-1 , place p t is the output of the transition t (resp. t -) when t is t u,i with u ∈ {a, b, c, d, e, f, g} and i ∈ {1, 2} (resp. i ∈ {3, 4})using notations of the figure. The same pattern of occurrences also happens at lower levels. So more generally, in subnet N k with k < n, place p t is the output of the transition t (resp. t -) when t is t u,i with u ∈ {a, b, c, d, e, f, g} and i ∈ {1, 2} (resp. i ∈ {3, 4}). With this choice, the simulating sequence is still a firing sequence in the enlarged net and the marking to be covered is q f . The complexity of reachability for Π 2 -nets remains an open issue (indeed the proof of EXPSPACE-hardness does not work for reachability).

The subclass of Π 3 -nets

In this section, we introduce Π 3 -nets, a subclass of product-form Petri nets for which the normalising constant can be efficiently computed. The first subsection defines the subclass; the second one studies its structural properties and the third one is devoted to the computation of the normalising constant.

Definition and properties

P i = ∅ for all 1 ≤ i ≤ n, 2. M i = (P i , T i , W - |P i ×T i , W + |P i ×T i ) is a strongly connected state machine, 3. ∀1 ≤ i ≤ n , ∀t ∈ T i , ∀p ∈ P , • t(p) > 0 implies p ∈ P i or p ∈ P i-1 (P 0 = ∅), 4. ∀2 ≤ i ≤ n , ∃t ∈ T i , ∃p ∈ P i-1 s.t. • t(p) > 0, 5. ∀1 ≤ i ≤ n , ∀t, t ′ ∈ T i , ( • t ∩ • t ′ ) ∩ P i = ∅ implies • t = • t ′ .
We call M i the level i state machine. The elements of P i (resp. T i ) are level i places (resp. transitions). The complexes • t with t ∈ T i are level i complexes.

By weak reversibility, the constraints 3, 4, and 5 also apply to the output bags t • . An ordered Π-net is a sequence of strongly connected state machines. Connections can only be made between a level i transition and a level (i -1) place (points 1, 2, 3). By construction, an ordered Π-net is connected (point 4). For i > 1, each level i place belongs to one and only one level i complex (point 5). An example of ordered Π-net can be found on figure 7.

Lemma 5.2. The reaction net of N is isomorphic to the disjoint union of state machines M i . Consequently, a T -semi-flow of M i is also a T -semiflow of N . If a transition of T i is enabled by a reachable marking then every transition of T i is live.

Proof. Consider the mapping f which maps each complex t • , t ∈ T i , to p the output place of t in P i . By construction of ordered Π-nets, f is a bijection from C to P . Moreover, each arc c 1 → c 2 of the reaction graph corresponds to the transition t = f (c 1 ) • = • f (c 2 ). This proves the first point of the lemma. To prove the second point, recall that for a state machine, the T -semi-flows correspond to circuits of the Petri net graph. From this and from the first point, a T -semi-flow of M i defines a circuit of the reaction graph of N , which yields a T -semi-flow of N . The set of transitions T i is the set of transitions occurring in a component of the reaction graph. The third point follows.

An ordered Π-net may be interpreted as a multi-level system. The transitions represent jobs or events while the tokens in the places represent resources or constraints. A level i job requires resources from level (i -1) and relocates these resources upon completion. On the contrary, events occurring in level (i -1) may make some resources unavailable, hence interrupting activities in level i. The dependency of an activity on the next level is measured by potentials, defined as follows.

Definition 5.3 (Interface, potential). A place p ∈ P i , 1 ≤ i ≤ n -1, is an interface place if p ∈ t • for some t ∈ T i+1 . For a place p ∈ P i , 2 ≤ i ≤ n, and a place q ∈ P i-1 , set: pot(p, q) = t • (q) if p and q have a common input transition t ∈ T i 0 otherwise.

The potential of a place p ∈ P i , 2 ≤ i, is defined by:

pot(p) = q∈P i-1 pot(p, q) .
By convention, pot(p) = 0 for all p ∈ P 1 .

By the definition of ordered Π-nets, the quantity t • (q) does not depend on the choice of t, so the potential is well-defined. Indeed, by weak reversibility, the constraint 5 also applies to the output bags t • .

Example. The Petri net in Figure 7 is a 3-level ordered Π-net. The potentials are written in parentheses. To keep the figure readable, the arcs between the place p 1 and the level 2 transitions are not shown. (5.1)

p 3 (2) q 3 (1) r 3 (0) p 2 (2) q 2 (2) r 2 (1) p 1 2 2 level 3 level 2 level 1
Remark. Note that a marking witness is not necessarily non-negative. It can be showed by induction that:

′ = m + W (t) for some t ∈ T i (1 ≤ i ≤ n).
Let p 1 and p 2 denote the input place and the output place of t in P i , respectively. Then for every place p:

m ′ (p) = m(p) -1 if p is p 1 , m(p) + 1 if p is p 2 , m(p) otherwise. (5.2)
Proof. Since m and m ′ have the same restriction on ∪ j>i P j , we have m

′ (p) = m(p) ∀p ∈ (∪ j≥i P j ) \ {p 1 , p 2 }. It follows that m ′ (p 1 ) -m(p 1 ) = m ′ (p 1 ) - m(p 1 ) = -1 and m ′ (p 2 ) -m(p 2 ) = m ′ (p 2 ) -m(p 2 ) = 1. For p ∈ P i-1 ∩ t • , we have m ′ (p) -m(p) = pot(p 2 , p) -pot(p 1 , p), hence m ′ (p) -m(p) = m ′ (p) -m(p) -( m ′ (p 1 ) -m(p 1 ))pot(p 1 , p) +( m ′ (p 2 ) -m(p 2 ))pot(p 2 , p) = 0 Similarly, m ′ (p) -m(p) = 0 for p ∈ P i-1 ∩ • t. For all other places, m ′ (p) = m(p) and m ′ (r) = m(r) ∀r s.t. pot(r, p) = 0, thus m ′ (p) = m(p).
The above lemma applies in particular when m and m ′ are markings such that m t -→ m ′ . Equations (5.2) look like the equations for witnesses. Since each level i complex contains exactly one level i place, one guesses that every complex admits a witness, i.e. that N is a Π 2 -net. This is confirmed by the next proposition.

Proposition 5.6. Let B denote the P × P integer matrix of the linear transformation m → m defined by (5.1). For p ∈ P i , the line vector B(p) is a witness for the i-level complex containing p. In particular, N is a Π 2 -net.

Proof. Denote by A ∈ Z(C × T ) the incidence matrix of the reaction graph. From Lemma 5.5, we have:

m t -→ m ′ =⇒ m ′ -m = A(t) .
We have to show that BW (t) = A(t) ∀t ∈ T . Indeed, let m and m ′ be two markings such that m t -→ m ′ , we have:

BW (t) = B(m ′ -m) = m ′ -m = A(t).
Lemma 5.5 allows to derive relevant S-semi-flows of N and S-invariants.

Corollary 5.7. Let m 0 be the initial marking of N . We have: ∀m ∈ R(m 0 ), ∀i ∈ {1, . . . , n}, m(P i ) = m 0 (P i ) More generally, for all i, the vector v i = p∈P i B(p) is a S-semi-flow of N .

Using this corollary, it can be shown that an ordered Π-net is bounded.

Example. Consider the ordered Π-net in Figure 7 with the initial marking m 0 = p 3 + q 3 + r 3 + 4p 1 . The marking witness of m 0 is m 0 = p 3 + q 3 + r 3 -2p 2q 2 + 10p 1 . Any reachable marking m satisfies the invariants:

m(P 3 ) = 3 m(P 2 ) -2m(p 3 ) -m(q 3 ) = -3 m(p 1 ) -2m(p 2 ) -2m(q 2 ) -m(r 2 ) + 4m(p 3 ) + 2m(q 3 ) = 10
We shown that {v i , 1 ≤ i ≤ n} is a basis of the S-semi-flows of N . Proposition 5.8. Let v be an S-semi-flow of N , i.e. v.W = 0. There exist unique rational numbers a 1 , . . . , a n such that v = n i=1 a i v i . Proof. The matrix B is a P × P unit lower triangular matrix, so it is invertible. We have:

v.W = 0 =⇒ (v.B -1 )(BW ) = 0 =⇒ (v.B -1 )A = 0 , hence v.B -1
is an S-semi-flow of the disjoint union of the state machines M i . But since a state machine's only S-semi-flows are a(1, . . . , 1), a ∈ Q, there exist rational numbers a 1 , . . . , a k such that

v.B -1 = n i=1 a i w i , (5.3)
where w i ∈ Q P are defined by w i (p) = 1 P i (p). Right-multiplying both sides of (5.3) by B, we get v = n i=1 a i v i . The independence of the set {v i , 1 ≤ i ≤ n} follows from the fact that the vectors v i B -1 have non-empty disjoint supports.

We now consider only ordered Π-nets in which the interface places in P i have maximal potential among the places of P i . From the technical point of view, this assumption is crucial for the reachability set analysis presented later. From the modelling point of view, it is a reasonable restriction. Consider the multi-level model, the assumption means that during the executions of level i jobs, the level (i -1) is idle, therefore the amount of available resource is maximal.

Definition 5.9 (Π 3 -net). An ordered Π-net N is a Π 3 -net if: ∀i, ∀p ∈ P i : p ∈ • T i+1 =⇒ pot(p) = max{pot(q), q ∈ P i } .

The reachability set

From now on, N is a n-level Π 3 -net with M 1 , . . . , M n being its state machines.

the markings of R i (m), m(P i ) > 0 (otherwise, the transitions of T i would be dead).

We prove the reverse direction and the second part of the proposition by induction on i ≥ 1, i.e. : If m satisfies the i-condition then:

(1) for every p, q ∈ P i such that p = q, m(p) > 0 and pot(p) ≤ m(P i-1 ), there exists

m ′ ∈ R i (m) such that: m ′ (p) = m(p) -1 , m ′ (q) = m(q) + 1 , ∀r ∈ P i \ {p, q}, m ′ (r) = m(r) .
(2) m is i-live.

The case i = 1 is trivial. Suppose that the claim has been proven for all j ≤ i -1. Let m be a marking which satisfies the i-condition. Consider two cases: pot(p) = 0 and pot(p) > 0.

If pot(p) = 0 then the output transitions of p are enabled by m. For any arbitrary q = p, fire the transitions along a path from p to q in T i , we obtain a marking m ′ satisfying (5.5). So we have proved assertion [START_REF] Ajmone Marsan | Modelling with Generalized Stochastic Petri Nets[END_REF]. Now choose some q such that pot(q) > 0 (there is at least one). Then m ′ (P i-1 ) ≥ pot(q) > 0. By the induction hypothesis, m ′ is (i -1)-live. Moreover, m ′ enables the output transitions of q. Hence m ′ is i-live, which implies m is i-live.

If pot(p) > 0 then m(P i-1 ) > 0, hence m is (i -1)-live by the induction hypothesis. It remains to find a marking in R i-1 (m) which enables the output transitions of p. If for all r ∈ P i-1 , m(r) ≥ pot(p, r) then choose m. Otherwise, choose a marked place q of P i-1 such that pot(q) ≤ m(P i-2 ) and a level (i -1) interface place q ′ , then apply the induction hypothesis on (5.5) to find m 1 ∈ R i-1 (m) such that m 1 (q) = m(q) -1, m 1 (q ′ ) = m(q ′ ) + 1 and m 1 (r) = m(r) for every other places r of P i-1 . We have ϕ i-1 (m 1 ) = max{pot(r), r ∈ P i-1 }. Now starting from m 1 , repeat the following procedure:

• Step 1: Find two place r 1 , r 2 in P i-1 such that m(r 1 ) < pot(p, r 1 ) and m(r 2 ) > pot(p, r 2 ), m denoting the current marking. • Step 2: Use the induction hypothesis on (5.5) to find m′ ∈ R i-1 ( m) such that m′ (r 1 ) = m(r 1 ) + 1, m′ (r 2 ) = m(r 2 ) -1 and m′ (r) = m(r) for all r ∈ P i-1 \ {r 1 , r 2 }. All the intermediate markings are (i -1)-live. Since m(P i-1 ) ≥ pot(p), if there exists r 1 ∈ P i-2 such that m(r 1 ) < pot(p, r 1 ) then there exists r 2 ∈ P i-2 such that m(r 2 ) > pot(p, r 2 ) ≥ 0 as well. Because the interface places have maximal potential, at the beginning of each iteration, we always have ϕ i-1 ( m) = max{pot(r), r ∈ P i-1 }, hence pot(r 2 ) ≤ ϕ i-1 ( m) ≤ m(P i-2 ). Each iteration strictly diminishes the number of "missing" tokens in the places of P i-1 synchronised with p, so the procedure eventually stops at a marking m 2 such that m 2 (r) ≥ pot(p, r) for every place r ∈ P i-1 . This marking enables the output transitions of p. networks (which correspond to 1-level ordered nets) and is not included in the class of S-invariant reachable Petri nets.

Suppose that m 0 is a live marking. Suppose that the places of each level are ordered by increasing potential: P i = {p i1 , . . . , p ik i } such that ∀1 ≤ j < k i , pot(p ij ) ≤ pot(p i(j+1) ).

Let V denote the n × P -matrix the i-th row of which is the S-invariant v i defined in Corollary 5.7. For 1 ≤ i ≤ n, set C i = v i m 0 = m 0 (P i ). Then the reachability set consists of all n-live markings m such that V m = t (C 1 , . . . , C n ).

For 1 ≤ i ≤ n, 1 ≤ j ≤ k i and c 1 , . . . , c i ∈ Z, define E(i, j, c 1 , . . . , c i ) as the set of markings m such that      m(p iν ) = 0 for all ν > j V m = t (c 1 , . . . , c i , 0 . . . , 0) ϕ ν (m) ≤ m(P ν-1 ) for all 2 ≤ ν ≤ i .

The elements of E(i, j, c 1 , . . . , c i ) are the markings which satisfy the second part of the i-condition and the S-invariants constraints (c 1 , . . . , c i , 0, . . . , 0) and concentrate tokens in P 1 , . . . , P i-1 and {p i1 , . . . , p ij }.

With each E(i, j, c 1 , . . . , c i ) associate G(i, j, c 1 , . . . , c i ) = π(E(i, j, c 1 , . . . , c i )) = p∈P u m(p) p the sum being taken over all m ∈ E(i, j, c 1 , . . . , c i ).

We propose to compute G(n, k n , C 1 , . . . , C n ) by dynamic programming. It consists in breaking each G(i, j, c 1 , . . . , c i ) into smaller sums. This corresponds to a partition of the elements of E(i, j, c 1 , . . . , c i ) by the number of tokens in p ij . Proposition 5.15. Let be given E = E(i, j, c 1 , . . . , c i ). If c i < 0 then E = ∅. If c i ≥ 0 then for every non-negative integer a: Proof. Suppose that E = ∅. Let m be an element of E such that m(p ij ) = a. We have m(P i ) = c i , so a ≤ c i . Moreover, if m(p ij ) < m(P i ) then m must mark some place p iν with ν < j, so j ≥ 2. These prove the first and the second cases.

Complexity. Since i ≤ n, j ≤ K = max{k 1 , . . . , k n }, the number of evaluations is bounded by n×K ×γ, where γ upper bounds the c i 's. Let α denote the global maximal potential. From (5.1), we obtain γ = O(m 0 (P )K n α n ). So the complexity of a dynamic programming algorithm using Cor. 5.16 is O(m 0 (P )nK n+1 α n ), i.e. pseudo-polynomial for a fixed number of state machines.

Perspectives

This work has several perspectives. First, we are interested in extending and applying our rules for a modular modelling of complex product-form Petri nets. We also want to obtain characterisation of product-form Petri nets when stochastic Petri nets are equipped with infinite-server policy. Then we want to validate the formalism of Π 3 -nets showing that it allows to express standard patterns of distributed systems. We plan to implement analysis of Π 3 -nets and integrate it into a tool for stochastic Petri nets like Great-SPN [START_REF] Chiola | GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets[END_REF]. Finally we conjecture that reachability is EXPSPACE-complete for Π 2 -nets and we want to establish it.

Definition 2 . 2 (

 22 Firing rule). A transition t is enabled by the marking m if m ≥ • t (denoted by m t -→); an enabled transition t may fire which transforms the marking m into

Figure 1 :

 1 Figure 1: Petri net.

Figure 2 :

 2 Figure 2: Relations between deficiency (δ) and WR for some classes of Petri nets.

Figure 3 :

 3 Figure 3: How to synthetise a Π 2 -net.

  WR. The regulated Petri net A ⊙ N has deficiency 0. Proof. By construction the reaction graph of the regulated Petri net A ⊙ N is the reaction graph of N , i.e. A, modulo a node renaming. So A ⊙ N is WR iff N is WR. Now let us prove that the deficiency is 0. We use the characterization by witnesses, see Prop. 2.8. Let C be the set of complexes of A ⊙ N . Consider c ∈ C and let c be the corresponding element in C. Define wit(c) ∈ Q P ⊔C by: wit(c) c = 1, ∀u = c, wit(c) u = 0. By direct inspection, we check that wit(c) is indeed a witness of c.

2 2 2 Figure 4 :

 24 Figure 4: Regulated Petri net associated with the Petri net of Fig 1.

Theorem 4 . 1 .

 41 The reachability problem for safe Π 2 -nets is PSPACE-complete.

Figure 5 :

 5 Figure 5: A 3-bit counter (without the reverse transitions).

Definition 5 . 1 (

 51 Ordered Π-net). Consider an integer n ≥ 2. An n-level ordered Π-net is a Π-net N = (P, T, W -, W + ) such that: 1. P = 1≤i≤n P i , T = 1≤i≤n T i and

Figure 7 :Definition 5 . 4 (

 754 Figure 7: Ordered Π-net.

Lemma 5 . 5 .

 55 ∀p ∈ P n , m(p) = m(p) and ∀p ∈ P i , i < n , m(p) = m(p) -r∈Pi+1 m(r)pot(r, p) Let m, m ′ be two vectors such that m

1 .

 1 If a > c i then E ∩ {m|m(p ij ) = a} = ∅. 2. If a < c i and j = 1 then E ∩ {m|m(p ij ) = a} = ∅. 3. If a < c i and j ≥ 2 then E ∩ {m|m(p ij ) = a} = {m + ap ij | m ∈ E(i, j -1, c 1v 1 (ap ij ), . . . , c iv i (a p ij ))}. 4. If a = c i and i = 1 then E ∩ {m|m(p ij ) = a} = {c 1 p 1j }. 5. If a = c i and i > 1 then E∩{m|m(p ij ) = a} = { m+ap ij | m ∈ E(i-1, k i-1 , c 1 -v 1 (ap ij ), . . . , c i-1v i-1 (ap ij ))}.

Acknowledgements. We would like to thank the anonymous referees whose numerous and pertinent suggestions have been helpful in preparing the final version of the paper.

Definition 5.10 (Minimal marked potential). Consider i ∈ {2, . . . , n}. The level i minimal potential marked by m is:

The next lemma gives a necessary condition for reachability.

Lemma 5.11. If ϕ i (m) ≤ m(P i-1 ) then ϕ i (m ′ ) ≤ m ′ (P i-1 ) for all m ′ ∈ R(m).

Proof. W.l.o.g., assume that m t -→ m ′ . First, suppose that t / ∈ T i . If t / ∈ T i+1 then firing t does not modify the marking on P i , so ϕ i (m ′ ) = ϕ i (m). If t ∈ T i+1 , firing t either leaves the marking of P i unchanged or moves tokens between places of maximal potential in P i ; in both cases

∈ T i . Now consider t ∈ T i , let p and q be the input and output places of t in P i . We have ϕ i (m ′ ) ≤ pot(q) ≤ m(P i-1 )pot(p) + pot(q) = m ′ (P i-1 ).

We now define the partial liveness and partial reachability. Definition 5.12 (i-reachability set, i-liveness). Let m be a marking. The i-reachability set of m, denoted by R i (m), is the set of all markings reachable from m by a firing sequence consisting of transitions in 1≤j≤i T j . We say that m is i-live if for any transitions t in 1≤j≤i T j , there exists a marking in R i (m) which enables t. By convention, R 0 (m) = {m} and every marking is 0-live.

The i-live markings are characterised by the following proposition. Proposition 5.13. A marking m is i-live if and only if it satisfies the following inequalities, called the i-condition:

If m satisfies the i-condition then for every p, q ∈ P i such that p = q, m(p) > 0 and pot(p) ≤ m(P i-1 ), there exists m ′ ∈ R i (m) such that:

A marking is live if and only if it satisfies the n-condition.

Proof. Consider an i-live marking m. For any j ≤ i, there is a marking m ′ ∈ R i (m) which enables a transition of T j . This marking satisfies ϕ j (m ′ ) ≤ m ′ (P j-1 ). By (weak) reversibility, m ∈ R(m ′ ), so ϕ j (m) ≤ m(P j-1 ) (Lemma 5.11). Since the number of tokens in P i is the same for all

Example: The ordered Π-net in Figure 7 is a Π 3 -net. Consider two markings: m 1 = p 3 + q 3 + r 3 + 4p 1 and m 2 = 3q 3 + 4p 1 . These markings agree on all the S-invariants, but only m 1 satisfies the 3-condition. It is easy to check that m 1 is live while m 2 is dead. We conclude this subsection by showing that the reachability problem for Π 3 -nets can be efficiently decided as well.

Theorem 5.14. Suppose that the initial marking m 0 is live. Then the reachability set R(m 0 ) coincides with the set S(m 0 ) of markings which satisfy the n-condition and agree with m 0 on the S-invariants given by Corollary 5.7.

Proof. The inclusion R(m 0 ) ⊂ S(m 0 ) is the combination of the results of Corollary 5.7 and Proposition 5.13. To prove the converse, we look for a marking which is reachable from every marking of S(m 0 ). Let p j , 1 ≤ j ≤ n, be a place of maximal potential of P j , that is, pot(p j ) = max{pot(p), p ∈ P j }. Let m ′ 0 denote the unique marking in S(m 0 ) such that m ′ 0 (p) = 0 for every p / ∈ {p 1 , . . . , p n }. Consider an arbitrary marking m in S(m 0 ). We prove by a reverse induction on i ≤ n and by using the second part of Proposition 5.13 that there exists a marking m ′ ∈ R(m) such that m ′ (p) = 0 ∀p / ∈ {p 1 , . . . , p n }. The inductive claim is: There exists a marking m ′ i ∈ R(m) such that ∀p ∈ ∪ i≤j≤n P j \ {p i , . . . , p n } m ′ i (p) = 0 and m ′ i satisfies the i -1 condition. Let us address the basis case i = n. Assume that there exists p = p n such that m 0 (p) > 0. Using proposition 5.13, we move a token from p to p n . Furthermore by lemma 5.11, the n-condition is still satisfied. Iterating this process, we obtain a marking m ′ n such that ∀p ∈ P n \ {p n } m ′ n (p) = 0 and the n-condition is still satisfied. The inductive case is similar by observing that the sequence that moves the tokens of P i does not use transitions of T j for j > i. Since m ′ is also an element of S(m 0 ), m ′ = m ′ 0 . So m ′ 0 is reachable from every marking in S(m 0 ). By (weak) reversibility, every marking in S(m 0 ) is reachable from

Computing the normalising constant

The normalising constant of a product-form Petri net (see Section 2.1) is

. It is in general a difficult task to compute G, as can be guessed from the complexity of the reachability problem. However, efficient algorithms may exist for nets with a well-structured reachability set. Such algorithms were known for Jackson networks [START_REF] Reiser | Mean Value Analysis of Closed Multichain Queueing Networks[END_REF] and the S-invariant reachable Petri nets defined in [START_REF] Coleman | Product form equilibrium distributions and a convolution algorithm for stochastic Petri nets[END_REF]. We show that is is also the case for the class of live Π 3 -nets which is strictly larger than the class of Jackson

The fourth case is trivial.

Let us address the third case, we have to show that:

The values c 1v 1 (ap ij ), . . . , c iv i (ap ij ) are obtained by:

Since m and (map ij ) only differ at p ij , it suffices to show that ϕ i (map ij ) ≤ (map ij )(P i-1 ). Indeed, ϕ i (map ij ) = ϕ i (m) because both markings mark some p iν with ν < j, and (map ij )(P i-1 ) = m(P i-1 ) because the two markings are identical on P

The fifth case is similar. It suffices to show that ϕ i-1 (map ij ) ≤ (map ij )(P i-2 ) and ϕ i (m ′ + ap ij ) ≤ (m ′ + ap ij )(P i-1 ). The first inequality is immediate since (map ij ) is the restriction of m on 1≤ν≤i-1 P ν . To prove the second one, note that (m ′ +ap ij )(P i-1 ) = m ′ (P i-1 ) = c i-1 -v i-1 (ap ij ) = m(P i-1 ) and ϕ i (m ′ + ap ij ) = ϕ i (m).

The proposition 5.15 induces the following relations between the sums G(i, j, c 1 , . . . , c i ).

Corollary 5.16. If c i < 0 then G(i, j, c 1 , . . . , c i ) = 0. If c i ≥ 0 then:

• Case 2 ≤ i ≤ n, j = 1:

G(i, 1, c 1 , . . . , c i ) = u ci pi1 G(i -1, k i-1 , c 1v 1 (c i p i1 ), . . . , c i-1v i-1 (c i p i1 )) .

• Case i = 1, j ≥ 2: G(1, j, c 1 ) = c1-1 ν=0 u ν p1j G(1, j -1, c 1ν) + u c1 p1j .

• Case i = 1, j = 1: G(1, 1, c 1 ) = u c1 p11 .