{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:49:37Z","timestamp":1761598177038},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,2,26]],"date-time":"2020-02-26T00:00:00Z","timestamp":1582675200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,2,26]],"date-time":"2020-02-26T00:00:00Z","timestamp":1582675200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s10626-019-00305-w","type":"journal-article","created":{"date-parts":[[2020,2,26]],"date-time":"2020-02-26T09:03:02Z","timestamp":1582707782000},"page":"301-334","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["On the computation of counterexamples in compositional nonblocking verification"],"prefix":"10.1007","volume":"30","author":[{"given":"Robi","family":"Malik","sequence":"first","affiliation":[]},{"given":"Simon","family":"Ware","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,2,26]]},"reference":[{"key":"305_CR1","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, DOI https:\/\/doi.org\/10.1109\/WODES.2006.382401","DOI":"10.1109\/WODES.2006.382401"},{"key":"305_CR2","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"},{"key":"305_CR3","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":"2nd edn."},{"key":"305_CR4","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, DOI https:\/\/doi.org\/10.1109\/LICS.1989.39190","DOI":"10.1109\/LICS.1989.39190"},{"key":"305_CR5","unstructured":"Dams D, Grumberg O, Gerth R (1994) Abstract interpretation of reactive systems: abstractions preserving \u2200CTL\u2217, \u2203CTL\u2217 and CTL\u2217. In: Olderog ER (ed) IFIP WG2.1\/WG2.2\/WG2.3 working conf. programming concepts, methods and calculi (PROCOMET), IFIP transactions. Elsevier, pp 573\u2013592"},{"issue":"1\u20132","key":"305_CR6","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. Theoret Comput Sci 34(1\u20132):83\u2013133. https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0","journal-title":"Theoret Comput Sci"},{"issue":"3","key":"305_CR7","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"},{"key":"305_CR8","doi-asserted-by":"publisher","unstructured":"Graf S, Steffen B (1990) Compositional minimization of finite state systems. In: 1990 workshop on computer- aided verification, LNCS, vol 531. Springer, pp 186\u2013196, DOI https:\/\/doi.org\/10.1007\/BFb0023732","DOI":"10.1007\/BFb0023732"},{"issue":"2","key":"305_CR9","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"PE Hart","year":"1968","unstructured":"Hart PE, Nilsson NJ, Raphael B (1968) A formal basis for the heuristic determination of minimum cost paths. IEEE Trans Syst Sci Cybern 4(2):100\u2013107. https:\/\/doi.org\/10.1109\/TSSC.1968.300136","journal-title":"IEEE Trans Syst Sci Cybern"},{"key":"305_CR10","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"305_CR11","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"},{"key":"305_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in computer science","author":"M Huth","year":"2004","unstructured":"Huth M, Ryan M (2004) Logic in computer science. Cambridge University Press, Cambridge"},{"key":"305_CR13","volume-title":"The set of certain conflicts. Honours project report","author":"J Lindsey","year":"2012","unstructured":"Lindsey J (2012) The set of certain conflicts. Honours project report. University of Waikato, Dept. of Computer Science"},{"key":"305_CR14","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":"305_CR15","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, DOI https:\/\/doi.org\/10.1109\/WODES.2016.7497885","DOI":"10.1109\/WODES.2016.7497885"},{"issue":"8","key":"305_CR16","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":"7","key":"305_CR17","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.ifacol.2018.06.334","volume":"51","author":"R Malik","year":"2018","unstructured":"Malik R, Ware S (2018) Counterexample computation in compositional nonblocking verification. IFAC PapersOnLine 51(7):230\u2013235. https:\/\/doi.org\/10.1016\/j.ifacol.2018.06.334","journal-title":"IFAC PapersOnLine"},{"issue":"4","key":"305_CR18","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"},{"key":"305_CR19","unstructured":"Milner R (1989) Communication and concurrency. Series in computer science. Prentice-Hall"},{"issue":"12","key":"305_CR20","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"},{"issue":"2","key":"305_CR21","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 Programming 113(2):119\u2013148. https:\/\/doi.org\/10.1016\/j.scico.2015.05.010","journal-title":"Sci Comput Programming"},{"issue":"1","key":"305_CR22","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":"6","key":"305_CR23","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":"305_CR24","doi-asserted-by":"publisher","unstructured":"Valmari A (1996) Compositionality in state space verification methods. In: 18th Int. conf. application and theory of Petri nets, LNCS, vol 1091. Springer, pp 29\u201356, DOI https:\/\/doi.org\/10.1007\/3-540-61363-3_3","DOI":"10.1007\/3-540-61363-3_3"},{"key":"305_CR25","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, DOI https:\/\/doi.org\/10.1109\/WODES.2008.4605966","DOI":"10.1109\/WODES.2008.4605966"},{"issue":"4","key":"305_CR26","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. Discrete Event Dyn Syst 22(4):451\u2013477. https:\/\/doi.org\/10.1007\/s10626-012-0133-3","journal-title":"Discrete Event Dyn Syst"},{"issue":"8","key":"305_CR27","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"},{"issue":"A","key":"305_CR28","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.scico.2013.09.006","volume":"89","author":"S Ware","year":"2014","unstructured":"Ware S, Malik R (2014) An algorithm to test the conflict preorder. Sci Comput Programming 89(A):23\u201340. https:\/\/doi.org\/10.1016\/j.scico.2013.09.006","journal-title":"Sci Comput Programming"},{"key":"305_CR29","unstructured":"Wirth N (1986) Algorithms and data structures. Prentice-Hall"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-019-00305-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-019-00305-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-019-00305-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,25]],"date-time":"2021-02-25T00:30:46Z","timestamp":1614213046000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-019-00305-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,26]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["305"],"URL":"https:\/\/doi.org\/10.1007\/s10626-019-00305-w","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,26]]},"assertion":[{"value":"6 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 December 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}