{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:10:01Z","timestamp":1746177001816,"version":"3.40.4"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319054155"},{"type":"electronic","value":"9783319054162"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05416-2_11","type":"book-chapter","created":{"date-parts":[[2014,4,5]],"date-time":"2014-04-05T05:41:09Z","timestamp":1396676469000},"page":"160-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Nonblocking Verification with Always Enabled Events and Selfloop-Only Events"],"prefix":"10.1007","author":[{"given":"Colin","family":"Pilbrow","sequence":"first","affiliation":[]},{"given":"Robi","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,6]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"\u00c5kesson, K., Fabian, M., Flordal, H., Malik, R.: 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, Ann Arbor, MI, USA, pp. 384\u2013385 (2006)","DOI":"10.1109\/WODES.2006.382401"},{"key":"11_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Brandin, B., Charbonnier, F.: The supervisory control of the automated manufacturing system of the AIP. In: Proceedings of Rensselaer\u2019s 4th International Conference on Computer Integrated Manufacturing and Automation Technology, Troy, NY, USA, pp. 319\u2013324 (1994)","DOI":"10.1109\/CIMAT.1994.389054"},{"issue":"3","key":"11_CR4","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1109\/TCST.2004.824795","volume":"12","author":"BA Brandin","year":"2004","unstructured":"Brandin, B.A., Malik, R., Malik, P.: Incremental verification and synthesis of discrete-event systems guided by counter-examples. IEEE Trans. Control Syst. Technol. 12(3), 387\u2013401 (2004)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"11_CR5","series-title":"LNCS","first-page":"97","volume-title":"ICALP 1983","author":"SD Brookes","year":"1983","unstructured":"Brookes, S.D., Rounds, W.C.: Behavioural equivalence relations induced by programming logics. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 97\u2013108. Springer, Heidelberg (1983)"},{"key":"11_CR6","volume-title":"Introduction to Discrete Event Systems","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S. (eds.): Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2008)","edition":"2"},{"issue":"1\u20132","key":"11_CR7","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, M.C.B.: Testing equivalences for processes. Theor. Comput. Sci. 34(1\u20132), 83\u2013133 (1984)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"11_CR8","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BF01933173","volume":"31","author":"J Eloranta","year":"1991","unstructured":"Eloranta, J.: Minimizing the number of transitions with respect to observation equivalence. BIT 31(4), 397\u2013419 (1991)","journal-title":"BIT"},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"1914","DOI":"10.1137\/070695526","volume":"48","author":"H Flordal","year":"2009","unstructured":"Flordal, H., Malik, R.: Compositional verification in supervisory control. SIAM J. Control Optim. 48(3), 1914\u20131938 (2009)","journal-title":"SIAM J. Control Optim."},{"key":"11_CR10","series-title":"LNCS","first-page":"186","volume-title":"CAV 1990","author":"S Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186\u20136. Springer, Heidelberg (1991)"},{"key":"11_CR11","unstructured":"Hinze, A., Malik, P., Malik, R.: Interaction design for a mobile context-aware system using discrete event modelling. In: Proceedings of the 29th Australasian Computer Science Conference, ACSC \u201906, pp. 257\u2013266. Australian Computer Society, Hobart (2006)"},{"key":"11_CR12","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"11_CR13","unstructured":"Leduc, R.J.: PLC implementation of a DES supervisor for a manufacturing testbed: an implementation perspective. Master\u2019s thesis. Department of Electrical Engineering, University of Toronto, ON, Canada. http:\/\/www.cas.mcmaster.ca\/~leduc (1996)"},{"key":"11_CR14","unstructured":"Leduc, R.J.: Hierarchical interface-based supervisory control. Ph.D. thesis, Department of Electrical Engineering, University of Toronto, ON, Canada. http:\/\/www.cas.mcmaster.ca\/~leduc (2002)"},{"issue":"2","key":"11_CR15","first-page":"138","volume":"9","author":"R Malik","year":"2003","unstructured":"Malik, R., M\u00fchlfeld, R.: A case study in verification of UML statecharts: the PROFIsafe protocol. J. Univ. Comput. Sci. 9(2), 138\u2013151 (2003)","journal-title":"J. Univ. Comput. Sci."},{"key":"11_CR16","unstructured":"Malik, R.: The language of certain conflicts of a nondeterministic process. Working Paper 05\/2010, Department of Computer Science, University of Waikato, Hamilton, New Zealand. http:\/\/hdl.handle.net\/10289\/4108 (2010)"},{"issue":"8","key":"11_CR17","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.: Compositional nonblocking verification using generalised nonblocking abstractions. IEEE Trans. Autom. Control 58(8), 1\u201313 (2013)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"11_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.: Conflicts and fair testing. Int. J. Found. Comput. Sci. 17(4), 797\u2013813 (2006)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"11_CR19","series-title":"Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Series in Computer Science. Prentice-Hall, Upper Saddle River (1989)"},{"issue":"12","key":"11_CR20","doi-asserted-by":"publisher","first-page":"2803","DOI":"10.1109\/TAC.2009.2031730","volume":"54","author":"PN Pena","year":"2009","unstructured":"Pena, P.N., Cury, J.E.R., Lafortune, S.: Verification of nonconflict of supervisors using abstractions. IEEE Trans. Autom. Control 54(12), 2803\u20132815 (2009)","journal-title":"IEEE Trans. Autom. Control"},{"key":"11_CR21","unstructured":"Pilbrow, C.: Compositional nonblocking verification with always enabled and selfloop-only events. Working Paper 07\/2013, Department of Computer Science, University of Waikato, Hamilton, New Zealand. http:\/\/hdl.handle.net\/10289\/8187 (2013)"},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81\u201398 (1989)","journal-title":"Proc. IEEE"},{"key":"11_CR23","unstructured":"KorSys Project. http:\/\/www4.in.tum.de\/proj\/korsys\/"},{"key":"11_CR24","unstructured":"Song, R.: Symbolic synthesis and verification of hierarchical interface-based supervisory control. Master\u2019s thesis, Department of Computing and Software, McMaster University, Hamilton, ON, Canada. http:\/\/www.cas.mcmaster.ca\/~leduc (2006)"},{"issue":"6","key":"11_CR25","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, J.H., Rooda, J.E., Hofkamp, A.T.: Nonconflict check by using sequential automaton abstractions based on weak observation equivalence. Automatica 46(6), 968\u2013978 (2010)","journal-title":"Automatica"},{"key":"11_CR26","unstructured":"Supremica. http:\/\/www.supremica.org"},{"key":"11_CR27","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/3-540-61363-3_3","volume-title":"Application and Theory of Petri Nets 1996","author":"A Valmari","year":"1996","unstructured":"Valmari, A.: Compositionality in state space verification methods. In: Billington, J., Reisig, W. (eds.) Application and Theory of Petri Nets 1996. LNCS, vol. 1091, pp. 29\u201356. Springer, Heidelberg (1996)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Yi, J., Ding, S., Zhang, M.T., van der Meulen, P.: Throughput analysis of linear cluster tools. In: Proceedings of the 3rd International Conference on Automation Science and Engineering, CASE 2007, Scottsdale, AZ, USA, pp. 1063\u20131068 (2007)","DOI":"10.1109\/COASE.2007.4341849"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05416-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:46:59Z","timestamp":1746175619000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05416-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319054155","9783319054162"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05416-2_11","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"6 April 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}