{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:53:46Z","timestamp":1766451226504,"version":"3.37.3"},"reference-count":96,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,8,21]],"date-time":"2023-08-21T00:00:00Z","timestamp":1692576000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,8,21]],"date-time":"2023-08-21T00:00:00Z","timestamp":1692576000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010061","name":"University of Waikato","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100010061","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2023,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This survey gives an overview of the current research on compositional algorithms for verification and synthesis of modular systems modelled as interacting finite-state machines. Compositional algorithms operate by repeatedly simplifying individual components of a large system, replacing them by smaller so-called <jats:italic>abstractions<\/jats:italic>, while preserving critical properties. In this way, the exponential growth of the state space can be limited, making it possible to analyse much bigger state spaces than possible by standard state space exploration. This paper gives an introduction to the principles underlying compositional methods, followed by a survey of algorithmic solutions from the recent literature that use compositional methods to analyse systems automatically. The focus is on applications in supervisory control of discrete event systems, particularly on methods that verify critical properties or synthesise controllable and nonblocking supervisors.<\/jats:p>","DOI":"10.1007\/s10626-023-00378-8","type":"journal-article","created":{"date-parts":[[2023,8,21]],"date-time":"2023-08-21T11:02:44Z","timestamp":1692615764000},"page":"279-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A survey on compositional algorithms for verification and synthesis in supervisory control"],"prefix":"10.1007","volume":"33","author":[{"given":"Robi","family":"Malik","sequence":"first","affiliation":[]},{"given":"Sahar","family":"Mohajerani","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Fabian","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,8,21]]},"reference":[{"issue":"1","key":"378_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.3182\/20020721-6-ES-1901.00517","volume":"35","author":"K \u00c5kesson","year":"2002","unstructured":"\u00c5kesson K, Flordal H, Fabian M (2002) Exploiting modularity for synthesis and verification of supervisors. IFAC Proc 35(1):175\u2013180. https:\/\/doi.org\/10.3182\/20020721-6-ES-1901.00517","journal-title":"IFAC Proc"},{"key":"378_CR2","doi-asserted-by":"publisher","unstructured":"\u00c5kesson K, Fabian M, Flordal H, Malik R (2006) Supremica\u2014an integrated environment for verification, synthesis and simulation of discrete event systems. In: 8th Int. Workshop on Discrete Event Systems, WODES \u201906. IEEE, pp 384\u2013385. https:\/\/doi.org\/10.1109\/WODES.2006.382401","DOI":"10.1109\/WODES.2006.382401"},{"issue":"06","key":"378_CR3","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"S Akers","year":"1978","unstructured":"Akers S (1978) Binary decision diagrams. IEEE Trans Comput 27(06):509\u2013516. https:\/\/doi.org\/10.1109\/TC.1978.1675141","journal-title":"IEEE Trans Comput"},{"key":"378_CR4","doi-asserted-by":"publisher","unstructured":"Andersen HR, Stirling C, Winskel G (1994) A compositional proof system for the modal $$\\mu $$-calculus. In: 9th Annual Symp. Logic in Computer Science. pp 144\u2013153. https:\/\/doi.org\/10.1109\/LICS.1994.316076","DOI":"10.1109\/LICS.1994.316076"},{"key":"378_CR5","volume-title":"Finite Transition Systems: Semantics of Communicating Systems","author":"A Arnold","year":"1994","unstructured":"Arnold A (1994) Finite Transition Systems: Semantics of Communicating Systems. Prentice-Hall, Hertfordshire"},{"key":"378_CR6","doi-asserted-by":"publisher","unstructured":"Aziz A, Singhal V, Brayton R, Swamy GM (1994) Minimizing interacting finite state machines: a compositional approach to language containment. In: 1994 IEEE Int. Conf. Computer Design: VLSI in Computers and Processors. IEEE, pp 255\u2013261. https:\/\/doi.org\/10.1109\/ICCD.1994.331900","DOI":"10.1109\/ICCD.1994.331900"},{"key":"378_CR7","unstructured":"Baier C, Katoen JP (2008) Principles of Model Checking. MIT Press"},{"key":"378_CR8","doi-asserted-by":"publisher","unstructured":"Balemi S (1992) Input\/output discrete event processes and system modeling. In: Int. Workshop on Discrete Event Systems, WODES \u201992, pp 15\u201327. https:\/\/doi.org\/10.1007\/978-3-0348-9120-2_2","DOI":"10.1007\/978-3-0348-9120-2_2"},{"key":"378_CR9","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (2001) Systems and Software Verification. Springer","DOI":"10.1007\/978-3-662-04558-9"},{"issue":"1\u20133","key":"378_CR10","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"JA Bergstra","year":"1984","unstructured":"Bergstra JA, Klop JW (1984) Process algebra for synchronous communication. Inf Control 60(1\u20133):109\u2013137. https:\/\/doi.org\/10.1016\/S0019-9958(84)80025-X","journal-title":"Inf Control"},{"issue":"3","key":"378_CR11","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1109\/TCST.2004.824795","volume":"12","author":"BA Brandin","year":"2004","unstructured":"Brandin BA, Malik R, Malik P (2004) Incremental verification and synthesis of discrete-event systems guided by counter-examples. IEEE Trans Control Syst Technol 12(3):387\u2013401. https:\/\/doi.org\/10.1109\/TCST.2004.824795","journal-title":"IEEE Trans Control Syst Technol"},{"key":"378_CR12","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/0167-6911(90)90004-E","volume":"15","author":"RD Brandt","year":"1990","unstructured":"Brandt RD, Garg V, Kumar R, Lin F, Marcus SI, Wonham WM (1990) Formulas for calculating supremal controllable and normal sublanguages. Syst Control Lett 15:111\u2013117. https:\/\/doi.org\/10.1016\/0167-6911(90)90004-E","journal-title":"Syst Control Lett"},{"issue":"8","key":"378_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691. https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Trans Comput"},{"issue":"2","key":"378_CR14","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170. https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inf Comput"},{"key":"378_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras CG, Lafortune S (2008) Introduction to Discrete Event Systems, 2nd edn. Springer Science & Business Media, New York","edition":"2"},{"issue":"1","key":"378_CR16","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/295558.295570","volume":"8","author":"SC Cheung","year":"1999","unstructured":"Cheung SC, Kramer J (1999) Checking safety properties using compositional reachability analysis. ACM Trans Softw Eng Methodol 8(1):49\u201378. https:\/\/doi.org\/10.1145\/295558.295570","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"3","key":"378_CR17","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1109\/9.402","volume":"33","author":"R Cieslak","year":"1988","unstructured":"Cieslak R, Desclaux C, Fawaz AS, Varaiya P (1988) Supervisory control of discrete-event processes with partial observations. IEEE Trans Autom Control 33(3):249\u2013260. https:\/\/doi.org\/10.1109\/9.402","journal-title":"IEEE Trans Autom Control"},{"issue":"2","key":"378_CR18","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263. https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans Program Lang Syst"},{"key":"378_CR19","doi-asserted-by":"publisher","unstructured":"Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: 4th Annual Symp. Logic in Computer Science. pp 353\u2013362. https:\/\/doi.org\/10.1109\/LICS.1989.39190","DOI":"10.1109\/LICS.1989.39190"},{"issue":"5","key":"378_CR20","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke EM, Grumberg O, Long DE (1994) Model checking and abstraction. ACM Trans Program Lang Syst 16(5):1512\u20131542. https:\/\/doi.org\/10.1145\/186025.186051","journal-title":"ACM Trans Program Lang Syst"},{"key":"378_CR21","unstructured":"Clarke EM Jr, Grumberg O, Peled DA (1999) Model Checking. MIT Press"},{"issue":"1\u20132","key":"378_CR22","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R De Nicola","year":"1984","unstructured":"De Nicola R, Hennessy MCB (1984) Testing equivalences for processes. Theor Comput Sci 34(1\u20132):83\u2013133. https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0","journal-title":"Theor Comput Sci"},{"issue":"4","key":"378_CR23","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BF01933173","volume":"31","author":"J Eloranta","year":"1991","unstructured":"Eloranta J (1991) Minimizing the number of transitions with respect to observation equivalence. BIT 31(4):397\u2013419. https:\/\/doi.org\/10.1007\/BF01933173","journal-title":"BIT"},{"issue":"1","key":"378_CR24","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson EA, Halpern JY (1986) \u201cSometimes\u2019\u2019 and \u201cnot never\u2019\u2019 revisited: On branching versus linear time temporal logic. J ACM 33(1):151\u2013178. https:\/\/doi.org\/10.1145\/4904.4999","journal-title":"J ACM"},{"key":"378_CR25","doi-asserted-by":"publisher","unstructured":"Feng L, Wonham WM (2006) TCT: A computation tool for supervisory control synthesis. In: 8th Int. Workshop on Discrete Event Systems, WODES \u201906. IEEE, pp 388\u2013389. https:\/\/doi.org\/10.1109\/WODES.2006.382399","DOI":"10.1109\/WODES.2006.382399"},{"issue":"6","key":"378_CR26","doi-asserted-by":"publisher","first-page":"1449","DOI":"10.1109\/TAC.2008.927679","volume":"53","author":"L Feng","year":"2008","unstructured":"Feng L, Wonham WM (2008) Supervisory control architecture for discrete-event systems. IEEE Trans Autom Control 53(6):1449\u20131461. https:\/\/doi.org\/10.1109\/TAC.2008.927679","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR27","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10626-008-0054-3","volume":"20","author":"L Feng","year":"2010","unstructured":"Feng L, Wonham WM (2010) On the computation of natural observers in discrete-event systems. Discret Event Dyn Syst 20:63\u2013102. https:\/\/doi.org\/10.1007\/s10626-008-0054-3","journal-title":"Discret Event Dyn Syst"},{"key":"378_CR28","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"JC Fernandez","year":"1990","unstructured":"Fernandez JC (1990) An implementation of an efficient algorithm for bisimulation equivalence. Sci Comput Program 13:219\u2013236. https:\/\/doi.org\/10.1016\/0167-6423(90)90071-K","journal-title":"Sci Comput Program"},{"key":"378_CR29","doi-asserted-by":"publisher","unstructured":"Flordal, H. and Malik, R. (2006). Modular nonblocking verification using conflict equivalence. In: 8th Int. Workshop on Discrete Event Systems, WODES \u201906. IEEE, pp 100\u2013106. https:\/\/doi.org\/10.1109\/WODES.2006.1678415","DOI":"10.1109\/WODES.2006.1678415"},{"issue":"3","key":"378_CR30","doi-asserted-by":"publisher","first-page":"1914","DOI":"10.1137\/070695526","volume":"48","author":"H Flordal","year":"2009","unstructured":"Flordal H, Malik R (2009) Compositional verification in supervisory control. SIAM J Control Optim 48(3):1914\u20131938. https:\/\/doi.org\/10.1137\/070695526","journal-title":"SIAM J Control Optim"},{"issue":"4","key":"378_CR31","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10626-007-0018-z","volume":"17","author":"H Flordal","year":"2007","unstructured":"Flordal H, Malik R, Fabian M, \u00c5kesson K (2007) Compositional synthesis of maximally permissive supervisors using supervision equivalence. Discret Event Dyn Syst 17(4):475\u2013504. https:\/\/doi.org\/10.1007\/s10626-007-0018-z","journal-title":"Discret Event Dyn Syst"},{"issue":"5","key":"378_CR32","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1109\/3477.875441","volume":"30","author":"P Gohari","year":"2000","unstructured":"Gohari P, Wonham WM (2000) On the complexity of supervisory control design in the RW framework. IEEE Trans Syst Man Cybern 30(5):643\u2013652. https:\/\/doi.org\/10.1109\/3477.875441","journal-title":"IEEE Trans Syst Man Cybern"},{"issue":"4","key":"378_CR33","doi-asserted-by":"publisher","first-page":"1625","DOI":"10.1109\/TAC.2019.2928119","volume":"65","author":"M Goorden","year":"2020","unstructured":"Goorden M, van de Mortel-Fronczak J, Reniers M, Fokkink W, Rooda J (2020) Structuring multilevel discrete-event systems with dependency structure matrices. IEEE Trans Autom Control 65(4):1625\u20131639. https:\/\/doi.org\/10.1109\/TAC.2019.2928119","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR34","doi-asserted-by":"publisher","unstructured":"Graf S, Steffen B (1990) Compositional minimization of finite state systems. In: 1990 Workshop on Computer-Aided Verification, volume 531 of LNCS. Springer, pp 186\u2013196. https:\/\/doi.org\/10.1007\/BFb0023732","DOI":"10.1007\/BFb0023732"},{"key":"378_CR35","doi-asserted-by":"publisher","unstructured":"Heymann M, Lin F (1998) Discrete-event control of nondeterministic systems. IEEE Trans Autom Control 43(1). https:\/\/doi.org\/10.1109\/9.654883","DOI":"10.1109\/9.654883"},{"issue":"9","key":"378_CR36","doi-asserted-by":"publisher","first-page":"1364","DOI":"10.1080\/00207170701799365","volume":"81","author":"RC Hill","year":"2008","unstructured":"Hill RC, Tilbury DM (2008) Incremental hierarchical construction of modular supervisors for discrete-event systems. Int J Control 81(9):1364\u20131281. https:\/\/doi.org\/10.1080\/00207170701799365","journal-title":"Int J Control"},{"issue":"1","key":"378_CR37","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s10626-009-0070-y","volume":"20","author":"RC Hill","year":"2010","unstructured":"Hill RC, Tilbury DM, Lafortune S (2010) Modular supervisory control with equivalence-based abstraction and covering-based conflict resolution. Discret Event Dyn Syst 20(1):139\u2013185. https:\/\/doi.org\/10.1007\/s10626-009-0070-y","journal-title":"Discret Event Dyn Syst"},{"key":"378_CR38","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating Sequential Processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"378_CR39","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"2001","unstructured":"Hopcroft JE, Motwani R, Ullman JD (2001) Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Boston"},{"issue":"4","key":"378_CR40","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/j.ifacol.2021.04.029","volume":"53","author":"J Komenda","year":"2020","unstructured":"Komenda J, Masopust T (2020) Conditions for hierarchical supervisory control under partial observation. IFAC PapersOnLine 53(4):303\u2013308. https:\/\/doi.org\/10.1016\/j.ifacol.2021.04.029","journal-title":"IFAC PapersOnLine"},{"issue":"7","key":"378_CR41","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.ifacol.2018.06.291","volume":"51","author":"J Krook","year":"2018","unstructured":"Krook J, Kianfar R, Zita A, Mohajerani S, Fabian M (2018) Modeling and synthesis of the lane change function of an autonomous vehicle. IFAC PapersOnLine 51(7):133\u2013138. https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.291","journal-title":"IFAC PapersOnLine"},{"issue":"9","key":"378_CR42","doi-asserted-by":"publisher","first-page":"1322","DOI":"10.1109\/TAC.2005.854586","volume":"50","author":"RJ Leduc","year":"2005","unstructured":"Leduc RJ, Brandin BA, Lawford M, Wonham WM (2005) Hierarchical interface-based supervisory control\u2013part I: Serial case. IEEE Trans Autom Control 50(9):1322\u20131335. https:\/\/doi.org\/10.1109\/TAC.2005.854586","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR43","doi-asserted-by":"publisher","first-page":"477","DOI":"10.3166\/ejc.8.477-491","volume":"8","author":"SH Lee","year":"2002","unstructured":"Lee SH, Wong KC (2002) Structural decentralised control of concurrent discrete-event systems. Eur J Control 8:477\u2013491. https:\/\/doi.org\/10.3166\/ejc.8.477-491","journal-title":"Eur J Control"},{"key":"378_CR44","doi-asserted-by":"publisher","unstructured":"Li Y (1997) On deadlock-free modular supervisory control of discrete-event systems. IEEE Trans Autom Control 42(12). https:\/\/doi.org\/10.1109\/9.650022","DOI":"10.1109\/9.650022"},{"issue":"2","key":"378_CR45","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1109\/TSMCC.2007.913920","volume":"38","author":"Z Li","year":"2008","unstructured":"Li Z, Zhou M, Wu N (2008) A survey and comparison of Petri net-based deadlock prevention policies for flexible manufacturing systems. IEEE Trans Syst Man Cybern 38(2):173\u2013188. https:\/\/doi.org\/10.1109\/TSMCC.2007.913920","journal-title":"IEEE Trans Syst Man Cybern"},{"issue":"3","key":"378_CR46","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0255(88)90001-1","volume":"44","author":"F Lin","year":"1988","unstructured":"Lin F, Wonham WM (1988) On observability of discrete-event systems. Inform Sci 44(3):173\u2013198. https:\/\/doi.org\/10.1016\/0020-0255(88)90001-1","journal-title":"Inform Sci"},{"key":"378_CR47","unstructured":"Lindsey J (2012) The set of certain conflicts. Honours project report, Dept. of Computer Science, University of Waikato"},{"key":"378_CR48","doi-asserted-by":"publisher","unstructured":"Malik R (2004) On the set of certain conflicts of a given language. In: 7th Int. Workshop on Discrete Event Systems. WODES \u201904. IFAC, pp 277\u2013282. https:\/\/doi.org\/10.1016\/S1474-6670(17)30757-7","DOI":"10.1016\/S1474-6670(17)30757-7"},{"key":"378_CR49","unstructured":"Malik R (2010) The language of certain conflicts of a nondeterministic process. Working Paper 05\/2010, Dept. of Computer Science, University of Waikato, Hamilton, New Zealand. http:\/\/hdl.handle.net\/10289\/4108"},{"key":"378_CR50","doi-asserted-by":"publisher","unstructured":"Malik R (2015) Advanced selfloop removal in compositional nonblocking verification of discrete event systems. In: 11th Int. Conf. Automation Science and Engineering, CASE 2015. https:\/\/doi.org\/10.1109\/CoASE.2015.7294182","DOI":"10.1109\/CoASE.2015.7294182"},{"key":"378_CR51","doi-asserted-by":"publisher","unstructured":"Malik R (2016) Programming a fast explicit conflict checker. In: 13th Int. Workshop on Discrete Event Systems, WODES \u201916. IEEE, pp 464\u2013469. https:\/\/doi.org\/10.1109\/WODES.2016.7497885","DOI":"10.1109\/WODES.2016.7497885"},{"issue":"6","key":"378_CR52","doi-asserted-by":"publisher","first-page":"205","DOI":"10.3182\/20070613-3-FR-4909.00037","volume":"40","author":"R Malik","year":"2007","unstructured":"Malik R, Flordal H, Pena PN (2007) Conflicts and projections. IFAC PapersOnLine 40(6):205\u2013210. https:\/\/doi.org\/10.3182\/20070613-3-FR-4909.00037","journal-title":"IFAC PapersOnLine"},{"key":"378_CR53","doi-asserted-by":"publisher","unstructured":"Malik R, Leduc R (2008) Generalised nonblocking. In: 9th Int. Workshop on Discrete Event Systems, WODES \u201908. IEEE, pp 340\u2013345. https:\/\/doi.org\/10.1109\/WODES.2008.4605969","DOI":"10.1109\/WODES.2008.4605969"},{"issue":"8","key":"378_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TAC.2013.2248255","volume":"58","author":"R Malik","year":"2013","unstructured":"Malik R, Leduc R (2013) Compositional nonblocking verification using generalised nonblocking abstractions. IEEE Trans Autom Control 58(8):1\u201313. https:\/\/doi.org\/10.1109\/TAC.2013.2248255","journal-title":"IEEE Trans Autom Control"},{"issue":"4","key":"378_CR55","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1142\/S012905410600411X","volume":"17","author":"R Malik","year":"2006","unstructured":"Malik R, Streader D, Reeves S (2006) Conflicts and fair testing. Int J Found Comput Sci 17(4):797\u2013813. https:\/\/doi.org\/10.1142\/S012905410600411X","journal-title":"Int J Found Comput Sci"},{"issue":"2","key":"378_CR56","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10626-019-00302-z","volume":"30","author":"R Malik","year":"2020","unstructured":"Malik R, Teixeira M (2020) Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction. Discret Event Dyn Syst 30(2):211\u2013241. https:\/\/doi.org\/10.1007\/s10626-019-00302-z","journal-title":"Discret Event Dyn Syst"},{"issue":"2","key":"378_CR57","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10626-019-00305-w","volume":"30","author":"R Malik","year":"2020","unstructured":"Malik R, Ware S (2020) On the computation of counterexamples in compositional nonblocking verification. Discret Event Dyn Syst 30(2):301\u2013334. https:\/\/doi.org\/10.1007\/s10626-019-00305-w","journal-title":"Discret Event Dyn Syst"},{"key":"378_CR58","unstructured":"Milner R (1989) Communication and concurrency. Series in Computer Science. Prentice-Hall"},{"issue":"29","key":"378_CR59","doi-asserted-by":"publisher","first-page":"239","DOI":"10.3182\/20121003-3-MX-4033.00040","volume":"45","author":"S Mohajerani","year":"2012","unstructured":"Mohajerani S, Malik R, Fabian M (2012) An algorithm for weak synthesis observation equivalence for compositional supervisor synthesis. IFAC PapersOnLine 45(29):239\u2013244. https:\/\/doi.org\/10.3182\/20121003-3-MX-4033.00040","journal-title":"IFAC PapersOnLine"},{"key":"378_CR60","unstructured":"Mohajerani S, Malik R, Fabian M (2012b) Synthesis observation equivalence and weak synthesis observation equivalence. Working Paper 03\/2012, Dept. of Computer Science, University of Waikato, Hamilton, New Zealand. http:\/\/hdl.handle.net\/10289\/6585"},{"key":"378_CR61","doi-asserted-by":"publisher","unstructured":"Mohajerani S, Malik R, Fabian M (2012c) Transition removal for compositional supervisor synthesis. In: 8th Int. Conf. Automation Science and Engineering, CASE 2012. pp 690\u2013695. https:\/\/doi.org\/10.1109\/CoASE.2012.6386447","DOI":"10.1109\/CoASE.2012.6386447"},{"issue":"1","key":"378_CR62","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1109\/TAC.2013.2283109","volume":"59","author":"S Mohajerani","year":"2014","unstructured":"Mohajerani S, Malik R, Fabian M (2014) A framework for compositional synthesis of modular nonblocking supervisors. IEEE Trans Autom Control 59(1):150\u2013162. https:\/\/doi.org\/10.1109\/TAC.2013.2283109","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR63","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/j.automatica.2016.10.012","volume":"76","author":"S Mohajerani","year":"2017","unstructured":"Mohajerani S, Malik R, Fabian M (2017) Compositional synthesis of supervisors in the form of state machines and state maps. Automatica 76:277\u2013281. https:\/\/doi.org\/10.1016\/j.automatica.2016.10.012","journal-title":"Automatica"},{"key":"378_CR64","doi-asserted-by":"publisher","unstructured":"Mohajerani S, Malik R, Ware S, Fabian M (2011) On the use of observation equivalence in synthesis abstraction. In: 3rd IFAC Workshop on Dependable Control of Discrete Systems, DCDS 2011. pp 84\u201389. https:\/\/doi.org\/10.1109\/DCDS.2011.5970323","DOI":"10.1109\/DCDS.2011.5970323"},{"issue":"12","key":"378_CR65","doi-asserted-by":"publisher","first-page":"2803","DOI":"10.1109\/TAC.2009.2031730","volume":"54","author":"PN Pena","year":"2009","unstructured":"Pena PN, Cury JER, Lafortune S (2009) Verification of nonconflict of supervisors using abstractions. IEEE Trans Autom Control 54(12):2803\u20132815. https:\/\/doi.org\/10.1109\/TAC.2009.2031730","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR66","doi-asserted-by":"publisher","unstructured":"Pena PN, Cury JER, Malik R, Lafortune S (2010) Efficient computation of observer projections using OP-Verifiers. In: 10th Int. Workshop on Discrete Event Systems, WODES \u201910. pp 416\u2013421. https:\/\/doi.org\/10.3182\/20100830-3-DE-4013.00067","DOI":"10.3182\/20100830-3-DE-4013.00067"},{"issue":"8","key":"378_CR67","doi-asserted-by":"publisher","first-page":"2176","DOI":"10.1109\/TAC.2014.2298985","volume":"59","author":"PN Pena","year":"2014","unstructured":"Pena PN, Bravo HJ, da Cunha AEC, Malik R, Lafortune S, Cury JER (2014) Verification of the observer property in discrete event systems. IEEE Trans Autom Control 59(8):2176\u20132181. https:\/\/doi.org\/10.1109\/TAC.2014.2298985","journal-title":"IEEE Trans Autom Control"},{"issue":"2","key":"378_CR68","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.scico.2015.05.010","volume":"113","author":"C Pilbrow","year":"2015","unstructured":"Pilbrow C, Malik R (2015) An algorithm for compositional nonblocking verification using special events. Sci Comput Programm 113(2):119\u2013148. https:\/\/doi.org\/10.1016\/j.scico.2015.05.010","journal-title":"Sci Comput Programm"},{"key":"378_CR69","doi-asserted-by":"publisher","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th Annual Symp. Found. of Computer Science. pp 46\u201357. https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"378_CR70","doi-asserted-by":"crossref","unstructured":"Ramadge PJ (1983) Control and Supervision of Discrete Event Processes. Ph.D. thesis, Dept. of Electrical Engineering, University of Toronto, ON, Canada","DOI":"10.1109\/CDC.1982.268351"},{"issue":"1","key":"378_CR71","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398. https:\/\/doi.org\/10.1109\/5.21072","journal-title":"Proc IEEE"},{"issue":"2","key":"378_CR72","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, Rooda JE (2020) Modeling for supervisor synthesis \u2013 a lock-bridge combination case study. Discret Event Dyn Syst 30(2):499\u2013532. https:\/\/doi.org\/10.1007\/s10626-020-00314-0","journal-title":"Discret Event Dyn Syst"},{"key":"378_CR73","unstructured":"Roscoe AW (1994) Model-checking CSP. In: Roscoe AW (ed) A Classical Mind: Essays in Honour of C. A. R, Hoare. Prentice-Hall"},{"key":"378_CR74","doi-asserted-by":"publisher","unstructured":"Roscoe AW, Gardiner PHB, Goldsmith M, Hulance JR, Jackson DM, Scattergood JB (1995) Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Workshop on Tools and Algorithms for The Construction and Analysis of Systems, TACAS \u201995, volume 1019 of LNCS. Springer, pp 133\u2013152. https:\/\/doi.org\/10.1007\/3-540-60630-0_7","DOI":"10.1007\/3-540-60630-0_7"},{"issue":"11","key":"378_CR75","doi-asserted-by":"publisher","first-page":"1692","DOI":"10.1109\/9.173140","volume":"37","author":"K Rudie","year":"1992","unstructured":"Rudie K, Wonham W (1992) Think globally, act locally: Decentralized supervisory control. IEEE Trans Autom Control 37(11):1692\u20131708. https:\/\/doi.org\/10.1109\/9.173140","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR76","doi-asserted-by":"publisher","unstructured":"Schmidt K, Breindl C (2008) On maximal permissiveness of hierarchical and modular supervisory control approaches for discrete event systems. In: 9th Int. Workshop on Discrete Event Systems, WODES \u201908. IEEE, pp 462\u2013467. https:\/\/doi.org\/10.1109\/WODES.2008.4605990","DOI":"10.1109\/WODES.2008.4605990"},{"issue":"4","key":"378_CR77","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1109\/TAC.2010.2067250","volume":"56","author":"K Schmidt","year":"2011","unstructured":"Schmidt K, Breindl C (2011) Maximally permissive hierarchical control of decentralized discrete event systems. IEEE Trans Autom Control 56(4):723\u2013737. https:\/\/doi.org\/10.1109\/TAC.2010.2067250","journal-title":"IEEE Trans Autom Control"},{"key":"378_CR78","doi-asserted-by":"publisher","unstructured":"Schmidt K, Moor T (2006) Marked-string accepting observers for the hierarchical and decentralized control of discrete event systems. In: 8th Int. Workshop on Discrete Event Systems, WODES \u201906. IEEE, pp 413\u2013418. https:\/\/doi.org\/10.1109\/WODES.2006.382509","DOI":"10.1109\/WODES.2006.382509"},{"issue":"7","key":"378_CR79","doi-asserted-by":"publisher","first-page":"1267","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. IEEE Trans Autom Control 55(7):1267\u20131640. https:\/\/doi.org\/10.1109\/TAC.2010.2042342","journal-title":"IEEE Trans Autom Control"},{"issue":"11","key":"378_CR80","doi-asserted-by":"publisher","first-page":"2527","DOI":"10.1109\/TAC.2010.2046931","volume":"55","author":"R Su","year":"2010","unstructured":"Su R, van Schuppen JH, Rooda JE (2010) Model abstraction of nondeterministic finite-state automata in supervisor synthesis. IEEE Trans Autom Control 55(11):2527\u20132541. https:\/\/doi.org\/10.1109\/TAC.2010.2046931","journal-title":"IEEE Trans Autom Control"},{"issue":"6","key":"378_CR81","doi-asserted-by":"publisher","first-page":"968","DOI":"10.1016\/j.automatica.2010.02.025","volume":"46","author":"R Su","year":"2010","unstructured":"Su R, van Schuppen JH, Rooda JE, Hofkamp AT (2010) Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6):968\u2013978. https:\/\/doi.org\/10.1016\/j.automatica.2010.02.025","journal-title":"Automatica"},{"key":"378_CR82","doi-asserted-by":"publisher","first-page":"108470","DOI":"10.1016\/j.automatica.2019.06.022","volume":"108","author":"S Takai","year":"2019","unstructured":"Takai S (2019) Bisimilarity enforcing supervisory control of nondeterministic discrete event systems with nondeterministic specifications. Automatica 108:108470. https:\/\/doi.org\/10.1016\/j.automatica.2019.06.022","journal-title":"Automatica"},{"key":"378_CR83","unstructured":"Tanenbaum AS (1992) Modern Operating Systems. Prentice-Hall"},{"key":"378_CR84","unstructured":"Ware S (2007) Modular finite-state machine analysis. Honours project report, Dept. of Computer Science, University of Waikato"},{"key":"378_CR85","unstructured":"Ware S (2014) On Conflicts in Concurrent Systems. Ph.D. thesis, Dept. of Computer Science, University of Waikato. http:\/\/hdl.handle.net\/10289\/8545"},{"key":"378_CR86","doi-asserted-by":"publisher","unstructured":"Ware S, Malik R (2008) The use of language projection for compositional verification of discrete event systems. In: 9th Int. Workshop on Discrete Event Systems, WODES \u201908. IEEE, pp 322\u2013327. https:\/\/doi.org\/10.1109\/WODES.2008.4605966","DOI":"10.1109\/WODES.2008.4605966"},{"issue":"4","key":"378_CR87","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s10626-012-0133-3","volume":"22","author":"S Ware","year":"2012","unstructured":"Ware S, Malik R (2012) Conflict-preserving abstraction of discrete event systems using annotated automata. Discret Event Dyn Syst 22(4):451\u2013477. https:\/\/doi.org\/10.1007\/s10626-012-0133-3","journal-title":"Discret Event Dyn Syst"},{"issue":"8","key":"378_CR88","doi-asserted-by":"publisher","first-page":"1183","DOI":"10.1142\/S0129054113500287","volume":"24","author":"S Ware","year":"2013","unstructured":"Ware S, Malik R (2013) Compositional verification of the generalized nonblocking property using abstraction and canonical automata. Int J Found Comput Sci 24(8):1183\u20131208. https:\/\/doi.org\/10.1142\/S0129054113500287","journal-title":"Int J Found Comput Sci"},{"key":"378_CR89","doi-asserted-by":"publisher","unstructured":"Ware S, Malik R, Mohajerani S, Fabian M (2013) Certainly unsupervisable states. In: 2nd Int. Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2013. pp 3\u201318. https:\/\/doi.org\/10.1007\/978-3-319-05416-2_18","DOI":"10.1007\/978-3-319-05416-2_18"},{"issue":"5","key":"378_CR90","doi-asserted-by":"publisher","first-page":"1143","DOI":"10.1080\/00207179108934202","volume":"54","author":"Y Willner","year":"1991","unstructured":"Willner Y, Heymann M (1991) Supervisory control of concurrent discrete-event systems. Int J Control 54(5):1143\u20131169. https:\/\/doi.org\/10.1080\/00207179108934202","journal-title":"Int J Control"},{"issue":"3","key":"378_CR91","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/BF01797154","volume":"6","author":"KC Wong","year":"1996","unstructured":"Wong KC, Wonham WM (1996) Hierarchical control of discrete-event systems. Discret Event Dyn Syst 6(3):241\u2013273. https:\/\/doi.org\/10.1007\/BF01797154","journal-title":"Discret Event Dyn Syst"},{"key":"378_CR92","doi-asserted-by":"crossref","unstructured":"Wonham WM (2013) Supervisory control of discrete-event systems. Systems Control Group, Dept. of Electrical Engineering, University of Toronto, ON, Canada","DOI":"10.1007\/978-1-4471-5102-9_54-1"},{"issue":"1","key":"378_CR93","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BF02551233","volume":"1","author":"WM Wonham","year":"1988","unstructured":"Wonham WM, Ramadge PJ (1988) Modular supervisory control of discrete event systems. Math Control Signals Syst 1(1):13\u201330. https:\/\/doi.org\/10.1007\/BF02551233","journal-title":"Math Control Signals Syst"},{"key":"378_CR94","unstructured":"Yeh WJ, Young M (1993) Hierarchical tracing of concurrent programs. In: 3rd Irvine Software Symp., ISS \u201993"},{"key":"378_CR95","doi-asserted-by":"publisher","unstructured":"Zhang ZH, Wonham WM (2002) STCT: An efficient algorithm for supervisory control design. In: Caillaud B, Darondeau P, Lavagno L, Xie X (Eds) Synthesis and Control of Discrete Event Systems, 77\u2013100. Kluwer, Dordrecht, the Netherlands. https:\/\/doi.org\/10.1007\/978-1-4757-6656-1_5","DOI":"10.1007\/978-1-4757-6656-1_5"},{"issue":"10","key":"378_CR96","doi-asserted-by":"publisher","first-page":"1125","DOI":"10.1109\/9.58555","volume":"35","author":"H Zhong","year":"1990","unstructured":"Zhong H, Wonham WM (1990) On the consistency of hierarchical supervision in discrete-event systems. IEEE Trans Autom Control 35(10):1125\u20131134. https:\/\/doi.org\/10.1109\/9.58555","journal-title":"IEEE Trans Autom Control"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-023-00378-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-023-00378-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-023-00378-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T11:13:06Z","timestamp":1694430786000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-023-00378-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,21]]},"references-count":96,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["378"],"URL":"https:\/\/doi.org\/10.1007\/s10626-023-00378-8","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2023,8,21]]},"assertion":[{"value":"16 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 August 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors have no conflicts of interest to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with ethical standards"}}]}}