Generation of synchronizing state machines from a transition system: A region-based approach

• Autorzy: Teren Viktor , Cortadella Jordi , Villa Tiziano

Identyfikatory

DOI

10.34768/amcs-2023-0011

• Języki publikacji: EN

Abstrakty

EN

Transition systems (TSs) and Petri nets (PNs) are important models of computation ubiquitous in formal methods for modeling systems. A crucial problem is how to extract, from a given TS, a PN whose reachability graph is equivalent (with a suitable notion of equivalence) to the original TS. This paper addresses the decomposition of transition systems into synchronizing state machines (SMs), which are a class of Petri nets where each transition has one incoming and one outgoing arc. Furthermore, all reachable markings (non-negative vectors representing the number of tokens for each place) of an SM have only one marked place with only one token. This is a significant case of the general problem of extracting a PN from a TS. The decomposition is based on the theory of regions, and it is shown that a property of regions called excitation-closure is a sufficient condition to guarantee the equivalence between the original TS and a decomposition into SMs. An efficient algorithm is provided which solves the problem by reducing its critical steps to the maximal independent set problem (to compute a minimal set of irredundant SMs) or to satisfiability (to merge the SMs). We report experimental results that show a good trade-off between quality of results vs. computation time.

Słowa kluczowe

EN

transition system; Petri net; state machine; theory of regions; SAT; pseudo Boolean optimization

PL

układ przejściowy; sieć Petriego; maszyna stanów; teoria regionów; SAT

• Wydawca: Oficyna Wydawnicza Uniwersytetu Zielonogórskiego
• Czasopismo: International Journal of Applied Mathematics and Computer Science
• Rocznik: 2023
• Tom: Vol. 33, no. 1
• Strony: 133--149
• Opis fizyczny: Bibliogr. 30 poz., rys., tab.

Twórcy

autor

Teren Viktor

• Department of Computer Science, University of Verona, Strada le Grazie 15, 37134, Verona, Italy

autor

Cortadella Jordi

• Department of Computer Science, Polytechnic University of Catalonia, Jordi Girona Salgado 1-3, 08034, Barcelona, Spain

autor

Villa Tiziano

• Department of Computer Science, University of Verona, Strada le Grazie 15, 37134, Verona, Italy

Bibliografia

• [1] Badouel, E., Bernardinello, L. and Darondeau, P. (2015). Petri Net Synthesis, Springer, Berlin.
• [2] Benini, L., De Micheli, G. and Macii, E. (2001). Designing low-power circuits: Practical recipes, IEEE Circuits and Systems Magazine 1(1): 6-25.
• [3] Boros, E. and Hammer, P.L. (2002). Pseudo-Boolean optimization, Discrete Applied Mathematics 123(1-3): 155-225.
• [4] Carmona, J., Colom, J-M, Cortadella, J. and Garcìa-Vallés, F. (2006). Synthesis of asynchronous controllers using integer linear programming, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25(9): 1637-1651.
• [5] Carmona, J., Cortadella, J. and Kishinevsky, M. (2009a). Divide-and-conquer strategies for process mining, International Conference on Business Process Management, Ulm, Germany, pp. 327-343.
• [6] Carmona, J., Cortadella, J. and Kishinevsky, M. (2009b). Genet: A tool for the synthesis and mining of Petri nets, 9th International Conference on Application of Concurrency to System Design, Augsburg, Germany, pp. 181-185.
• [7] Carmona, J., Cortadella, J. and Kishinevsky, M. (2009c). New region-based algorithms for deriving bounded Petri nets, IEEE Transactions on Computers 59(3): 371-384.
• [8] Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L. and Yakovlev, A. (1997). Petrify: A tool for manipulating concurrent specifications and synthesis of asynchronous controllers, IEICE Transactions on Information and Systems 80(3): 315-325.
• [9] Cortadella, J., Kishinevsky, M., Lavagno, L. and Yakovlev, A. (1995). Synthesizing Petri nets from state-based models, Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), San Jose, USA, pp. 164-171.
• [10] Cortadella, J., Kishinevsky, M., Lavagno, L. and Yakovlev, A. (1998). Deriving Petri nets from finite transition systems, IEEE Transactions on Computers 47(8): 859-882.
• [11] de San Pedro, J. and Cortadella, J. (2016). Mining structured Petri nets for the visualization of process behavior, Proceedings of the 31st Annual ACM Symposium on Applied Computing, New York, USA, pp. 839-846.
• [12] Desel, J. (1995). Free Choice Petri Nets, Cambridge University Press, Cambridge.
• [13] Ehrenfeucht, A. and Rozenberg, G. (1990). Partial (set) 2-structures, Acta Informatica 27(4): 343-368.
• [14] Gansner, E., Koutsofios, E., North, S. and Vo, K.-P. (1993). A technique for drawing directed graphs, IEEE Transactions on Software Engineering 19(3): 214-230.
• [15] Hagberg, A., Swart, P. and S Chult, D. (2008). Exploring network structure, dynamics, and function using NetworkX, Proceedings of the 7th Python in Science Conference (SciPy2008), Pasadena, USA, pp. 11-15.
• [16] Kalenkova, A.A., Lomazova, I.A. and Van der Aalst, W.M. (2014). Process model discovery: A method based on transition system decomposition, International Conference on Applications and Theory of Petri Nets and Concurrency, Tunis, Tunisia, pp. 71-90.
• [17] Kemper, P. and Bause, F. (1992). An efficient polynomial-time algorithm to decide liveness and boundedness of free-choice nets, in K. Jensen (Ed.), Application and Theory of Petri Nets, Springer, Berlin/Heidelberg, pp. 263-278.
• [18] Khomenko, V., Koutny, M. and Yakovlev, A. (2004). Detecting state encoding conflicts in STG unfoldings using SAT, Fundamenta Informaticae 62(2): 221-241.
• [19] Mattheakis, P.M. (2013). Logic Synthesis of Concurrent Controller Specifications, PhD thesis, University of Crete, Rethymnon, https://thesis.ekt.gr/thesisBo okReader/id/29912#page/1/mode/2up.
• [20] Mokhov, A., Cortadella, J. and de Gennaro, A. (2017). Process windows, 17th International Conference on Application of Concurrency to System Design (ACSD), Zaragoza, Spain, pp. 86-95.
• [21] Murata, T. (1989). Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77(4): 541-580.
• [22] Philipp, T. and Steinke, P. (2015). PBLib-A library for encoding pseudo-Boolean constraints into CNF, in M. Heule and S. Weaver (Eds), Theory and Applications of Satisfiability Testing, SAT 2015, Lecture Notes in Computer Science, Vol. 9340, Springer, Cham, pp. 9-16.
• [23] Schrijver, A. (1998). Theory of Linear and Integer Programming, Wiley, Amsterdam.
• [24] Taibi, D. and Systä, K. (2019). From monolithic systems to microservices: A decomposition framework based on process mining, Proceedings of the 9th International Conference on Cloud Computing and Services Science-CLOSER, Heraklion, Greece, pp. 153-164, DOI: 10.5220/0007755901530164.
• [25] Teren, V., Cortadella, J. and Villa, T. (2021). Decomposition of transition systems into sets of synchronizing state machines, 2021 24th Euromicro Conference on Digital System Design (DSD), Palermo, Italy, pp. 77-81, DOI: 10.1109/DSD53832.2021.00021.
• [26] Van der Aalst, W.M. (2012). Decomposing process mining problems using passages, International Conference on Application and Theory of Petri Nets and Concurrency, Hamburg, Germany, pp. 72-91.
• [27] Van der Aalst, W.M. (2013). Decomposing Petri nets for process mining: A generic approach, Distributed and Parallel Databases 31(4): 471-507.
• [28] Van der Aalst, W.M., Rubin, V., Verbeek, H., van Dongen, B.F., Kindler, E. and Günther, C.W. (2010). Process mining: A two-step approach to balance between underfitting and overfitting, Software & Systems Modeling 9(1): 87.
• [29] Verbeek, H. and Van der Aalst, W.M. (2014). Decomposed process mining: The ILP case, International Conference on Business Process Management, Eindhoven, The Netherlands, pp. 264-276.
• [30] Wojnakowski, M., Wiśniewski, R., Bazydło, G. and Popławski, M. (2021). Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems, International Journal of Applied Mathematics and Computer Science 31(4): 647-657, DOI: 10.34768/amcs-2021-0045.

Uwagi

PL

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023)