{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T11:57:57Z","timestamp":1694433477171},"reference-count":11,"publisher":"World Scientific Pub Co Pte Lt","issue":"08","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2013,12]]},"abstract":"<jats:p> This paper brings together two methods to compositionally verify the generalized non-blocking property, which is a weak liveness property to express the ability of concurrent systems to terminate under given preconditions. Appropriate notions of equivalence and refinement for the generalized nonblocking property are discussed, and abstraction rules to simplify finite-state automata accordingly are presented. The paper also presents a unique canonical automaton representation for all generalized nonblocking equivalent automata, which gives rise to more general means of abstraction and to effective decision procedures for generalized nonblocking equivalence. Experimental results demonstrate how abstraction rules and canonical automata can be combined to model-check large models of concurrent software. <\/jats:p>","DOI":"10.1142\/s0129054113500287","type":"journal-article","created":{"date-parts":[[2014,4,2]],"date-time":"2014-04-02T02:43:49Z","timestamp":1396406629000},"page":"1183-1208","source":"Crossref","is-referenced-by-count":3,"title":["COMPOSITIONAL VERIFICATION OF THE GENERALIZED NONBLOCKING PROPERTY USING ABSTRACTION AND CANONICAL AUTOMATA"],"prefix":"10.1142","volume":"24","author":[{"given":"SIMON","family":"WARE","sequence":"first","affiliation":[{"name":"Department of Computer Science, The University of Waikato, Private Bag 3105, Hamilton 3240, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ROBI","family":"MALIK","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Waikato, Private Bag 3105, Hamilton 3240, New Zealand"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2014,4]]},"reference":[{"key":"p_2","first-page":"313","volume":"962","author":"Brinksma E.","year":"1995","journal-title":"I. Lee and S. A. Smolka LNCS"},{"key":"p_3","first-page":"97","volume":"154","author":"Brookes S. D.","year":"1983","journal-title":"LNCS"},{"key":"p_4","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"p_7","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"p_9","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289519"},{"key":"p_11","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90071-K"},{"key":"p_12","doi-asserted-by":"publisher","DOI":"10.1137\/070695526"},{"key":"p_23","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2248255"},{"key":"p_24","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410600411X"},{"key":"p_28","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"p_29","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2010.02.025"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054113500287","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T13:48:18Z","timestamp":1565185698000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054113500287"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12]]},"references-count":11,"journal-issue":{"issue":"08","published-online":{"date-parts":[[2014,4]]},"published-print":{"date-parts":[[2013,12]]}},"alternative-id":["10.1142\/S0129054113500287"],"URL":"https:\/\/doi.org\/10.1142\/s0129054113500287","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12]]}}}