{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:55:44Z","timestamp":1766451344846},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,9,12]],"date-time":"2015-09-12T00:00:00Z","timestamp":1442016000000},"content-version":"tdm","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":[[2016,3]]},"DOI":"10.1007\/s10626-015-0217-y","type":"journal-article","created":{"date-parts":[[2015,9,12]],"date-time":"2015-09-12T01:39:37Z","timestamp":1442021977000},"page":"33-84","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["A framework for compositional nonblocking verification of extended finite-state machines"],"prefix":"10.1007","volume":"26","author":[{"given":"Sahar","family":"Mohajerani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robi","family":"Malik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Fabian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,12]]},"reference":[{"key":"217_CR1","doi-asserted-by":"crossref","unstructured":"\u00c5kesson K, Fabian M, Flordal H, Malik R (2006) Supremica\u2014an integrated environment for verification, synthesis and simulation of discrete event systems. In: Proceedings of the 8th international workshop on discrete event systems, WODES\u201906. IEEE, Ann Arbor, pp 384\u2013385","DOI":"10.1109\/WODES.2006.382401"},{"key":"217_CR2","doi-asserted-by":"crossref","unstructured":"Aloul FA, Markov IL, Sakallah KA (2003) FORCE: A fast & easy-to-implement variable-ordering heuristic. In: Proceedings of the 13th ACM great lakes symposium on VLSI, pp. 116\u2013119. Washington, DC, USA","DOI":"10.1145\/764808.764839"},{"key":"217_CR3","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press"},{"issue":"3","key":"217_CR4","doi-asserted-by":"crossref","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\u2013318","journal-title":"ACM Comput Surv"},{"key":"217_CR5","doi-asserted-by":"crossref","unstructured":"Chen Y, Lin F (2000) Modeling of discrete event systems using finite state machines with parameters. In: Proceedings of 2000 IEEE international conference on control applications (CCA). Anchorage, Alaska, pp 941\u2013946","DOI":"10.1109\/CCA.2000.897591"},{"key":"217_CR6","doi-asserted-by":"crossref","unstructured":"Cheng KT, Krishnakumar AS (1993) Automatic functional test generation using the extended finite state machine model.. In: Proceedings of the 30th ACM\/IEEE design automation conference. doi: 10.1145\/157485.164585 , Dallas, pp 86\u201391","DOI":"10.1145\/157485.164585"},{"key":"217_CR7","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) Proceedings of IFIP WG2.1\/WG2.2\/WG2.3 working conference on programming concepts, methods and calculi (PROCOMET), IFIP transactions. Elsevier, Amsterdam, pp 573\u2013592"},{"key":"217_CR8","doi-asserted-by":"crossref","unstructured":"Fabian M, Fei Z, Miremadi S, Lennartson B, \u00c5kesson K (2014). In: Campos J, Seatzu C, Xie X (eds) Supervisory control of manufacturing systems using extended finite automata, CRC Press","DOI":"10.1201\/b16529-13"},{"issue":"3","key":"217_CR9","doi-asserted-by":"crossref","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. doi: 10.1137\/070695526","journal-title":"SIAM J Control Optim"},{"issue":"5","key":"217_CR10","doi-asserted-by":"crossref","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. doi: 10.1109\/3477.875441","journal-title":"IEEE Trans Syst Man Cybern"},{"key":"217_CR11","unstructured":"Graf S, Steffen B (1990) Compositional minimization of finite state systems. In: Proceedings of the 1990 workshop on computer-aided verification, LNCS, vol 531. Springer, NJ, pp 186\u2013196"},{"key":"217_CR12","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"217_CR13","doi-asserted-by":"crossref","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. University Press, Cambridge"},{"issue":"8","key":"217_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TAC.2013.2268919","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. doi: 10.1109\/TAC.2013.2248255","journal-title":"IEEE Trans Autom Control"},{"issue":"2","key":"217_CR15","first-page":"138","volume":"9","author":"R Malik","year":"2003","unstructured":"Malik R, M\u00fchlfeld R (2003) A case study in verification of UML statecharts: the PROFIsafe protocol. Journal of Universal Computer Science 9(2):138\u2013151","journal-title":"Journal of Universal Computer Science"},{"issue":"4","key":"217_CR16","doi-asserted-by":"crossref","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. doi: 10.1142\/S012905410600411X","journal-title":"Int J Found Comput Sci"},{"key":"217_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic Publishers, Boston"},{"key":"217_CR18","unstructured":"Milner R (1989) Communication and concurrency. Series in Computer Science. Prentice-Hall"},{"key":"217_CR19","doi-asserted-by":"crossref","unstructured":"Mohajerani S, Malik R, Fabian M (2013) Compositional nonblocking verification for extended finite-state automata using partial unfolding. In: Proceedings of the 9th international conference on automation science and engineering, CASE. Wisconsin Press, Madison, pp 942\u2013947","DOI":"10.1109\/CoASE.2013.6654014"},{"key":"217_CR20","volume-title":"Partial unfolding for compositional nonblocking verification of extended finite-state machines. Working Paper 01\/2013, Department of Computer Science, University of Waikato","author":"S Mohajerani","year":"2013","unstructured":"Mohajerani S, Malik R, Fabian M (2013) Partial unfolding for compositional nonblocking verification of extended finite-state machines. Working Paper 01\/2013, Department of Computer Science, University of Waikato. Hamilton, New Zealand. http:\/\/hdl.handle.net\/10289\/7140"},{"key":"217_CR21","doi-asserted-by":"crossref","unstructured":"Mohajerani S, Malik R, Fabian M (2014) An algorithm for compositional nonblocking verification of extended finite-state machines. In: Proceedings of the 12th international workshop on discrete event systems, WODES\u201914, pp. 376\u2013382. Paris, France","DOI":"10.3182\/20140514-3-FR-4046.00039"},{"key":"217_CR22","volume-title":"Implementation of a framework for restart after unforeseen errors in manufacturing systems. Master\u2019s thesis, Chalmers University of Technology","author":"S Parsaeian","year":"2014","unstructured":"Parsaeian S (2014) Implementation of a framework for restart after unforeseen errors in manufacturing systems. Master\u2019s thesis, Chalmers University of Technology. G\u00f6teborg, Sweden"},{"issue":"12","key":"217_CR23","doi-asserted-by":"crossref","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","journal-title":"IEEE Trans Autom Control"},{"issue":"1","key":"217_CR24","doi-asserted-by":"crossref","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","journal-title":"Proc IEEE"},{"key":"217_CR25","doi-asserted-by":"crossref","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, CDC \u201907, pp. 3387\u2013 3392","DOI":"10.1109\/CDC.2007.4434894"},{"issue":"6","key":"217_CR26","doi-asserted-by":"crossref","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. doi: 10.1016\/j.automatica.2010.02.025","journal-title":"Automatica"},{"key":"217_CR27","doi-asserted-by":"crossref","unstructured":"Teixeira M, Malik R, Cury JER, de Queiroz MH (2013) Variable abstraction and approximations in supervisory control synthesis. In: 2013 American Control Conference, pp. 120\u2013125. Washington, DC, USA","DOI":"10.1109\/ACC.2013.6579826"},{"key":"217_CR28","unstructured":"Vahidi A (2004) Efficient analysis of discrete event systems\u2014supervisor synthesis with binary decision diagrams. Ph.D. thesis. Chalmers University of Technology, G\u00f6teborg"},{"key":"217_CR29","unstructured":"Wonham WM Supervisory control of discrete-event systems. http:\/\/www.control.utoronto.edu\/"},{"issue":"1","key":"217_CR30","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1016\/j.sysconle.2011.10.010","volume":"61","author":"J Zhaoa","year":"2012","unstructured":"Zhaoa J, Chen YL, Chen Z, Lin F, Wang C, Zhang H (2012) Modeling and control of discrete event systems using finite state machines with variables and their applications in power grids. Syst Control Lett 61(1):212\u2013222","journal-title":"Syst Control Lett"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-015-0217-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-015-0217-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-015-0217-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,30]],"date-time":"2019-08-30T07:53:41Z","timestamp":1567151621000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-015-0217-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,12]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["217"],"URL":"https:\/\/doi.org\/10.1007\/s10626-015-0217-y","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,12]]}}}