{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:44:22Z","timestamp":1761648262873},"reference-count":31,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"2","license":[{"start":{"date-parts":[[2015,6,1]],"date-time":"2015-06-01T00:00:00Z","timestamp":1433116800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"Multiscale Systems Center (MuSyC)"},{"name":"Boeing Corporation"},{"name":"AFOSR Award","award":["FA9550-12-1-0302"],"award-info":[{"award-number":["FA9550-12-1-0302"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Control Netw. Syst."],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1109\/tcns.2015.2401174","type":"journal-article","created":{"date-parts":[[2015,2,6]],"date-time":"2015-02-06T19:55:53Z","timestamp":1423252553000},"page":"193-203","source":"Crossref","is-referenced-by-count":11,"title":["Specification and Synthesis of Reactive Protocols for Aircraft Electric Power Distribution"],"prefix":"10.1109","volume":"2","author":[{"given":"Huan","family":"Xu","sequence":"first","affiliation":[]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[]},{"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679387"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2011.6161470"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2011.22"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1142\/9789812797773_0023"},{"key":"ref16","author":"moir","year":"2001","journal-title":"Aircraft Systems Mechanical Electrical Avionics Subsystems Integration"},{"key":"ref17","article-title":"Electrical starting, generation, conversion and distribution system architecture for a more electric vehicle","author":"michalko","year":"2008"},{"key":"ref18","article-title":"Pentagon says F-35 fighter delayed, costs rise 4.3 percent","author":"shalal-esa","year":"2012","journal-title":"Chicago Tribune"},{"key":"ref19","article-title":"Dreamliner's slow flight","author":"creedy","year":"2013","journal-title":"The Australian"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0115-3"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6656-1_2"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1049\/cp.2010.0049"},{"key":"ref6","first-page":"364","article-title":"Synthesis of reactive (1) designs","author":"piterman","year":"2006","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_33"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.2514\/6.2011-1506"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","article-title":"Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends","author":"pnueli","year":"1986","journal-title":"Current Trends Concurrency"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2007.339624"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.4271\/2010-01-1804"},{"key":"ref9","author":"galton","year":"1987","journal-title":"Temporal Logics and Their Applications"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MAES.2007.340500"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref22","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2195811"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967747"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","article-title":"Jtlv: A framework for developing verification algorithms","author":"pnueli","year":"2010","journal-title":"Computer Aided Verification"}],"container-title":["IEEE Transactions on Control of Network Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6509490\/7127070\/07035090.pdf?arnumber=7035090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:47:19Z","timestamp":1642006039000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7035090\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6]]},"references-count":31,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.1109\/tcns.2015.2401174","relation":{},"ISSN":["2325-5870"],"issn-type":[{"value":"2325-5870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6]]}}}