none 10.1007/s10626-023-00378-8 Springer Science and Business Media LLC Springer-Verlag 297 152407160 2668 20230911130158638 10.1007 2023-09-11T11:13:06Z 2023-08-21T11:02:44Z 13 Discrete Event Dynamic Systems Discrete Event Dyn Syst 0924-6703 1573-7594 09 2023 33 3 Robi Malik Sahar Mohajerani Martin Fabian Abstract 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 abstractions , 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. 08 21 2023 09 2023 279 340 378 1 10.1007/springer_crossmark_policy link.springer.com false 16 March 2022 3 May 2023 21 August 2023 The authors have no conflicts of interest to declare that are relevant to the content of this article. University of Waikato http://dx.doi.org/10.13039/100010061 https://creativecommons.org/licenses/by/4.0 https://creativecommons.org/licenses/by/4.0 10.1007/s10626-023-00378-8 20230911130158638 https://link.springer.com/10.1007/s10626-023-00378-8 https://link.springer.com/content/pdf/10.1007/s10626-023-00378-8.pdf https://link.springer.com/content/pdf/10.1007/s10626-023-00378-8.pdf https://link.springer.com/article/10.1007/s10626-023-00378-8/fulltext.html IFAC Proc K Åkesson 35 1 175 2002 10.3182/20020721-6-ES-1901.00517 Åkesson K, Flordal H, Fabian M (2002) Exploiting modularity for synthesis and verification of supervisors. IFAC Proc 35(1):175–180. https://doi.org/10.3182/20020721-6-ES-1901.00517 10.1109/WODES.2006.382401 Åkesson K, Fabian M, Flordal H, Malik R (2006) Supremica—an integrated environment for verification, synthesis and simulation of discrete event systems. In: 8th Int. Workshop on Discrete Event Systems, WODES ’06. IEEE, pp 384–385. https://doi.org/10.1109/WODES.2006.382401 IEEE Trans Comput S Akers 27 06 509 1978 10.1109/TC.1978.1675141 Akers S (1978) Binary decision diagrams. IEEE Trans Comput 27(06):509–516. https://doi.org/10.1109/TC.1978.1675141 10.1109/LICS.1994.316076 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–153. https://doi.org/10.1109/LICS.1994.316076 A Arnold 1994 Finite Transition Systems: Semantics of Communicating Systems Arnold A (1994) Finite Transition Systems: Semantics of Communicating Systems. Prentice-Hall, Hertfordshire 10.1109/ICCD.1994.331900 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–261. https://doi.org/10.1109/ICCD.1994.331900 Baier C, Katoen JP (2008) Principles of Model Checking. MIT Press 10.1007/978-3-0348-9120-2_2 Balemi S (1992) Input/output discrete event processes and system modeling. In: Int. Workshop on Discrete Event Systems, WODES ’92, pp 15–27. https://doi.org/10.1007/978-3-0348-9120-2_2 10.1007/978-3-662-04558-9 Bérard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (2001) Systems and Software Verification. Springer Inf Control JA Bergstra 60 1–3 109 1984 10.1016/S0019-9958(84)80025-X Bergstra JA, Klop JW (1984) Process algebra for synchronous communication. Inf Control 60(1–3):109–137. https://doi.org/10.1016/S0019-9958(84)80025-X IEEE Trans Control Syst Technol BA Brandin 12 3 387 2004 10.1109/TCST.2004.824795 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–401. https://doi.org/10.1109/TCST.2004.824795 Syst Control Lett RD Brandt 15 111 1990 10.1016/0167-6911(90)90004-E 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–117. https://doi.org/10.1016/0167-6911(90)90004-E IEEE Trans Comput RE Bryant 35 8 677 1986 10.1109/TC.1986.1676819 Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677–691. https://doi.org/10.1109/TC.1986.1676819 Inf Comput JR Burch 98 2 142 1992 10.1016/0890-5401(92)90017-A Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170. https://doi.org/10.1016/0890-5401(92)90017-A CG Cassandras 2008 Introduction to Discrete Event Systems 2 10.1007/978-0-387-68612-7 Cassandras CG, Lafortune S (2008) Introduction to Discrete Event Systems, 2nd edn. Springer Science & Business Media, New York ACM Trans Softw Eng Methodol SC Cheung 8 1 49 1999 10.1145/295558.295570 Cheung SC, Kramer J (1999) Checking safety properties using compositional reachability analysis. ACM Trans Softw Eng Methodol 8(1):49–78. https://doi.org/10.1145/295558.295570 IEEE Trans Autom Control R Cieslak 33 3 249 1988 10.1109/9.402 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–260. https://doi.org/10.1109/9.402 ACM Trans Program Lang Syst EM Clarke 8 2 244 1986 10.1145/5397.5399 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–263. https://doi.org/10.1145/5397.5399 10.1109/LICS.1989.39190 Clarke EM, Long DE, McMillan KL (1989) Compositional model checking. In: 4th Annual Symp. Logic in Computer Science. pp 353–362. https://doi.org/10.1109/LICS.1989.39190 ACM Trans Program Lang Syst EM Clarke 16 5 1512 1994 10.1145/186025.186051 Clarke EM, Grumberg O, Long DE (1994) Model checking and abstraction. ACM Trans Program Lang Syst 16(5):1512–1542. https://doi.org/10.1145/186025.186051 Clarke EM Jr, Grumberg O, Peled DA (1999) Model Checking. MIT Press Theor Comput Sci R De Nicola 34 1–2 83 1984 10.1016/0304-3975(84)90113-0 De Nicola R, Hennessy MCB (1984) Testing equivalences for processes. Theor Comput Sci 34(1–2):83–133. https://doi.org/10.1016/0304-3975(84)90113-0 BIT J Eloranta 31 4 397 1991 10.1007/BF01933173 Eloranta J (1991) Minimizing the number of transitions with respect to observation equivalence. BIT 31(4):397–419. https://doi.org/10.1007/BF01933173 J ACM EA Emerson 33 1 151 1986 10.1145/4904.4999 Emerson EA, Halpern JY (1986) “Sometimes’’ and “not never’’ revisited: On branching versus linear time temporal logic. J ACM 33(1):151–178. https://doi.org/10.1145/4904.4999 10.1109/WODES.2006.382399 Feng L, Wonham WM (2006) TCT: A computation tool for supervisory control synthesis. In: 8th Int. Workshop on Discrete Event Systems, WODES ’06. IEEE, pp 388–389. https://doi.org/10.1109/WODES.2006.382399 IEEE Trans Autom Control L Feng 53 6 1449 2008 10.1109/TAC.2008.927679 Feng L, Wonham WM (2008) Supervisory control architecture for discrete-event systems. IEEE Trans Autom Control 53(6):1449–1461. https://doi.org/10.1109/TAC.2008.927679 Discret Event Dyn Syst L Feng 20 63 2010 10.1007/s10626-008-0054-3 Feng L, Wonham WM (2010) On the computation of natural observers in discrete-event systems. Discret Event Dyn Syst 20:63–102. https://doi.org/10.1007/s10626-008-0054-3 Sci Comput Program JC Fernandez 13 219 1990 10.1016/0167-6423(90)90071-K Fernandez JC (1990) An implementation of an efficient algorithm for bisimulation equivalence. Sci Comput Program 13:219–236. https://doi.org/10.1016/0167-6423(90)90071-K 10.1109/WODES.2006.1678415 Flordal, H. and Malik, R. (2006). Modular nonblocking verification using conflict equivalence. In: 8th Int. Workshop on Discrete Event Systems, WODES ’06. IEEE, pp 100–106. https://doi.org/10.1109/WODES.2006.1678415 SIAM J Control Optim H Flordal 48 3 1914 2009 10.1137/070695526 Flordal H, Malik R (2009) Compositional verification in supervisory control. SIAM J Control Optim 48(3):1914–1938. https://doi.org/10.1137/070695526 Discret Event Dyn Syst H Flordal 17 4 475 2007 10.1007/s10626-007-0018-z Flordal H, Malik R, Fabian M, Åkesson K (2007) Compositional synthesis of maximally permissive supervisors using supervision equivalence. Discret Event Dyn Syst 17(4):475–504. https://doi.org/10.1007/s10626-007-0018-z IEEE Trans Syst Man Cybern P Gohari 30 5 643 2000 10.1109/3477.875441 Gohari P, Wonham WM (2000) On the complexity of supervisory control design in the RW framework. IEEE Trans Syst Man Cybern 30(5):643–652. https://doi.org/10.1109/3477.875441 IEEE Trans Autom Control M Goorden 65 4 1625 2020 10.1109/TAC.2019.2928119 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–1639. https://doi.org/10.1109/TAC.2019.2928119 10.1007/BFb0023732 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–196. https://doi.org/10.1007/BFb0023732 10.1109/9.654883 Heymann M, Lin F (1998) Discrete-event control of nondeterministic systems. IEEE Trans Autom Control 43(1). https://doi.org/10.1109/9.654883 Int J Control RC Hill 81 9 1364 2008 10.1080/00207170701799365 Hill RC, Tilbury DM (2008) Incremental hierarchical construction of modular supervisors for discrete-event systems. Int J Control 81(9):1364–1281. https://doi.org/10.1080/00207170701799365 Discret Event Dyn Syst RC Hill 20 1 139 2010 10.1007/s10626-009-0070-y 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–185. https://doi.org/10.1007/s10626-009-0070-y 10.1007/978-3-642-82921-5_4 Hoare CAR (1985) Communicating Sequential Processes. Prentice-Hall JE Hopcroft 2001 Introduction to Automata Theory, Languages, and Computation Hopcroft JE, Motwani R, Ullman JD (2001) Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Boston IFAC PapersOnLine J Komenda 53 4 303 2020 10.1016/j.ifacol.2021.04.029 Komenda J, Masopust T (2020) Conditions for hierarchical supervisory control under partial observation. IFAC PapersOnLine 53(4):303–308. https://doi.org/10.1016/j.ifacol.2021.04.029 IFAC PapersOnLine J Krook 51 7 133 2018 10.1016/j.ifacol.2018.06.291 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–138. https://doi.org/10.1016/j.ifacol.2018.06.291 IEEE Trans Autom Control RJ Leduc 50 9 1322 2005 10.1109/TAC.2005.854586 Leduc RJ, Brandin BA, Lawford M, Wonham WM (2005) Hierarchical interface-based supervisory control–part I: Serial case. IEEE Trans Autom Control 50(9):1322–1335. https://doi.org/10.1109/TAC.2005.854586 Eur J Control SH Lee 8 477 2002 10.3166/ejc.8.477-491 Lee SH, Wong KC (2002) Structural decentralised control of concurrent discrete-event systems. Eur J Control 8:477–491. https://doi.org/10.3166/ejc.8.477-491 10.1109/9.650022 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 IEEE Trans Syst Man Cybern Z Li 38 2 173 2008 10.1109/TSMCC.2007.913920 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–188. https://doi.org/10.1109/TSMCC.2007.913920 Inform Sci F Lin 44 3 173 1988 10.1016/0020-0255(88)90001-1 Lin F, Wonham WM (1988) On observability of discrete-event systems. Inform Sci 44(3):173–198. https://doi.org/10.1016/0020-0255(88)90001-1 Lindsey J (2012) The set of certain conflicts. Honours project report, Dept. of Computer Science, University of Waikato 10.1016/S1474-6670(17)30757-7 Malik R (2004) On the set of certain conflicts of a given language. In: 7th Int. Workshop on Discrete Event Systems. WODES ’04. IFAC, pp 277–282. https://doi.org/10.1016/S1474-6670(17)30757-7 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 10.1109/CoASE.2015.7294182 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 10.1109/WODES.2016.7497885 Malik R (2016) Programming a fast explicit conflict checker. In: 13th Int. Workshop on Discrete Event Systems, WODES ’16. IEEE, pp 464–469. https://doi.org/10.1109/WODES.2016.7497885 IFAC PapersOnLine R Malik 40 6 205 2007 10.3182/20070613-3-FR-4909.00037 Malik R, Flordal H, Pena PN (2007) Conflicts and projections. IFAC PapersOnLine 40(6):205–210. https://doi.org/10.3182/20070613-3-FR-4909.00037 10.1109/WODES.2008.4605969 Malik R, Leduc R (2008) Generalised nonblocking. In: 9th Int. Workshop on Discrete Event Systems, WODES ’08. IEEE, pp 340–345. https://doi.org/10.1109/WODES.2008.4605969 IEEE Trans Autom Control R Malik 58 8 1 2013 10.1109/TAC.2013.2248255 Malik R, Leduc R (2013) Compositional nonblocking verification using generalised nonblocking abstractions. IEEE Trans Autom Control 58(8):1–13. https://doi.org/10.1109/TAC.2013.2248255 Int J Found Comput Sci R Malik 17 4 797 2006 10.1142/S012905410600411X Malik R, Streader D, Reeves S (2006) Conflicts and fair testing. Int J Found Comput Sci 17(4):797–813. https://doi.org/10.1142/S012905410600411X Discret Event Dyn Syst R Malik 30 2 211 2020 10.1007/s10626-019-00302-z 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–241. https://doi.org/10.1007/s10626-019-00302-z Discret Event Dyn Syst R Malik 30 2 301 2020 10.1007/s10626-019-00305-w Malik R, Ware S (2020) On the computation of counterexamples in compositional nonblocking verification. Discret Event Dyn Syst 30(2):301–334. https://doi.org/10.1007/s10626-019-00305-w Milner R (1989) Communication and concurrency. Series in Computer Science. Prentice-Hall IFAC PapersOnLine S Mohajerani 45 29 239 2012 10.3182/20121003-3-MX-4033.00040 Mohajerani S, Malik R, Fabian M (2012) An algorithm for weak synthesis observation equivalence for compositional supervisor synthesis. IFAC PapersOnLine 45(29):239–244. https://doi.org/10.3182/20121003-3-MX-4033.00040 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 10.1109/CoASE.2012.6386447 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–695. https://doi.org/10.1109/CoASE.2012.6386447 IEEE Trans Autom Control S Mohajerani 59 1 150 2014 10.1109/TAC.2013.2283109 Mohajerani S, Malik R, Fabian M (2014) A framework for compositional synthesis of modular nonblocking supervisors. IEEE Trans Autom Control 59(1):150–162. https://doi.org/10.1109/TAC.2013.2283109 Automatica S Mohajerani 76 277 2017 10.1016/j.automatica.2016.10.012 Mohajerani S, Malik R, Fabian M (2017) Compositional synthesis of supervisors in the form of state machines and state maps. Automatica 76:277–281. https://doi.org/10.1016/j.automatica.2016.10.012 10.1109/DCDS.2011.5970323 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–89. https://doi.org/10.1109/DCDS.2011.5970323 IEEE Trans Autom Control PN Pena 54 12 2803 2009 10.1109/TAC.2009.2031730 Pena PN, Cury JER, Lafortune S (2009) Verification of nonconflict of supervisors using abstractions. IEEE Trans Autom Control 54(12):2803–2815. https://doi.org/10.1109/TAC.2009.2031730 10.3182/20100830-3-DE-4013.00067 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 ’10. pp 416–421. https://doi.org/10.3182/20100830-3-DE-4013.00067 IEEE Trans Autom Control PN Pena 59 8 2176 2014 10.1109/TAC.2014.2298985 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–2181. https://doi.org/10.1109/TAC.2014.2298985 Sci Comput Programm C Pilbrow 113 2 119 2015 10.1016/j.scico.2015.05.010 Pilbrow C, Malik R (2015) An algorithm for compositional nonblocking verification using special events. Sci Comput Programm 113(2):119–148. https://doi.org/10.1016/j.scico.2015.05.010 10.1109/SFCS.1977.32 Pnueli A (1977) The temporal logic of programs. In: 18th Annual Symp. Found. of Computer Science. pp 46–57. https://doi.org/10.1109/SFCS.1977.32 10.1109/CDC.1982.268351 Ramadge PJ (1983) Control and Supervision of Discrete Event Processes. Ph.D. thesis, Dept. of Electrical Engineering, University of Toronto, ON, Canada Proc IEEE PJG Ramadge 77 1 81 1989 10.1109/5.21072 Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81–98. https://doi.org/10.1109/5.21072 Discret Event Dyn Syst FFH Reijnen 30 2 499 2020 10.1007/s10626-020-00314-0 Reijnen FFH, Goorden MA, van de Mortel-Fronczak JM, Rooda JE (2020) Modeling for supervisor synthesis – a lock-bridge combination case study. Discret Event Dyn Syst 30(2):499–532. https://doi.org/10.1007/s10626-020-00314-0 Roscoe AW (1994) Model-checking CSP. In: Roscoe AW (ed) A Classical Mind: Essays in Honour of C. A. R, Hoare. Prentice-Hall 10.1007/3-540-60630-0_7 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 ’95, volume 1019 of LNCS. Springer, pp 133–152. https://doi.org/10.1007/3-540-60630-0_7 IEEE Trans Autom Control K Rudie 37 11 1692 1992 10.1109/9.173140 Rudie K, Wonham W (1992) Think globally, act locally: Decentralized supervisory control. IEEE Trans Autom Control 37(11):1692–1708. https://doi.org/10.1109/9.173140 10.1109/WODES.2008.4605990 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 ’08. IEEE, pp 462–467. https://doi.org/10.1109/WODES.2008.4605990 IEEE Trans Autom Control K Schmidt 56 4 723 2011 10.1109/TAC.2010.2067250 Schmidt K, Breindl C (2011) Maximally permissive hierarchical control of decentralized discrete event systems. IEEE Trans Autom Control 56(4):723–737. https://doi.org/10.1109/TAC.2010.2067250 10.1109/WODES.2006.382509 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 ’06. IEEE, pp 413–418. https://doi.org/10.1109/WODES.2006.382509 IEEE Trans Autom Control R Su 55 7 1267 2010 10.1109/TAC.2010.2042342 Su R, van Schuppen JH, Rooda JE (2010) Aggregative synthesis of distributed supervisors based on automaton abstraction. IEEE Trans Autom Control 55(7):1267–1640. https://doi.org/10.1109/TAC.2010.2042342 IEEE Trans Autom Control R Su 55 11 2527 2010 10.1109/TAC.2010.2046931 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–2541. https://doi.org/10.1109/TAC.2010.2046931 Automatica R Su 46 6 968 2010 10.1016/j.automatica.2010.02.025 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–978. https://doi.org/10.1016/j.automatica.2010.02.025 Automatica S Takai 108 108470 2019 10.1016/j.automatica.2019.06.022 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 Tanenbaum AS (1992) Modern Operating Systems. Prentice-Hall Ware S (2007) Modular finite-state machine analysis. Honours project report, Dept. of Computer Science, University of Waikato Ware S (2014) On Conflicts in Concurrent Systems. Ph.D. thesis, Dept. of Computer Science, University of Waikato. http://hdl.handle.net/10289/8545 10.1109/WODES.2008.4605966 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 ’08. IEEE, pp 322–327. https://doi.org/10.1109/WODES.2008.4605966 Discret Event Dyn Syst S Ware 22 4 451 2012 10.1007/s10626-012-0133-3 Ware S, Malik R (2012) Conflict-preserving abstraction of discrete event systems using annotated automata. Discret Event Dyn Syst 22(4):451–477. https://doi.org/10.1007/s10626-012-0133-3 Int J Found Comput Sci S Ware 24 8 1183 2013 10.1142/S0129054113500287 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–1208. https://doi.org/10.1142/S0129054113500287 10.1007/978-3-319-05416-2_18 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–18. https://doi.org/10.1007/978-3-319-05416-2_18 Int J Control Y Willner 54 5 1143 1991 10.1080/00207179108934202 Willner Y, Heymann M (1991) Supervisory control of concurrent discrete-event systems. Int J Control 54(5):1143–1169. https://doi.org/10.1080/00207179108934202 Discret Event Dyn Syst KC Wong 6 3 241 1996 10.1007/BF01797154 Wong KC, Wonham WM (1996) Hierarchical control of discrete-event systems. Discret Event Dyn Syst 6(3):241–273. https://doi.org/10.1007/BF01797154 10.1007/978-1-4471-5102-9_54-1 Wonham WM (2013) Supervisory control of discrete-event systems. Systems Control Group, Dept. of Electrical Engineering, University of Toronto, ON, Canada Math Control Signals Syst WM Wonham 1 1 13 1988 10.1007/BF02551233 Wonham WM, Ramadge PJ (1988) Modular supervisory control of discrete event systems. Math Control Signals Syst 1(1):13–30. https://doi.org/10.1007/BF02551233 Yeh WJ, Young M (1993) Hierarchical tracing of concurrent programs. In: 3rd Irvine Software Symp., ISS ’93 10.1007/978-1-4757-6656-1_5 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–100. Kluwer, Dordrecht, the Netherlands. https://doi.org/10.1007/978-1-4757-6656-1_5 IEEE Trans Autom Control H Zhong 35 10 1125 1990 10.1109/9.58555 Zhong H, Wonham WM (1990) On the consistency of hierarchical supervision in discrete-event systems. IEEE Trans Autom Control 35(10):1125–1134. https://doi.org/10.1109/9.58555