A Symbolic Algorithm for the Synthesis of Bounded Petri Nets

  • J. Carmona
  • J. Cortadella
  • M. Kishinevsky
  • A. Kondratyev
  • L. Lavagno
  • A. Yakovlev
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)


This paper presents an algorithm for the synthesis of bounded Petri nets from transition systems. A bounded Petri net is always provided in case it exists. Otherwise, the events are split into several transitions to guarantee the synthesis of a Petri net with bisimilar behavior. The algorithm uses symbolic representations of multisets of states to efficiently generate all the minimal regions. The algorithm has been implemented in a tool. Experimental results show a significant net reduction when compared with approaches for the synthesis of safe Petri nets.


Boolean Function Transition System Symbolic Representation Concurrent System Minimal Region 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BBD95]
    Badouel, E., Bernardinello, L., Darondeau, P.: Polynomial algorithms for the synthesis of bounded nets. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 364–383. Springer, Heidelberg (1995)Google Scholar
  2. [BD98]
    Badouel, E., Darondeau, P.: Theory of regions. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models. LNCS, vol. 1491, pp. 529–586. Springer, Heidelberg (1998)Google Scholar
  3. [BDLS07]
    Bergenthum, R., Desel, J., Lorenz, R., Mauser, S.: Process mining based on regions of languages. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 375–383. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. [Bry86]
    Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computer-Aided Design 35(8), 677–691 (1986)zbMATHGoogle Scholar
  5. [Cai02]
    Caillaud, B.: Synet: A synthesizer of distributable bounded Petri-nets from finite automata (2002),
  6. [CGP00]
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)Google Scholar
  7. [CKLY98]
    Cortadella, J., Kishinevsky, M., Lavagno, L., Yakovlev, A.: Deriving Petri nets from finite transition systems. IEEE Transactions on Computers 47(8), 859–882 (1998)CrossRefMathSciNetGoogle Scholar
  8. [Dar07]
    Darondeau, P.: Synthesis and control of asynchronous and distributed systems. In: Basten, T., Juhás, G., Shukla, S.K. (eds.) ACSD. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  9. [DR96]
    Desel, J., Reisig, W.: The synthesis problem of Petri nets. Acta Informatica 33(4), 297–315 (1996)CrossRefMathSciNetGoogle Scholar
  10. [ER90]
    Ehrenfeucht, A., Rozenberg, G.: Partial (Set) 2-Structures. Part I, II. Acta Informatica 27, 315–368 (1990)zbMATHMathSciNetCrossRefGoogle Scholar
  11. [HKT95]
    Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: A trace semantics for petri nets. Inf. Comput. 117(1), 98–114 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  12. [HKT96]
    Hoogers, P.W., Kleijn, H.C.M., Thiagarajan, P.S.: An event structure semantics for general petri nets. Theor. Comput. Sci. 153(1&2), 129–170 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  13. [Maz87]
    Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)Google Scholar
  14. [Mil89]
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  15. [Muk92]
    Mukund, M.: Petri nets and step transition systems. Int. Journal of Foundations of Computer Science 3(4), 443–478 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  16. [SBY07]
    Sokolov, D., Bystrov, A., Yakovlev, A.: Direct mapping of low-latency asynchronous controllers from STGs. IEEE Transactions on Computer-Aided Design 26(6), 993–1009 (2007)CrossRefGoogle Scholar
  17. [VPWJ07]
    Verbeek, H.M.W., Pretorius, A.J., van der Aalst, W.M.P., van Wijk, J.J.: On Petri-net synthesis and attribute-based visualization. In: Proc. Workshop on Petri Nets and Software Engineering (PNSE 2007), pp. 127–141 (June 2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • J. Carmona
    • 1
  • J. Cortadella
    • 1
  • M. Kishinevsky
    • 2
  • A. Kondratyev
    • 3
  • L. Lavagno
    • 4
  • A. Yakovlev
    • 5
  1. 1.Universitat Politècnica de CatalunyaSpain
  2. 2.Intel CorporationUSA
  3. 3.Cadence Berkeley LaboratoriesUSA
  4. 4.Politecnico di TorinoItaly
  5. 5.Newcastle UniversityUK

Personalised recommendations