{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T13:49:47Z","timestamp":1787320187683,"version":"build-2736575974"},"reference-count":30,"publisher":"Society for Industrial & Applied Mathematics (SIAM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIAM J. Control Optim."],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>This paper proposes a compositional approach to verifying whether a large discrete event system is nonblocking. The new approach avoids computing the synchronous product of a large set of finite-state machines. Instead, the synchronous product is computed gradually, and intermediate results are simplified using conflict-preserving abstractions based on process-algebraic results about fair testing. Heuristics are used to choose between different possible abstractions. By translating the problem representation, the same method can also be applied to verify safety properties, in particular, controllability. Experimental results show that the method is applicable to finite-state machine models of industrial scale and brings considerable improvements in performance over other methods for nonblocking verification.<\/jats:p>","DOI":"10.1137\/070695526","type":"journal-article","created":{"date-parts":[[2009,6,3]],"date-time":"2009-06-03T18:07:36Z","timestamp":1244052456000},"page":"1914-1938","source":"Crossref","is-referenced-by-count":61,"title":["Compositional Verification in Supervisory Control"],"prefix":"10.1137","volume":"48","author":[{"given":"Hugo","family":"Flordal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robi","family":"Malik","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"351","published-online":{"date-parts":[[2009,6,3]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","unstructured":"K. \u00c5kesson, H. Flordal, and M. Fabian,\n                      Exploiting modularity for synthesis and verification of supervisors\n                      , in Proceedings of the 15th IFAC World Congress, Barcelona, Spain, 2002.","DOI":"10.3182\/20020721-6-ES-1901.00517"},{"key":"R2","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2004.824795"},{"key":"R3","doi-asserted-by":"crossref","unstructured":"E. Brinksma, A. Rensink, and W. Vogler,\n                      Fair testing\n                      , in Proceedings of the 6th International Conference on Concurrency Theory, CONCUR '95, Philadelphia, I. Lee and S. A. Smolka, eds., Lecture Notes in Comput. Sci. 962, Springer, Berlin, 1995, pp. 313\u2013327.","DOI":"10.1007\/3-540-60218-6_23"},{"key":"R4","doi-asserted-by":"crossref","unstructured":"C. G. Cassandras and S. Lafortune,\n                      Introduction to Discrete Event Systems\n                      , Kluwer Academic Publishers, Boston, 1999.","DOI":"10.1007\/978-1-4757-4070-7"},{"key":"R5","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan,\n                      Compositional model checking\n                      , in Proceedings of the Fourth Annual Symposium on Logic in Computer Science, IEEE, Piscataway, NJ, 1989, pp. 353\u2013362.","DOI":"10.1109\/LICS.1989.39190"},{"key":"R6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"R7","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933173"},{"key":"R8","doi-asserted-by":"crossref","unstructured":"M. Fabian and B. Lennartson,\n                      On non-deterministic supervisory control\n                      , in Proceedings of the 35th IEEE Conference on Decision and Control, Kobe, Japan, 1996, pp. 2213\u20132218.","DOI":"10.1109\/CDC.1996.572970"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"H. Flordal and R. Malik,\n                      Modular nonblocking verification using conflict equivalence\n                      , in Proceedings of the 8th International Workshop on Discrete Event Systems, WODES '06, Ann Arbor, MI, 2006, pp. 100\u2013106.","DOI":"10.1109\/WODES.2006.1678415"},{"key":"R10","doi-asserted-by":"crossref","unstructured":"H. Flordal and R. Malik,\n                      Supervision equivalence\n                      , in Proceedings of the 8th International Workshop on Discrete Event Systems, WODES '06, Ann Arbor, MI, 2006, pp. 155\u2013160.","DOI":"10.1109\/WODES.2006.1678424"},{"key":"R11","unstructured":"C. A. R. Hoare,\n                      Communicating Sequential Processes\n                      , Prentice Hall Internat. Ser. Comput. Sci., Prentice\u2013Hall, Englewood Cliffs, NJ, 1985."},{"key":"R12","unstructured":"R. J. Leduc,\n                      Hierarchical Interface-Based Supervisory Control\n                      , Ph.D. thesis, Department of Electrical and Computer Engineering, University of Toronto, Toronto, ON, Canada, 2002."},{"key":"R13","doi-asserted-by":"publisher","DOI":"10.1109\/9.61009"},{"key":"R14","unstructured":"A. L\u00f6tzbeyer and R. M\u00fchlfeld,\n                      Task Description of a Flexible Production Cell with Real Time Properties\n                      , Technical report, Forschungszentrum Informatik, Karlsruhe, Germany, 1996."},{"key":"R15","unstructured":"P. Malik,\n                      From Supervisory Control to Nonblocking Controllers for Discrete Event Systems\n                      , Ph.D. thesis, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, 2003."},{"key":"R16","unstructured":"R. Malik,\n                      On the set of certain conflicts of a given language\n                      , in Proceedings of the 7th International Workshop on Discrete Event Systems, WODES '04, Reims, France, 2004, pp. 277\u2013282."},{"key":"R17","doi-asserted-by":"crossref","unstructured":"R. Malik and H. Flordal,\n                      Yet another approach to compositional synthesis of discrete event systems\n                      , in Proceedings of the 9th International Workshop on Discrete Event Systems, WODES '08, G\u00f6teborg, Sweden, 2008, pp. 16\u201321.","DOI":"10.1109\/WODES.2008.4605916"},{"key":"R18","unstructured":"R. Malik, H. Flordal, and P. N. Pena,\n                      Conflicts and observers\n                      , in Proceedings of the 1st IFAC Workshop on Dependable Control of Discrete Event Systems, Paris, France, 2007, pp. 63\u201368."},{"key":"R19","doi-asserted-by":"crossref","unstructured":"R. Malik, D. Streader, and S. Reeves,\n                      Fair testing revisited: A process-algebraic characterization of conflicts\n                      , in Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, 2004, Lecture Notes in Comput. Sci. 3299, Springer, Berlin, 2004, pp. 120\u2013134.","DOI":"10.1007\/978-3-540-30476-0_14"},{"key":"R20","unstructured":"R. Milner,\n                      Communication and Concurrency\n                      , Prentice Hall Internat. Ser. Comput. Sci., Prentice\u2013Hall, Englewood Cliffs, NJ, 1989."},{"key":"R21","doi-asserted-by":"crossref","unstructured":"J. O. Moody and P. J. Antsaklis,\n                      Supervisory Control of Discrete Event Systems Using Petri Nets\n                      , Kluwer Academic Publishers, Boston, 1998.","DOI":"10.1007\/978-1-4615-5711-1"},{"key":"R22","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"R23","doi-asserted-by":"crossref","unstructured":"P. N. Pena, J. E. R. Cury, and S. Lafortune,\n                      Testing modularity of local supervisors: An approach based on abstractions\n                      , in Proceedings of the 8th International Workshop on Discrete Event Systems, WODES '06, Ann Arbor, MI, 2006, pp. 107\u2013112.","DOI":"10.1109\/WODES.2006.1678416"},{"key":"R24","doi-asserted-by":"crossref","unstructured":"M. H. d. Queiroz and J. E. R. Cury,\n                      Modular control of composed systems\n                      , in Proceedings of the 2003 American Control Conference, 2000, pp. 4051\u20134055.","DOI":"10.1109\/ACC.2000.876983"},{"key":"R25","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-005-4058-y"},{"key":"R26","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"R27","unstructured":"Supremica,\n                      www.supremica.org. The official website for the Supremica project\n                      , 2006."},{"key":"R28","doi-asserted-by":"crossref","unstructured":"S. Ware and R. Malik,\n                      The use of language projection for compositional verification of discrete event systems\n                      , in Proceedings of the 9th International Workshop on Discrete Event Systems, WODES '08, G\u00f6teborg, Sweden, 2008, pp. 322\u2013327.","DOI":"10.1109\/WODES.2008.4605966"},{"key":"R29","unstructured":"S. Westin,\n                      Fast Decision of Strong Bisimulation Equivalence Using Partition Refinement\n                      , licentiate thesis, Department of Computer Sciences, Chalmers University of Technology, G\u00f6teborg, Sweden, 1989."},{"key":"R30","unstructured":"W. M. Wonham,\n                      Supervisory Control of Discrete Event Systems\n                      , Technical report, Department of Electrical and Computer Engineering, University of Toronto, Toronto, ON, Canada, 2008."}],"container-title":["SIAM Journal on Control and Optimization"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/070695526","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T12:55:49Z","timestamp":1787316949000},"score":1,"resource":{"primary":{"URL":"https:\/\/epubs.siam.org\/doi\/10.1137\/070695526"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1137\/070695526"],"URL":"https:\/\/doi.org\/10.1137\/070695526","relation":{},"ISSN":["0363-0129","1095-7138"],"issn-type":[{"value":"0363-0129","type":"print"},{"value":"1095-7138","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]}}}