{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:23:04Z","timestamp":1762521784707,"version":"3.40.5"},"reference-count":41,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2015,12,1]],"date-time":"2015-12-01T00:00:00Z","timestamp":1448928000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1016\/j.scico.2015.05.010","type":"journal-article","created":{"date-parts":[[2015,6,6]],"date-time":"2015-06-06T00:23:06Z","timestamp":1433550186000},"page":"119-148","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":11,"special_numbering":"P2","title":["An algorithm for compositional nonblocking verification using special events"],"prefix":"10.1016","volume":"113","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6320-7269","authenticated-orcid":false,"given":"Colin","family":"Pilbrow","sequence":"first","affiliation":[]},{"given":"Robi","family":"Malik","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"year":"2008","series-title":"Introduction to Discrete Event Systems","author":"Cassandras","key":"10.1016\/j.scico.2015.05.010_br0010"},{"issue":"1","key":"10.1016\/j.scico.2015.05.010_br0020","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/5.21072","article-title":"The control of discrete event systems","volume":"77","author":"Ramadge","year":"1989","journal-title":"Proc. IEEE"},{"year":"2008","series-title":"Principles of Model Checking","author":"Baier","key":"10.1016\/j.scico.2015.05.010_br0030"},{"key":"10.1016\/j.scico.2015.05.010_br0040","series-title":"Proceedings of the 1990 Workshop on Computer-Aided Verification","first-page":"186","article-title":"Compositional minimization of finite state systems","volume":"vol. 531","author":"Graf","year":"1990"},{"key":"10.1016\/j.scico.2015.05.010_br0050","series-title":"Proceedings of the 18th International Conference on Application and Theory of Petri Nets","first-page":"29","article-title":"Compositionality in state space verification methods","volume":"vol. 1091","author":"Valmari","year":"1996"},{"key":"10.1016\/j.scico.2015.05.010_br0060","series-title":"Proceedings of the 5th IEEE Symposium on Logic in Computer Science","first-page":"353","article-title":"Compositional model checking","author":"Clarke","year":"1989"},{"key":"10.1016\/j.scico.2015.05.010_br0070","series-title":"Proceedings of IFIP WG2.1\/WG2.2\/WG2.3 Working Conference on Programming Concepts, Methods and Calculi","first-page":"573","article-title":"Abstract interpretation of reactive systems: abstractions preserving \u2200CTL\u204e, \u2203CTL\u204e and CTL\u204e","author":"Dams","year":"1994"},{"issue":"3","key":"10.1016\/j.scico.2015.05.010_br0080","doi-asserted-by":"crossref","first-page":"1914","DOI":"10.1137\/070695526","article-title":"Compositional verification in supervisory control","volume":"48","author":"Flordal","year":"2009","journal-title":"SIAM J. Control Optim."},{"issue":"4","key":"10.1016\/j.scico.2015.05.010_br0090","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1142\/S012905410600411X","article-title":"Conflicts and fair testing","volume":"17","author":"Malik","year":"2006","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"12","key":"10.1016\/j.scico.2015.05.010_br0100","doi-asserted-by":"crossref","first-page":"2803","DOI":"10.1109\/TAC.2009.2031730","article-title":"Verification of nonconflict of supervisors using abstractions","volume":"54","author":"Pena","year":"2009","journal-title":"IEEE Trans. Autom. Control"},{"issue":"6","key":"10.1016\/j.scico.2015.05.010_br0110","doi-asserted-by":"crossref","first-page":"968","DOI":"10.1016\/j.automatica.2010.02.025","article-title":"Nonconflict check by using sequential automaton abstractions based on weak observation equivalence","volume":"46","author":"Su","year":"2010","journal-title":"Automatica"},{"issue":"8","key":"10.1016\/j.scico.2015.05.010_br0120","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TAC.2013.2248255","article-title":"Compositional nonblocking verification using generalised nonblocking abstractions","volume":"58","author":"Malik","year":"2013","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"10.1016\/j.scico.2015.05.010_br0130","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s10626-012-0133-3","article-title":"Conflict-preserving abstraction of discrete event systems using annotated automata","volume":"22","author":"Ware","year":"2012","journal-title":"Discrete Event Dyn. Syst. Theory Appl."},{"issue":"8","key":"10.1016\/j.scico.2015.05.010_br0140","doi-asserted-by":"crossref","first-page":"1183","DOI":"10.1142\/S0129054113500287","article-title":"Compositional verification of the generalized nonblocking property using abstraction and canonical automata","volume":"24","author":"Ware","year":"2013","journal-title":"Int. J. Found. Comput. Sci."},{"key":"10.1016\/j.scico.2015.05.010_br0150","series-title":"Proceedings of the 2nd International Workshop on Formal Techniques for Safety-Critical Systems","first-page":"147","article-title":"Compositional nonblocking verification with always enabled events and selfloop-only events","author":"Pilbrow","year":"2013"},{"year":"1985","series-title":"Communicating Sequential Processes","author":"Hoare","key":"10.1016\/j.scico.2015.05.010_br0160"},{"issue":"1\u20132","key":"10.1016\/j.scico.2015.05.010_br0170","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"De Nicola","year":"1984","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10.1016\/j.scico.2015.05.010_br0180","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"Tarjan","year":"1972","journal-title":"SIAM J. Comput."},{"issue":"5","key":"10.1016\/j.scico.2015.05.010_br0190","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1109\/3477.875441","article-title":"On the complexity of supervisory control design in the RW framework","volume":"30","author":"Gohari","year":"2000","journal-title":"IEEE Trans. Syst. Man Cybern."},{"article-title":"Communication and Concurrency","year":"1989","author":"Milner","key":"10.1016\/j.scico.2015.05.010_br0200"},{"key":"10.1016\/j.scico.2015.05.010_br0210","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","article-title":"An implementation of an efficient algorithm for bisimulation equivalence","volume":"13","author":"Fernandez","year":"1990","journal-title":"Sci. Comput. Program."},{"year":"2010","series-title":"The language of certain conflicts of a nondeterministic process","author":"Malik","key":"10.1016\/j.scico.2015.05.010_br0220"},{"key":"10.1016\/j.scico.2015.05.010_br0230","article-title":"Efficient Transitive Closure Computation in Large Digraphs","volume":"vol. 74","author":"Nuutila","year":"1995"},{"issue":"3","key":"10.1016\/j.scico.2015.05.010_br0240","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1109\/TCST.2004.824795","article-title":"Incremental verification and synthesis of discrete-event systems guided by counter-examples","volume":"12","author":"Brandin","year":"2004","journal-title":"IEEE Trans. Control Syst. Technol."},{"issue":"4","key":"10.1016\/j.scico.2015.05.010_br0250","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/BF01933173","article-title":"Minimizing the number of transitions with respect to observation equivalence","volume":"31","author":"Eloranta","year":"1991","journal-title":"BIT"},{"key":"10.1016\/j.scico.2015.05.010_br0260","series-title":"Protocol Specification, Testing and Verification VII: Proceedings of IFIP WG6.1 7th International Conference on Protocol Specification, Testing and Verification","first-page":"165","article-title":"Fundamental results for the verification of observational equivalence: a survey","author":"Bolognesi","year":"1987"},{"key":"10.1016\/j.scico.2015.05.010_br0270","series-title":"Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing","first-page":"204","article-title":"Reverse observation equivalence between labelled state transition systems","author":"Wen","year":"2004"},{"key":"10.1016\/j.scico.2015.05.010_br0280","series-title":"Proceedings of the 8th International Workshop on Discrete Event Systems","first-page":"384","article-title":"Supremica\u2014an integrated environment for verification, synthesis and simulation of discrete event systems","author":"\u00c5kesson","year":"2006"},{"year":"2011","series-title":"An implementation of a compositional approach for verifying generalised nonblocking","author":"Francis","key":"10.1016\/j.scico.2015.05.010_br0300"},{"key":"10.1016\/j.scico.2015.05.010_br0310","series-title":"Proceedings of the 12th International Workshop on Discrete Event Systems","first-page":"376","article-title":"An algorithm for compositional nonblocking verification of extended finite-state machines","author":"Mohajerani","year":"2014"},{"key":"10.1016\/j.scico.2015.05.010_br0320","series-title":"Proceedings of Rensselaer's 4th International Conference on Computer Integrated Manufacturing and Automation Technology","first-page":"319","article-title":"The supervisory control of the automated manufacturing system of the AIP","author":"Brandin","year":"1994"},{"year":"2002","series-title":"Hierarchical interface-based supervisory control","author":"Leduc","key":"10.1016\/j.scico.2015.05.010_br0330"},{"year":"2006","series-title":"Symbolic synthesis and verification of hierarchical interface-based supervisory control","author":"Song","key":"10.1016\/j.scico.2015.05.010_br0340"},{"key":"10.1016\/j.scico.2015.05.010_br0350","doi-asserted-by":"crossref","first-page":"1152","DOI":"10.1007\/s00170-008-1555-9","article-title":"A structural approach to the non-blocking supervisory control of discrete-event systems","volume":"41","author":"Feng","year":"2009","journal-title":"Int. J. Adv. Manuf. Technol."},{"year":"1996","series-title":"Task description of a flexible production cell with real time properties","author":"L\u00f6tzbeyer","key":"10.1016\/j.scico.2015.05.010_br0360"},{"issue":"2","key":"10.1016\/j.scico.2015.05.010_br0370","first-page":"138","article-title":"A case study in verification of UML statecharts: the PROFIsafe protocol","volume":"9","author":"Malik","year":"2003","journal-title":"J. Univers. Comput. Sci."},{"year":"1996","series-title":"PLC implementation of a DES supervisor for a manufacturing testbed: an implementation perspective","author":"Leduc","key":"10.1016\/j.scico.2015.05.010_br0380"},{"key":"10.1016\/j.scico.2015.05.010_br0390","series-title":"Proceedings of the 29th Australasian Computer Science Conference","first-page":"257","article-title":"Interaction design for a mobile context-aware system using discrete event modelling","author":"Hinze","year":"2006"},{"key":"10.1016\/j.scico.2015.05.010_br0410","series-title":"Proceedings of the 3rd International Conference on Automation Science and Engineering","first-page":"1063","article-title":"Throughput analysis of linear cluster tools","author":"Yi","year":"2007"},{"issue":"1","key":"10.1016\/j.scico.2015.05.010_br0420","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1109\/TAC.2013.2283109","article-title":"A framework for compositional synthesis of modular nonblocking supervisors","volume":"59","author":"Mohajerani","year":"2014","journal-title":"IEEE Trans. Autom. Control"},{"key":"10.1016\/j.scico.2015.05.010_br0430","series-title":"Proceedings of the 30th ACM\/IEEE Design Automation Conference","first-page":"86","article-title":"Automatic functional test generation using the extended finite state machine model","author":"Cheng","year":"1993"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642315001136?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642315001136?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T14:36:06Z","timestamp":1575297366000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642315001136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12]]},"references-count":41,"alternative-id":["S0167642315001136"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2015.05.010","relation":{},"ISSN":["0167-6423"],"issn-type":[{"type":"print","value":"0167-6423"}],"subject":[],"published":{"date-parts":[[2015,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"An algorithm for compositional nonblocking verification using special events","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2015.05.010","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2015 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}