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

Teren, Viktor  ; Cortadella, Jordi ; Villa, Tiziano

International Journal of Applied Mathematics and Computer Science, Tome 33 (2023) no. 1, pp. 133-149.

Résumé

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.

Détail

Keywords: transition system, Petri net, state machine, theory of regions, SAT, pseudo Boolean optimization
Mots-clés : układ przejściowy, sieć Petriego, maszyna stanów, teoria regionów, SAT

Bibliographie

[1] [1] Badouel, E., Bernardinello, L. and Darondeau, P. (2015). Petri Net Synthesis, Springer, Berlin.

[2] [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] [3] Boros, E. and Hammer, P.L. (2002). Pseudo-Boolean optimization, Discrete Applied Mathematics 123(1-3): 155-225.

[4] [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] [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] [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] [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] [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] [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] [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] [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] [12] Desel, J. (1995). Free Choice Petri Nets, Cambridge University Press, Cambridge.

[13] [13] Ehrenfeucht, A. and Rozenberg, G. (1990). Partial (set) 2-structures, Acta Informatica 27(4): 343-368.

[14] [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] [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] [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] [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] [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] [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] [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] [21] Murata, T. (1989). Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77(4): 541-580.

[22] [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] [23] Schrijver, A. (1998). Theory of Linear and Integer Programming, Wiley, Amsterdam.

[24] [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] [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] [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] [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] [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] [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] [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.