{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T14:52:13Z","timestamp":1772549533516,"version":"3.50.1"},"reference-count":161,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. IEEE"],"published-print":{"date-parts":[[2018,9]]},"DOI":"10.1109\/jproc.2018.2834926","type":"journal-article","created":{"date-parts":[[2018,9,17]],"date-time":"2018-09-17T18:37:36Z","timestamp":1537209456000},"page":"1616-1654","source":"Crossref","is-referenced-by-count":8,"title":["Layering Assume-Guarantee Contracts for Hierarchical System Design"],"prefix":"10.1109","volume":"106","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4704-3334","authenticated-orcid":false,"given":"Ioannis","family":"Filippidis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5785-7481","authenticated-orcid":false,"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289062"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1984.10017"},{"key":"ref31","first-page":"67","article-title":"Checking a large routine","author":"turing","year":"1949","journal-title":"Report of a Conference on High Speed Automatic Calculating-Machines"},{"key":"ref30","volume":"1","author":"goldstine","year":"1947","journal-title":"Planning and Coding Problems for an Electronic Computing Instrument Report on the Mathematical and Logical Aspects of an Electronic Computing Instrument Part II"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289074"},{"key":"ref36","first-page":"179","article-title":"On the synthesis of a reactive module","author":"pnueli","year":"1989","journal-title":"Proc POPL"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1830-2"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume":"19","author":"floyd","year":"1967","journal-title":"Mathematical Aspects of Computer and Information Sciences"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2003.1203057"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0167-9260(94)00007-7"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/954092.954488"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"ref22","first-page":"1","article-title":"Synthesis of programs from temporal property specifications","author":"pnueli","year":"2009","journal-title":"Proc MEMOCODE"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1145\/2728606.2728626","article-title":"Estimator-based reactive synthesis under incomplete information","author":"ehlers","year":"2015","journal-title":"Proc HSCC"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref23","first-page":"746","article-title":"Distributed reactive systems are hard to synthesize","volume":"2","author":"pnueli","year":"1990","journal-title":"Proc FOCS"},{"key":"ref101","first-page":"185","article-title":"From logic to manuals again","volume":"144","author":"thimbleby","year":"1997","journal-title":"Proc Inst Elect Eng &#x2014 I"},{"key":"ref26","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref100","article-title":"Design approach for real-time reactive systems","author":"katara","year":"1999","journal-title":"Proceedings of the International Workshop on Real-time Constraints"},{"key":"ref25","first-page":"1","article-title":"Algorithmic verification of linear temporal logic specifications","author":"kesten","year":"1998","journal-title":"Proc ICALP"},{"key":"ref50","first-page":"342","article-title":"Circular compositional reasoning about liveness","author":"mcmillan","year":"1999","journal-title":"Proc CHARME"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"ref154","article-title":"A temporal logic of actions","author":"lamport","year":"1990"},{"key":"ref153","author":"kleene","year":"1971","journal-title":"Introduction to Metamathematics"},{"key":"ref156","first-page":"1030","article-title":"Control design for hybrid systems with TuLiP: The temporal logic planning toolbox","author":"filippidis","year":"2016","journal-title":"Proc IEEE Conf Control Appl (CCA)"},{"key":"ref155","volume":"34","author":"kunen","year":"2013","journal-title":"Set Theory"},{"key":"ref150","first-page":"42","article-title":"Dynamic variable ordering for ordered binary decision diagrams","author":"rudell","year":"1993","journal-title":"Proc ICCAD"},{"key":"ref152","year":"0"},{"key":"ref151","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07512-9"},{"key":"ref146","article-title":"Implicit prime cover computation: An overview","author":"coudert","year":"1993","journal-title":"Proc Synthesis Simulation Meeting Int Interchange"},{"key":"ref147","first-page":"625","article-title":"A new viewpoint on two-level logic minimization","author":"coudert","year":"1993","journal-title":"Proc Design Autom Conf (DAC)"},{"key":"ref148","first-page":"36","article-title":"Implicit and incremental computation of primes and essential primes of Boolean functions","author":"coudert","year":"1992","journal-title":"Proc Design Autom Conf (DAC)"},{"key":"ref149","first-page":"73","article-title":"A multi-paradigm language for reactive synthesis","author":"filippidis","year":"2015","journal-title":"Proc 4th Workshop on Synthesis (SYNT)"},{"key":"ref59","first-page":"21","article-title":"A property-based proof system for contract-based design","author":"cimatti","year":"2012","journal-title":"Proc EUROMICRO"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref57","first-page":"104","article-title":"Are interface theories equivalent to contract theories?","author":"nuzzo","year":"2014","journal-title":"Proc MEMOCODE"},{"key":"ref56","article-title":"Compositional design of cyber-physical systems using contracts","author":"nuzzo","year":"2015"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.18.217-238"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"},{"key":"ref53","article-title":"Contracts for systems design","author":"benveniste","year":"2012"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2993.357247"},{"key":"ref161","article-title":"An introduction to zero-suppressed binary decision diagrams","author":"mishchenko","year":"2014"},{"key":"ref160","first-page":"440","article-title":"You assume, we guarantee: Methodology and case studies","author":"henzinger","year":"1998","journal-title":"Proc CAV"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2007.4339280"},{"key":"ref3","first-page":"321","article-title":"Specification and design of (parallel) programs","author":"jones","year":"1983","journal-title":"Proc Inf Process"},{"key":"ref6","first-page":"166","article-title":"Verification of a multiplier: 64 bits and beyond","author":"kurshan","year":"1993","journal-title":"Proc Comput Aided Verification"},{"key":"ref5","first-page":"134","article-title":"Component and interface refinement in closed-system specifications","author":"kurki-suonio","year":"1999","journal-title":"Proc Formal Methods"},{"key":"ref8","author":"lamport","year":"1991","journal-title":"Miscellany TLA Mailing List"},{"key":"ref159","first-page":"1574","article-title":"Specification decomposition for synthesis from libraries of LTL Assume\/Guarantee contracts","author":"iannopollo","year":"2018","journal-title":"Proc DATE"},{"key":"ref7","first-page":"402","article-title":"Composition: A way to make proofs harder","author":"lamport","year":"1997","journal-title":"Compositionality The Significant Difference"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16042-6_21"},{"key":"ref157","doi-asserted-by":"publisher","DOI":"10.1007\/s11784-012-0071-6"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_3"},{"key":"ref158","first-page":"245","article-title":"Decomposing refinement proofs using assume-guarantee reasoning","author":"henzinger","year":"2000","journal-title":"Proc ICCAD"},{"key":"ref46","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S1474-6670(17)40546-5","article-title":"Modular verification of programmable logic controllers with TLA","volume":"31","author":"wolpers","year":"1998","journal-title":"Proc IFAC-INCOM"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6355-9_16"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61455-2_14"},{"key":"ref47","first-page":"81","article-title":"Open systems in TLA","author":"abadi","year":"1994","journal-title":"Proc PODC"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"ref43","first-page":"46","article-title":"The temporal logic of programs","author":"pnueli","year":"1977","journal-title":"Proc FOCS"},{"key":"ref127","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90168-H"},{"key":"ref126","first-page":"499","article-title":"An abstract account of composition","author":"abadi","year":"1995","journal-title":"Proc Int l Symp Mathematical Foundations of Computer Science"},{"key":"ref125","volume":"19","author":"kunen","year":"2012","journal-title":"Mathematical foundations"},{"key":"ref124","first-page":"782","article-title":"Symbolic construction of GR(1) contracts for systems with full information","author":"filippidis","year":"2016","journal-title":"Proc ACC"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0091-5"},{"key":"ref71","article-title":"The design of distributed systems: An introduction to FOCUS","author":"broy","year":"1992"},{"key":"ref129","first-page":"250","article-title":"Verification of open systems","author":"vardi","year":"1997","journal-title":"Proc FSTTCS"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60225-7_14"},{"key":"ref128","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_16"},{"key":"ref76","first-page":"1038","article-title":"Information flow in concurrent games","author":"de alfaro","year":"2003","journal-title":"Proc ICALP"},{"key":"ref77","first-page":"127","article-title":"Synthesis of asynchronous systems","author":"schewe","year":"2007","journal-title":"Proc of LOPSTR?93"},{"key":"ref130","doi-asserted-by":"publisher","DOI":"10.1145\/365559.365617"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"ref75","first-page":"458","article-title":"The control of synchronous systems","author":"de alfaro","year":"2000","journal-title":"Proc CONCUR"},{"key":"ref133","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"ref134","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00129-7"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9586-5_6"},{"key":"ref131","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref79","first-page":"321","article-title":"Uniform distributed synthesis","author":"finkbeiner","year":"2005","journal-title":"Proc LICS"},{"key":"ref132","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"ref136","article-title":"Decomposing formal specifications into assume-guarantee contracts for hierarchical system design","author":"filippidis","year":"2019"},{"key":"ref135","article-title":"Symbolic construction of GR(1) contracts for synchronous systems with full information","author":"filippidis","year":"2015"},{"key":"ref138","first-page":"258","article-title":"Anzu: A tool for property synthesis","author":"jobstmann","year":"2007","journal-title":"Proc CAV"},{"key":"ref137","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"ref60","first-page":"702","article-title":"Ocra: A tool for checking the refinement of temporal contracts","author":"cimatti","year":"2013","journal-title":"Proc ASE"},{"key":"ref139","first-page":"171","article-title":"JTLV: A framework for developing verification algorithms","author":"pnueli","year":"2010","journal-title":"Proc CAV"},{"key":"ref62","first-page":"1","article-title":"Library-based scalable refinement checking for contract-based design","author":"iannopollo","year":"2014","journal-title":"Proc DATE"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/2885752"},{"key":"ref63","first-page":"1","article-title":"Constrained synthesis from component libraries","author":"iannopollo","year":"2016","journal-title":"Formal Aspects of Component Software"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00069-2"},{"key":"ref65","first-page":"161","article-title":"Revisiting synthesis of GR(1) specifications","author":"klein","year":"2010","journal-title":"Proceedings of HVC"},{"key":"ref140","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-6155-2"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_3"},{"key":"ref141","author":"hachtel","year":"1996","journal-title":"Logic Synthesis and Verification Algorithms"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/1985342.1985345"},{"key":"ref142","doi-asserted-by":"publisher","DOI":"10.1109\/92.250190"},{"key":"ref68","first-page":"2:1","article-title":"Refinement calculus of reactive systems","author":"preoteasa","year":"2014","journal-title":"Proc EMSOFT"},{"key":"ref143","article-title":"Logic synthesis for VLSI design","author":"rudell","year":"1989"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934503"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2736348"},{"key":"ref144","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-2821-6"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/362575.362577"},{"key":"ref145","first-page":"641","article-title":"New ideas for solving covering problems","author":"coudert","year":"1995","journal-title":"Proc Design Autom Conf (DAC)"},{"key":"ref109","article-title":"TLA+2: A preliminary guide","author":"lamport","year":"2014"},{"key":"ref95","first-page":"104","article-title":"Local proofs for global safety properties","volume":"34","author":"cohen","year":"2009","journal-title":"Proceedings of FMSD"},{"key":"ref108","author":"ebbinghaus","year":"2007","journal-title":"Ernst Zermelo An Approach to His Life and Work"},{"key":"ref94","article-title":"Compositional reactive synthesis for multi-agent systems","author":"moarref","year":"2016"},{"key":"ref107","first-page":"32","article-title":"Rules for abstraction","author":"merz","year":"1997","journal-title":"Advances in Computing Science—"},{"key":"ref93","first-page":"3478","article-title":"Synthesizing cooperative reactive mission plans","author":"ehlers","year":"2015","journal-title":"Proc IROS"},{"key":"ref106","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"ref92","first-page":"501","article-title":"Pattern-based refinement of assume-guarantee specifications in reactive synthesis","author":"alur","year":"2015","journal-title":"Proc TACAS"},{"key":"ref105","first-page":"394","article-title":"Minimum satisfying assignments for SMT","author":"dillig","year":"2012","journal-title":"Proc CAV"},{"key":"ref91","first-page":"26","article-title":"Counter-strategy guided refinement of GR(1) temporal logic specifications","author":"alur","year":"2013","journal-title":"Proc FMCAD"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.157.12"},{"key":"ref90","first-page":"43","article-title":"Mining assumptions for synthesis","author":"li","year":"2011","journal-title":"Proc MEMOCODE"},{"key":"ref103","first-page":"303","article-title":"Improving robot controller transparency through autonomous policy explanation","author":"hayes","year":"2017","journal-title":"Human Robot Interaction"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1109\/JRA.1987.1087080"},{"key":"ref111","author":"leisenring","year":"1969","journal-title":"Mathematical Logic and Hilbert’s ?-Symbol"},{"key":"ref112","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"ref110","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86896-2"},{"key":"ref98","first-page":"4841","article-title":"Distributed power allocation for vehicle management systems","author":"ozay","year":"2011","journal-title":"Proc CDC"},{"key":"ref99","article-title":"Abstractions and logical layers in specifications of reactive systems","author":"mikkonen","year":"1999"},{"key":"ref96","first-page":"2408","article-title":"Integrating active sensing into reactive synthesis with temporal logic constraints under partial observations","author":"fu","year":"2015","journal-title":"Proc ACC"},{"key":"ref97","first-page":"2305","article-title":"Synthesis of correct-by-construction control protocols for hybrid systems using partial state information","author":"mickelin","year":"2014","journal-title":"Proc ACC"},{"key":"ref10","author":"lamport","year":"2002","journal-title":"Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers"},{"key":"ref11","first-page":"657","article-title":"What good is temporal logic?","author":"lamport","year":"1983","journal-title":"Proc Inf Process"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/69624.357207"},{"key":"ref13","article-title":"Modular synthesis of reactive systems","author":"rosner","year":"1991"},{"key":"ref14","first-page":"364","article-title":"Synthesis of Reactive(1) designs","author":"piterman","year":"2006","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"ref15","first-page":"275","article-title":"Faster solutions of Rabin and Streett games","author":"piterman","year":"2006","journal-title":"Proc LICS"},{"key":"ref118","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"ref82","first-page":"22","article-title":"Effective control synthesis for DES under partial observations","volume":"1","author":"lamouchi","year":"2000","journal-title":"Proc CDC"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_19"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.01.006"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0228-z"},{"key":"ref17","first-page":"219","article-title":"Predicate abstraction for reactive synthesis","author":"walker","year":"2014","journal-title":"Proc FMCAD"},{"key":"ref84","first-page":"261","article-title":"Assume-guarantee synthesis","author":"chatterjee","year":"2007","journal-title":"Proc TACAS"},{"key":"ref18","first-page":"531","article-title":"Safraless decision procedures","author":"kupferman","year":"2005","journal-title":"Proc FOCS"},{"key":"ref119","first-page":"1","article-title":"On the synthesis of strategies in infinite games","author":"thomas","year":"1995","journal-title":"Proc STACS"},{"key":"ref83","first-page":"4104","article-title":"Undecidable problems of decentralized observation and control","volume":"5","author":"tripakis","year":"2001","journal-title":"Proc CDC"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_14"},{"key":"ref114","first-page":"1","article-title":"Realizable and unrealizable specifications of reactive systems","author":"abadi","year":"1989","journal-title":"Proc ICALP"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.1145\/93385.93442"},{"key":"ref116","article-title":"Formalizing synthesis in TLA","author":"filippidis","year":"2016"},{"key":"ref80","first-page":"18","article-title":"Distributed synthesis for LTL fragments","author":"chatterjee","year":"2013","journal-title":"Proc FMCAD"},{"key":"ref115","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50403-6_28"},{"key":"ref120","first-page":"211","article-title":"Solution of Church’s problem: A tutorial","volume":"4","author":"thomas","year":"2008","journal-title":"New Perspectives on Games and Interaction"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0221-y"},{"key":"ref121","first-page":"226","article-title":"Program repair as a game","author":"jobstmann","year":"2005","journal-title":"Proc CAV"},{"key":"ref122","article-title":"Proof automation and type synthesis for set theory in the context of TLA","author":"vanzetto","year":"2014"},{"key":"ref123","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319317"},{"key":"ref85","first-page":"82","article-title":"Automating modular verification","author":"alur","year":"1999","journal-title":"Proc CONCUR"},{"key":"ref86","first-page":"331","article-title":"Learning assumptions for compositional verification","author":"cobleigh","year":"2003","journal-title":"Proc TACAS"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_15"},{"key":"ref88","first-page":"147","article-title":"Environment assumptions for synthesis","author":"chatterjee","year":"2008","journal-title":"Proc CONCUR"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/8466984\/08466991.pdf?arnumber=8466991","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T18:43:40Z","timestamp":1662057820000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8466991\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":161,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2018.2834926","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"value":"0018-9219","type":"print"},{"value":"1558-2256","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}