{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:51Z","timestamp":1740122691559,"version":"3.37.3"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T00:00:00Z","timestamp":1726099200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T00:00:00Z","timestamp":1726099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100011688","name":"Electronic Components and Systems for European Leadership","doi-asserted-by":"publisher","award":["826452","826452"],"award-info":[{"award-number":["826452","826452"]}],"id":[{"id":"10.13039\/501100011688","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100016238","name":"Ministerie van Economische Zaken en Klimaat","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100016238","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100013405","name":"Rijksdienst voor Ondernemend Nederland","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100013405","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Supervisor synthesis is a means to algorithmically derive a supervisory controller from a discrete-event model of a system and a requirements specification. For large systems, synthesis suffers from state space explosion. To mitigate this, synthesis can be applied to a symbolic representation of the models by using Binary Decision Diagrams (BDDs). Peak used BDD nodes and BDD operation count are introduced as deterministic and platform independent metrics to express the computational effort of a symbolic synthesis. These BDD-based metrics are useful to analyze the efficiency of the synthesis algorithm. From this analysis, modifications can be made to how BDDs are handled during synthesis, improving synthesis efficiency. We demonstrate this approach by introducing and analyzing: DCSH, a variable ordering heuristic; several edge ordering heuristics; and an approach to efficiently enforce state exclusion requirements in synthesis. These methods were recently implemented in our open source supervisory control tool: Eclipse ESCET. The analysis is based on large scale experiments of performing synthesis on a variety of models from literature. We show that: (1) by using DCSH, synthesis with high computational effort can be avoided, and generally low computational effort is required, relative to the variable ordering heuristics that were used prior to this work; (2) applying reverse-model edge order realizes relatively low synthesis effort; and (3) state exclusion requirements can efficiently be enforced by restricting edge guards prior to synthesis. While these methods reduce computational effort in practice, it should be noted that they do not affect the theoretical (worst-case) complexity of synthesis.<\/jats:p>","DOI":"10.1007\/s10626-024-00403-4","type":"journal-article","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T08:20:41Z","timestamp":1726129241000},"page":"689-732","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reducing the computational effort of symbolic supervisor synthesis"],"prefix":"10.1007","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1628-8622","authenticated-orcid":false,"given":"Sander","family":"Thuijsman","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9886-7918","authenticated-orcid":false,"given":"Dennis","family":"Hendriks","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9283-4074","authenticated-orcid":false,"given":"Michel","family":"Reniers","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,12]]},"reference":[{"issue":"6","key":"403_CR1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/tc.1978.1675141","volume":"27","author":"SB Akers","year":"1978","unstructured":"Akers SB (1978) Binary decision diagrams. Trans Comp 27(6):509\u2013516. https:\/\/doi.org\/10.1109\/tc.1978.1675141","journal-title":"Binary decision diagrams. Trans Comp"},{"key":"403_CR2","doi-asserted-by":"publisher","unstructured":"Aloul FA, Markov IL, Sakallah KA (2003) FORCE: a fast and easy-to-implement variable-ordering heuristic. In: Proceedings of the 13th ACM Great Lakes Symposium on VLSI. ACM Press, pp 116\u201311. https:\/\/doi.org\/10.1145\/764808.764839","DOI":"10.1145\/764808.764839"},{"key":"403_CR3","doi-asserted-by":"publisher","unstructured":"Aziz A, Ta\u015firan S, Brayton RK (1994) BDD variable ordering for interacting finite state machines. In: Proceedings of the 31st annual conference on design automation. ACM Press, pp 283\u2013288. https:\/\/doi.org\/10.1145\/196244.196379","DOI":"10.1145\/196244.196379"},{"issue":"1","key":"403_CR4","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/tem.2015.2491283","volume":"63","author":"T Browning","year":"2016","unstructured":"Browning T (2016) Design structure matrix extensions and innovations: a survey and new opportunities. Trans Eng Manage 63(1):27\u201352. https:\/\/doi.org\/10.1109\/tem.2015.2491283","journal-title":"Trans Eng Manage"},{"issue":"3","key":"403_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293\u201331. https:\/\/doi.org\/10.1145\/136035.136043","journal-title":"ACM Comput Surv"},{"issue":"4","key":"403_CR6","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"JR Burch","year":"1994","unstructured":"Burch JR, Clarke EM, Long DE et al (1994) Symbolic model checking for sequential circuit verification. Trans Comp-Aided Design of Integ Circ Syst 13(4):401\u201342. https:\/\/doi.org\/10.1109\/43.275352","journal-title":"Trans Comp-Aided Design of Integ Circ Syst"},{"issue":"5","key":"403_CR7","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1109\/43.759068","volume":"18","author":"G Cabodi","year":"1999","unstructured":"Cabodi G, Camurati PE, Quer S (1999) Improving the efficiency of BDD-based operators by means of partitioning. Trans Comp-Aided Design of Integ Circ Syst 18(5):545\u201355. https:\/\/doi.org\/10.1109\/43.759068","journal-title":"Trans Comp-Aided Design of Integ Circ Syst"},{"key":"403_CR8","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10626-014-0194-6","volume":"25","author":"K Cai","year":"2014","unstructured":"Cai K, Wonham W (2014) New results on supervisor localization, with case studies. Disc Event Dyna Syst 25:203\u2013226. https:\/\/doi.org\/10.1007\/s10626-014-0194-6","journal-title":"Disc Event Dyna Syst"},{"key":"403_CR9","doi-asserted-by":"publisher","unstructured":"Cassandras CG, Lafortune S (2021) Introduction to Discrete Event Systems, 3rd edn. Springer Nature Switzerland https:\/\/doi.org\/10.1007\/978-3-030-72274-6","DOI":"10.1007\/978-3-030-72274-6"},{"key":"403_CR10","doi-asserted-by":"publisher","unstructured":"\u010cengi\u0107 G, \u00c5kesson K (2008) A control software development method using IEC 61499 function blocks, simulation and formal verification. In: Proceedings of the 20th IFAC World congress. Elsevier BV, pp 22\u201327. https:\/\/doi.org\/10.3182\/20080706-5-kr-1001.00003","DOI":"10.3182\/20080706-5-kr-1001.00003"},{"key":"403_CR11","doi-asserted-by":"publisher","unstructured":"Chaki S, Gurfinkel A (2018) BDD-based symbolic model checking. In: Handbook of model checking. Springer International Publishing, p 219\u2013245. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_8","DOI":"10.1007\/978-3-319-10575-8_8"},{"key":"403_CR12","doi-asserted-by":"publisher","unstructured":"Ciardo G, Siminiceanu R (2002) Using edge-valued decision diagrams for symbolic generation of shortest paths. In: Formal methods in computer-aided design. Springer Berlin Heidelberg, pp 256\u2013273. https:\/\/doi.org\/10.1007\/3-540-36126-x_16","DOI":"10.1007\/3-540-36126-x_16"},{"key":"403_CR13","doi-asserted-by":"publisher","unstructured":"Cuthill EH, McKee J (1969) Reducing the bandwidth of sparse symmetric matrices. In: Proceedings of the 1969 24th national conference. ACM Press, pp 157\u2013172. https:\/\/doi.org\/10.1145\/800195.805928","DOI":"10.1145\/800195.805928"},{"key":"403_CR14","doi-asserted-by":"publisher","unstructured":"Fei Z, Miremadi S, \u00c5kesson K et\u00a0al (2013) Symbolic state-space exploration and guard generation in supervisory control theory. In: Communications in computer and information science, vol 271. Springer Berlin Heidelberg, pp 161\u2013175. https:\/\/doi.org\/10.1007\/978-3-642-29966-7_11","DOI":"10.1007\/978-3-642-29966-7_11"},{"key":"403_CR15","doi-asserted-by":"publisher","unstructured":"Fei Z, Miremadi S, \u00c5kesson K et al (2014) Efficient symbolic supervisor synthesis for extended finite automata. Trans Contr Syst Tech 22(6):2368\u20132375. https:\/\/doi.org\/10.1109\/tcst.2014.2303134","DOI":"10.1109\/tcst.2014.2303134"},{"issue":"11\u201312","key":"403_CR16","doi-asserted-by":"publisher","first-page":"1152","DOI":"10.1007\/s00170-008-1555-9","volume":"41","author":"L Feng","year":"2008","unstructured":"Feng L, Cai K, Wonham W (2008) A structural approach to the non-blocking supervisory control of discrete-event systems. The Int J Adv Manu Tech 41(11\u201312):1152\u20131168. https:\/\/doi.org\/10.1007\/s00170-008-1555-9","journal-title":"The Int J Adv Manu Tech"},{"key":"403_CR17","doi-asserted-by":"publisher","unstructured":"Flordal H, Malik R, Fabian M et al (2007) Compositional synthesis of maximally permissive supervisors using supervision equivalence. Disc Event Dyna Syst 17(4):475\u2013504. https:\/\/doi.org\/10.1007\/s10626-007-0018-z","DOI":"10.1007\/s10626-007-0018-z"},{"key":"403_CR18","doi-asserted-by":"publisher","unstructured":"Fokkink WJ, Goorden MA, Hendriks D et\u00a0al (2023) Eclipse ESCET\u2122: the eclipse supervisory control engineering toolkit. In: Tools and algorithms for the construction and analysis of systems. Springer, p 44\u201352. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_6","DOI":"10.1007\/978-3-031-30820-8_6"},{"key":"403_CR19","doi-asserted-by":"publisher","unstructured":"Forschelen STJ, van de Mortel-Fronczak JM, Su R et al (2012) Application of supervisory control theory to theme park vehicles. Discr Event Dyna Syst 22(4):511\u2013540. https:\/\/doi.org\/10.1007\/s10626-012-0130-6","DOI":"10.1007\/s10626-012-0130-6"},{"issue":"4","key":"403_CR20","doi-asserted-by":"publisher","first-page":"1625","DOI":"10.1109\/tac.2019.2928119","volume":"65","author":"MA Goorden","year":"2020","unstructured":"Goorden MA, van de Mortel-Fronczak J, Reniers MA et al (2020) Structuring multilevel discrete-event systems with dependence structure matrices. Trans Auto Contr 65(4):1625\u20131639. https:\/\/doi.org\/10.1109\/tac.2019.2928119","journal-title":"Trans Auto Contr"},{"key":"403_CR21","doi-asserted-by":"publisher","unstructured":"Knuth DE (1976) Big omicron and big omega and big theta. ACM SIGACT News 8(2):18\u201324. https:\/\/doi.org\/10.1145\/1008328.1008329","DOI":"10.1145\/1008328.1008329"},{"key":"403_CR22","doi-asserted-by":"publisher","unstructured":"Korssen T, Dolk V, van de Mortel-Fronczak JM et al (2018) Systematic model-based design and implementation of supervisors for advanced driver assistance systems. Trans Intel Trans Syst 19(2):533\u2013544. https:\/\/doi.org\/10.1109\/tits.2017.2776354","DOI":"10.1109\/tits.2017.2776354"},{"issue":"4","key":"403_CR23","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"CY Lee","year":"1959","unstructured":"Lee CY (1959) Representation of switching circuits by binary-decision programs. The Bell Syst Tech J 38(4):985\u2013999. https:\/\/doi.org\/10.1002\/j.1538-7305.1959.tb01585.x","journal-title":"The Bell Syst Tech J"},{"key":"403_CR24","doi-asserted-by":"publisher","unstructured":"Loose R, van\u00a0der Sanden BJ, Reniers MA et\u00a0al (2018) Component-wise supervisory controller synthesis in a client\/server architecture. In: Proceedings of the 14th IFAC workshop on discrete event systems. Elsevier BV, pp 381\u2013387. https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.329","DOI":"10.1016\/j.ifacol.2018.06.329"},{"key":"403_CR25","doi-asserted-by":"publisher","unstructured":"Lopes YK, Trenkwalder SM, Leal AB et al (2016) Supervisory control theory applied to swarm robotics. Swarm Intell 10(1):65\u201397. https:\/\/doi.org\/10.1007\/s11721-016-0119-0","DOI":"10.1007\/s11721-016-0119-0"},{"key":"403_CR26","doi-asserted-by":"publisher","unstructured":"Lousberg SAJ, Thuijsman SB, Reniers MA (2020) DSM-based variable ordering heuristic for reduced computational effort of symbolic supervisor synthesis. In: Proceedings of the 15th IFAC workshop on discrete event systems. Elsevier BV, pp 429\u2013436. https:\/\/doi.org\/10.1016\/j.ifacol.2021.04.058","DOI":"10.1016\/j.ifacol.2021.04.058"},{"issue":"5","key":"403_CR27","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/tac.2006.875030","volume":"51","author":"C Ma","year":"2006","unstructured":"Ma C, Wonham W (2006) Nonblocking supervisory control of state tree structures. Transactions on Automatic Control 51(5):782\u2013793. https:\/\/doi.org\/10.1109\/tac.2006.875030","journal-title":"Transactions on Automatic Control"},{"key":"403_CR28","doi-asserted-by":"publisher","unstructured":"Ma C, Wonham W (2008) STSLib and its application to two benchmarks. In: Proceedings of the 9th international workshop on discrete event systems. IEEE, pp 119\u2013124. https:\/\/doi.org\/10.1109\/wodes.2008.4605932","DOI":"10.1109\/wodes.2008.4605932"},{"key":"403_CR29","doi-asserted-by":"publisher","unstructured":"Malik R, \u00c5kesson K, Flordal H et\u00a0al (2017) Supremica\u2013an efficient tool for large-scale discrete event systems. In: Proceedings of the 20th IFAC world congress. Elsevier BV, pp 5794\u20135799. https:\/\/doi.org\/10.1016\/j.ifacol.2017.08.427","DOI":"10.1016\/j.ifacol.2017.08.427"},{"key":"403_CR30","doi-asserted-by":"publisher","unstructured":"Markovski J, van Beek DA, Theunissen RJM et\u00a0al (2010) A state-based framework for supervisory control synthesis and verification. In: Proceedings of the 49th IEEE conference on decision and control. IEEE, pp 3481\u20133486. https:\/\/doi.org\/10.1109\/cdc.2010.5717095","DOI":"10.1109\/cdc.2010.5717095"},{"key":"403_CR31","doi-asserted-by":"publisher","unstructured":"Meijer J, van\u00a0de Pol JC (2016) Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: Proceedings of the 8th NASA formal methods symposium. Springer International Publishing, p 255\u2013271. https:\/\/doi.org\/10.1007\/978-3-319-40648-0_20","DOI":"10.1007\/978-3-319-40648-0_20"},{"key":"403_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58940-9","author":"C Meinel","year":"1998","unstructured":"Meinel C, Theobald T (1998) Algorithms and Data Structures in VLSI Design. Springer, Berlin Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-58940-9","journal-title":"Springer, Berlin Heidelberg"},{"key":"403_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-1303-8","author":"S Minato","year":"1996","unstructured":"Minato S (1996) Binary Decision Diagrams and Applications for VLSI CAD. Springer, US. https:\/\/doi.org\/10.1007\/978-1-4613-1303-8","journal-title":"Springer, US"},{"issue":"2","key":"403_CR34","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s100090100038","volume":"3","author":"S Minato","year":"2001","unstructured":"Minato S (2001) Zero-suppressed BDDs and their applications. Int J Softw Tools Technol Transfer 3(2):156\u2013170. https:\/\/doi.org\/10.1007\/s100090100038","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"6","key":"403_CR35","doi-asserted-by":"publisher","first-page":"1421","DOI":"10.1109\/tcst.2011.2167150","volume":"20","author":"S Miremadi","year":"2012","unstructured":"Miremadi S, Lennartson B, \u00c5kesson K (2012) A BDD-based approach for modeling plant and supervisor by extended finite automata. Trans Control Syst Technol 20(6):1421\u20131435. https:\/\/doi.org\/10.1109\/tcst.2011.2167150","journal-title":"Trans Control Syst Technol"},{"key":"403_CR36","doi-asserted-by":"publisher","unstructured":"Miremadi S, Lennartson B (2016) Symbolic on-the-fly synthesis in supervisory control theory. Trans Control Syst Technol 24(5):1705\u20131716. https:\/\/doi.org\/10.1109\/tcst.2015.2508978","DOI":"10.1109\/tcst.2015.2508978"},{"key":"403_CR37","unstructured":"Montgomery DC, Runger GC (2018) Applied Statistics and Probability for Engineers, 7th edn. John Wiley & Sons, Inc., https:\/\/www.wiley.com\/en-us\/Applied+Statistics+and+Probability+for+Engineers%2C+7th+Edition-p-9781119400363"},{"key":"403_CR38","doi-asserted-by":"publisher","first-page":"74","DOI":"10.4204\/eptcs.64.6","volume":"64","author":"D Nadales Agut","year":"2011","unstructured":"Nadales Agut D, Reniers M (2011) Linearization of CIF through SOS. Electron Proceed Theoretical Comp Sci 64:74\u201388. https:\/\/doi.org\/10.4204\/eptcs.64.6","journal-title":"Electron Proceed Theoretical Comp Sci"},{"issue":"3","key":"403_CR39","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1109\/tase.2011.2124457","volume":"8","author":"L Ouedraogo","year":"2011","unstructured":"Ouedraogo L, Kumar R, Malik R et al (2011) Nonblocking and safe control of discrete-event systems modeled as extended finite automata. Trans Automat Sci Eng 8(3):560\u2013569. https:\/\/doi.org\/10.1109\/tase.2011.2124457","journal-title":"Trans Automat Sci Eng"},{"key":"403_CR40","doi-asserted-by":"publisher","unstructured":"Panda S, Somenzi F, Plessier BF (1994) Symmetry detection and dynamic variable ordering of decision diagrams. In: Proceedings of the 1994 IEEE\/ACM international conference on computer-aided design. IEEE, p 628\u2013631. https:\/\/doi.org\/10.5555\/191326.191598","DOI":"10.5555\/191326.191598"},{"issue":"1","key":"403_CR41","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"PJ Ramadge","year":"1987","unstructured":"Ramadge PJ, Wonham W (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25(1):206\u2013230. https:\/\/doi.org\/10.1137\/0325013","journal-title":"SIAM J Control Optim"},{"key":"403_CR42","doi-asserted-by":"publisher","unstructured":"Ramadge PJ, Wonham W (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398. https:\/\/doi.org\/10.1109\/5.21072","DOI":"10.1109\/5.21072"},{"key":"403_CR43","unstructured":"Ranjan RK, Aziz A, Brayton RK et\u00a0al (1995) Efficient BDD algorithms for FSM synthesis and verification. In: International workshop on logic and synthesis, https:\/\/is.ifmo.ru\/research\/_efficient_bdd_algorithms_for_fsm_synthesis_and_verification.pdf"},{"key":"403_CR44","doi-asserted-by":"publisher","unstructured":"Reijnen FFH, Goorden MA, van\u00a0de Mortel-Fronczak JM et\u00a0al (2017) Supervisory control synthesis for a waterway lock. In: Proceedings of the 2017 IEEE conference on control technology and applications. IEEE, pp 1562\u2013156. https:\/\/doi.org\/10.1109\/ccta.2017.8062679","DOI":"10.1109\/ccta.2017.8062679"},{"key":"403_CR45","doi-asserted-by":"publisher","unstructured":"Reijnen FFH, Goorden MA, van\u00a0de Mortel-Fronczak JM et\u00a0al (2018a) Application of dependency structure matrices and multilevel synthesis to a production line. In: Proceedings of the 2018 IEEE conference on control technology and applications. IEEE, pp 458\u2013464. https:\/\/doi.org\/10.1109\/ccta.2018.8511449","DOI":"10.1109\/ccta.2018.8511449"},{"key":"403_CR46","doi-asserted-by":"publisher","unstructured":"Reijnen FFH, Reniers MA, van\u00a0de Mortel-Fronczak JM et\u00a0al (2018b) Structured synthesis of fault-tolerant supervisory controllers. In: Proceedings 10th IFAC symposium on fault detection, Supervision and Safety for Technical Processes. Elsevier BV, pp 894\u2013901. https:\/\/doi.org\/10.1016\/j.ifacol.2018.09.681","DOI":"10.1016\/j.ifacol.2018.09.681"},{"issue":"3","key":"403_CR47","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/s10626-020-00314-0","volume":"30","author":"FFH Reijnen","year":"2020","unstructured":"Reijnen FFH, Goorden MA, van de Mortel-Fronczak JM et al (2020) Modeling for supervisor synthesis \u2013 a lock-bridge combination case study. Disc Event Dyna Syst 30(3):499\u2013532. https:\/\/doi.org\/10.1007\/s10626-020-00314-0","journal-title":"Disc Event Dyna Syst"},{"key":"403_CR48","doi-asserted-by":"publisher","unstructured":"Reniers MA, van\u00a0de Mortel-Fronczak JM (2018) An engineering perspective on model-based design of supervisors. Proceedings of the 14th IFAC Workshop on Discrete Event Systems 51(7):257\u2013264. https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.310","DOI":"10.1016\/j.ifacol.2018.06.310"},{"key":"403_CR49","doi-asserted-by":"publisher","unstructured":"Siminiceanu R, Ciardo G (2006) New metrics for static variable ordering in decision diagrams. In: Tools and algorithms for the construction and analysis of systems. Springer Berlin Heidelberg, pp 90\u2013104. https:\/\/doi.org\/10.1007\/11691372_6","DOI":"10.1007\/11691372_6"},{"key":"403_CR50","doi-asserted-by":"publisher","unstructured":"Sk\u00f6ldstam M, \u00c5kesson K, Fabian M (2007) Modeling of discrete event systems using finite automata with variables. In: Proceedings of the 46th IEEE conference on decision and control. IEEE, pp 3387\u20133392. https:\/\/doi.org\/10.1109\/cdc.2007.4434894","DOI":"10.1109\/cdc.2007.4434894"},{"issue":"11","key":"403_CR51","doi-asserted-by":"publisher","first-page":"2651","DOI":"10.1002\/nme.1620281111","volume":"28","author":"SW Sloan","year":"1989","unstructured":"Sloan SW (1989) A FORTRAN program for profile and wavefront reduction. Int J Numer Meth Eng 28(11):2651\u20132679. https:\/\/doi.org\/10.1002\/nme.1620281111","journal-title":"Int J Numer Meth Eng"},{"key":"403_CR52","doi-asserted-by":"publisher","unstructured":"Somenzi F (1999) Binary decision diagrams. In: The VLSI handbook. CRC Press, pp 680\u2013694. https:\/\/doi.org\/10.1201\/9781420049671-29","DOI":"10.1201\/9781420049671-29"},{"key":"403_CR53","doi-asserted-by":"publisher","unstructured":"Song R, Leduc RJ (2006) Symbolic synthesis and verification of hierarchical interface-based supervisory control. In: Proceedings of the 8th IFAC workshop on discrete event systems. IEEE, pp 419\u2013426. https:\/\/doi.org\/10.1109\/wodes.2006.382510","DOI":"10.1109\/wodes.2006.382510"},{"issue":"7","key":"403_CR54","doi-asserted-by":"publisher","first-page":"1627","DOI":"10.1109\/tac.2010.2042342","volume":"55","author":"R Su","year":"2010","unstructured":"Su R, van Schuppen JH, Rooda JE (2010) Aggregative synthesis of distributed supervisors based on automaton abstraction. Trans Automat Control 55(7):1627\u2013164. https:\/\/doi.org\/10.1109\/tac.2010.2042342","journal-title":"Trans Automat Control"},{"key":"403_CR55","doi-asserted-by":"publisher","unstructured":"Theunissen RJM, Petreczky M, Schiffelers RRH et al (2014) Application of supervisory control synthesis to a patient support table of a magnetic resonance imaging scanner. Trans Automat Sci Eng 11(1):20\u201332. https:\/\/doi.org\/10.1109\/tase.2013.2279692","DOI":"10.1109\/tase.2013.2279692"},{"key":"403_CR56","doi-asserted-by":"publisher","unstructured":"Thuijsman SB, Hendriks D, Theunissen RJM et\u00a0al (2019) Computational effort of BDD-based supervisor synthesis of extended finite automata. In: Proceedings of the IEEE 15th international conference on automation science and engineering. IEEE, pp 486\u2013493. https:\/\/doi.org\/10.1109\/coase.2019.8843327","DOI":"10.1109\/coase.2019.8843327"},{"key":"403_CR57","doi-asserted-by":"publisher","unstructured":"Thuijsman SB, Reniers MA, Hendriks D (2021) Efficiently enforcing mutual state exclusion requirements in symbolic supervisor synthesis. In: Proceedings of the IEEE 17th international conference on automation science and engineering. IEEE, pp 777\u2013783. https:\/\/doi.org\/10.1109\/case49439.2021.9551593","DOI":"10.1109\/case49439.2021.9551593"},{"issue":"10","key":"403_CR58","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.1016\/j.conengprac.2006.02.013","volume":"14","author":"A Vahidi","year":"2006","unstructured":"Vahidi A, Fabian M, Lennartson B (2006) Efficient supervisory synthesis of large systems. Control Eng Pract 14(10):1157\u20131167. https:\/\/doi.org\/10.1016\/j.conengprac.2006.02.013","journal-title":"Control Eng Pract"},{"key":"403_CR59","unstructured":"Vos Z (2020) Efficient supervisor synthesis for feature models. Master\u2019s thesis, Eindhoven University of Technology, https:\/\/research.tue.nl\/en\/studentTheses\/initialization-and-termination-of-flexible-manufacturing-systems"},{"key":"403_CR60","doi-asserted-by":"publisher","unstructured":"van Beek DA, Fokkink WJ, Hendriks D et\u00a0al (2014) CIF 3: model-based engineering of supervisory controllers. In: Tools and algorithms for the construction and analysis of systems. Springer Berlin Heidelberg, p 575\u2013580. https:\/\/doi.org\/10.1007\/978-3-642-54862-8_48","DOI":"10.1007\/978-3-642-54862-8_48"},{"key":"403_CR61","doi-asserted-by":"publisher","unstructured":"Wonham W, Cai K, Rudie K (2018) Supervisory control of discrete-event systems: a brief history. Annu Rev Control 45:250\u2013256. https:\/\/doi.org\/10.1016\/j.arcontrol.2018.03.002","DOI":"10.1016\/j.arcontrol.2018.03.002"},{"key":"403_CR62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77452-7","author":"W Wonham","year":"2019","unstructured":"Wonham W, Cai K (2019) Supervisory Control of Discrete-Event Systems. Springer Int Publish. https:\/\/doi.org\/10.1007\/978-3-319-77452-7","journal-title":"Springer Int Publish"},{"key":"403_CR63","doi-asserted-by":"publisher","unstructured":"Ziller R, Schneider K (2003) Reducing complexity of supervisor synthesis. Proceedings of the 2nd IFAC Conference on Control Systems Design pp 183\u2013191. https:\/\/doi.org\/10.1016\/s1474-6670(17)34666-9","DOI":"10.1016\/s1474-6670(17)34666-9"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-024-00403-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-024-00403-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-024-00403-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T10:06:06Z","timestamp":1733738766000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-024-00403-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,12]]},"references-count":63,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["403"],"URL":"https:\/\/doi.org\/10.1007\/s10626-024-00403-4","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2024,9,12]]},"assertion":[{"value":"16 May 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 September 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflict of interest to declare that are relevant to this paper.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of Interest"}}]}}