{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:57:15Z","timestamp":1779087435221,"version":"3.51.4"},"reference-count":46,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2015,7,1]],"date-time":"2015-07-01T00:00:00Z","timestamp":1435708800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Sci. Eng."],"published-print":{"date-parts":[[2015,7]]},"DOI":"10.1109\/tase.2014.2369858","type":"journal-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T20:28:43Z","timestamp":1419020923000},"page":"990-1006","source":"Crossref","is-referenced-by-count":17,"title":["A BDD-Based Approach for Designing Maximally Permissive Deadlock Avoidance Policies for Complex Resource Allocation Systems"],"prefix":"10.1109","volume":"12","author":[{"given":"Zhennan","family":"Fei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Spyros","family":"Reveliotis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sajed","family":"Miremadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Knut","family":"Akesson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/CASE.2011.6042469"},{"key":"ref38","author":"fei","year":"2014","journal-title":"Symbolic supervisory control of resource allocation systems"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2011.2167150"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.2060332"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2006.02.013"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.875030"},{"key":"ref37","author":"fei","year":"2014","journal-title":"Supplement for the paper entitled ?A BDD-based approach for designing maximally permissive deadlock avoidance policies for complex resource allocation systems?"},{"key":"ref36","first-page":"384","article-title":"Supremica?An integrated environment for verification, synthesis and simulation of discrete event systems","author":"\ufffdkesson","year":"2006","journal-title":"Proc 8th Int Workshop Discrete Event Syst"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2011.2146249"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2007.4434894"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-012-0139-x"},{"key":"ref40","first-page":"362","article-title":"A symbolic approach for maximally permissive deadlock avoidance in complex resource allocation systems","author":"fei","year":"2014","journal-title":"Proc Int Workshop Discrete Event Syst"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2012.2226034"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2010.2046111"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/9.956052"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2003.820576"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2230814"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1109\/TRA.2002.807555","article-title":"Design of a live and maximally permissive Petri net controller using the theory of regions","volume":"19","author":"ghaffari","year":"2003","journal-title":"IEEE Trans Robotics & Automation"},{"key":"ref28","first-page":"2789","article-title":"Symbolic synthesis of supervisory controllers","author":"hoffmann","year":"1992","journal-title":"Proc Amer Control Conf"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/70.544768"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/70.370500"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1080\/07408170008967423","article-title":"Conflict resolution in AGV systems","volume":"32","author":"reveliotis","year":"2000","journal-title":"IIE Trans"},{"key":"ref29","first-page":"419","article-title":"Symbolic synthesis and verification of hierarchical interface-based supervisory control","author":"song","year":"2006","journal-title":"Proc 8th Int Workshop Discrete Event Syst"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/70.585898"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2010.2098270"},{"key":"ref7","first-page":"64","article-title":"Resource-oriented Petri nets in deadlock avoidance of AGV systems","author":"wu","year":"2001","journal-title":"Proc ICRA"},{"key":"ref2","author":"zhou","year":"2004","journal-title":"Deadlock Resolution in Computer-Integrated Systems"},{"key":"ref9","first-page":"1231","article-title":"Monitor design for colored Petri nets: An application to deadlock prevention in railway networks","volume":"10","author":"giua","year":"2006","journal-title":"Control Eng Practice"},{"key":"ref1","author":"reveliotis","year":"2005","journal-title":"Real-Time Management of Resource Allocation Systems A Discrete Event Systems Approach"},{"key":"ref46","first-page":"286","article-title":"Maximally permissive deadlock avoidance for resource allocation systems with R\/W-locks","author":"nazeem","year":"2012","journal-title":"Proc WODES"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/3-540-65306-6_22","author":"badouel","year":"1998","journal-title":"In LNCS 1491Advances in Petri Nets Basic Models"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-014-0202-x"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2011.01.070"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/CASE.2011.6042440"},{"key":"ref42","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2011.2159112"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1201\/b16529-9"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2179422"},{"key":"ref44","year":"0","journal-title":"JavaBDD"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"ref43","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.2266793"}],"container-title":["IEEE Transactions on Automation Science and Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8856\/7161421\/06990639.pdf?arnumber=6990639","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:42:08Z","timestamp":1642005728000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6990639\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7]]},"references-count":46,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tase.2014.2369858","relation":{},"ISSN":["1545-5955","1558-3783"],"issn-type":[{"value":"1545-5955","type":"print"},{"value":"1558-3783","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7]]}}}