iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/S10703-006-0022-1
Verification of bounded Petri nets using integer programming | Formal Methods in System Design Skip to main content
Springer Nature Link
Log in

Verification of bounded Petri nets using integer programming

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings—themselves a class of acyclic Petri nets—which contain enough information, albeit implicit, to reason about the reachable markings of the original Petri nets. In [19], a verification technique for net unfoldings was proposed, in which deadlock detection was reduced to a mixed integer linear programming problem. In this paper, we present a further development of this approach. The essence of the proposed modifications is to transfer the information about causality and conflicts between the events involved in an unfolding, into a relationship between the corresponding integer variables in the system of linear constraints. Moreover, we present some problem-specific optimisation rules, reducing the search space. To solve other verification problems, such as mutual exclusion or marking reachability and coverability, we adopt Contejean and Devie's algorithm for solving systems of linear constraints over the natural numbers domain and refine it, by taking advantage of the specific properties of systems of linear constraints to be solved.

Another contribution of this paper is a method of re-formulating some problems specified in terms of Petri nets as problems defined for their unfoldings. Using this method, we obtain a memory efficient translation of a deadlock detection problem for a safe Petri net into an LP problem. We also propose an on-the-fly deadlock detection method.

Experimental results demonstrate that the resulting algorithms can achieve significant speedups.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8

Similar content being viewed by others

Notes

  1. We will often identify Unf Σ and Pref Σ, provided that this does not create an ambiguity.

  2. Including the virtual node 0.

  3. The ordering \(\prec_x\) may be defined in other ways as well [4].

  4. From the point of view of this paper, such an assumption is unproblematic. The case 0 ∈ D is discussed in Remark 1, at the end of this section.

  5. Later we will take ξ to be the \(\mathit{MCC}\) function to apply the developed technique to unfolding-based model checking.

  6. E.g., G ξ could be searched in the breadth-first or depth-first manner.

  7. Using, e.g., depth-first search as the breadth-first search would be inefficient due to the need to record frozen components.

  8. x i is fixed if it is equal to the highest value in D i , or if ε i has been frozen.

  9. Intuitively, opt(x) is undefined if, during the application of the optimisation rules, the algorithm finds out that the system has no ξ-minimal solution y≥x.

  10. Though in Section 8.3 we consider other model checking problems, some of the existing tools we use for comparison support only deadlock checking; moreover, the system of constraints for the other described problems tend to be smaller and easier to solve than those for deadlock detection.

References

  1. Ajili F, Contejean E (1997) Avoiding slack variables in the solving of linear diophantine equations and inequations. Theor Comput Sci 173:183–208

    Google Scholar 

  2. Best E, Grahlmann B (1996) PEP —More than a Petri net tool. In: Proc TACAS'96, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1055, pp 397–401

  3. Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press

  4. Contejean E, Devie H (1994) An efficient incremental algorithm for solving systems of linear diophantine equations. Inf Comput 113:143–172

    Google Scholar 

  5. Corbett JC (1996) Evaluating deadlock detection methods for concurrent software. IEEE Trans Soft Eng SE-22(3):161–180

    Google Scholar 

  6. CPLEX Corporation (1995) CPLEX 3.0 Manual

  7. Engelfriet J (1991) Branching processes of Petri nets. Acta Inform 28:575–591

    Google Scholar 

  8. Esparza J, Römer S, Vogler W (2002) An improvement of McMillan's unfolding algorithm. Form Method Syst Des 20(3):285–310

    Google Scholar 

  9. Esparza J (1994) Model checking based on branching processes. Sci Comput Program 23:151–195

    Google Scholar 

  10. Heljanko K (1999) Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets. IOS Press, Fundamenta Inform 37(3):247–268

  11. Khomenko V (2003) Model checking based on prefixes of Petri net unfoldings. PhD Thesis, School of Computing Science, University of Newcastle

  12. Khomenko V, Koutny M (2000) Deadlock checking using liner programming and partial order dependencies. Technical Report CS-TR-695, School of Computing Science, University of Newcastle

  13. Khomenko V, Koutny M (2000) Verification of bounded Petri Nets using integer programming. Technical Report CS-TR-711, School of Computing Science, University of Newcastle

  14. Koutny M, Best E (1999) Fundamental study: operational and denotational semantics for the box algebra. Theor Comput Sci 211:1–83

    Google Scholar 

  15. Krivoi S (1999) About some methods of solving and feasibility criteria of linear diophantine equations over the natural numbers domain (in Russian). Cybern Syst Anal 4:12–36

    Google Scholar 

  16. McMillan KL (1992) Using unfoldings to avoid state explosion problem in the verification of asynchronous circuits. In: Proc CAV'92, Lecture Notes in Computer Science, Springer-Verlag, Vol 663, pp 164–174

  17. McMillan KL (1992) Symbolic model checking: an approach to the state explosion problem. PhD Thesis, School of Computer Science, Carnegie Mellon University

  18. Melzer S (1998) Verifikation verteilter systeme mit linearer—und constraint-programmierung. PhD Thesis. Technische Universität München

  19. Melzer S, Römer S (1997) Deadlock checking using net unfoldings. In: Proc CAV'97, Lecture Notes in Computer Science, Springer-Verlag, vol 1254, pp 352–363

  20. Murata T (1989) Petri nets: properties, analysis and applications. In: Proc IEEE vol. 77 no. 4, pp. 541–580

  21. Niemelä I, Simons P (1997) smodels —An implementation of the stable model and well-founded semantics for normal logic programs. In: Proc LPNMR'97, Lecture Notes in Artificial Intelligence, Springer-Verlag, vol 1265, pp 420–429

  22. Silva M, Teruel E, Colom J-M (1998) Linear algebraic and linear programming techniques for the analysis of place/transition net systems. In: Reisig W, Rozenberg G (eds) Lectures on Petri nets I: basic models. Springer-Verlag, pp 309–373

  23. Simons P (1999) Extending the stable model semantics with more expressive rules. In: Proc LPNMR'99, Lecture Notes in artificial intelligence, Springer-Verlag vol 1730.

Download references

Acknowledgments

We would like to thank Paul Watson for comments on an earlier version of this paper, Alexander Letichevsky and Sergei Krivoi for drawing our attention to CDA and discussions on the theory of Diophantine equations, Christian Stehno for help with using the PEP tool, and Stephan Melzer for sending his PhD thesis. In particular, we would like to thank Keijo Heljanko for explaining the SM algorithm, providing the mcsmodels deadlock checking tool and some of the unfoldings used in the experiments, and extensive discussions about net unfoldings.

This research was supported by the ORS Awards Scheme grant ORS/C20/4, the Epsrc grant GR/M99293, the Royal Academy of Engineering/Epsrc post-doctoral research fellowship EP/C53400X/1 (Davac) and the EC IST grant 511599 (Rodin).

Author information

Authors and Affiliations

  1. School of Computing Science, University of Newcastle, Newcastle upon Tyne, NE1 7RU, UK

    Victor Khomenko & Maciej Koutny

Authors
  1. Victor Khomenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maciej Koutny
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Victor Khomenko.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Khomenko, V., Koutny, M. Verification of bounded Petri nets using integer programming. Form Method Syst Des 30, 143–176 (2007). https://doi.org/10.1007/s10703-006-0022-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-006-0022-1

Keywords

Search

Navigation