{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T23:24:30Z","timestamp":1781565870952,"version":"3.54.5"},"reference-count":21,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.202.5","type":"journal-article","created":{"date-parts":[[2016,2,1]],"date-time":"2016-02-01T23:24:58Z","timestamp":1454369098000},"page":"58-72","source":"Crossref","is-referenced-by-count":27,"title":["Synthesizing a Lego Forklift Controller in GR(1): A Case Study"],"prefix":"10.4204","volume":"202","author":[{"given":"Shahar","family":"Maoz","sequence":"first","affiliation":[{"name":"Tel Aviv University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan Oliver","family":"Ringert","sequence":"additional","affiliation":[{"name":"Tel Aviv University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2720","published-online":{"date-parts":[[2016,2,2]]},"reference":[{"key":"AlurMT13","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/FMCAD.2013.6679387","article-title":"Counter-strategy guided refinement of GR(1) temporal logic specifications","volume-title":"Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013","author":"Alur","year":"2013"},{"key":"BloemJK14","series-title":"EPTCS","doi-asserted-by":"publisher","first-page":"68","DOI":"10.4204\/EPTCS.157.9","article-title":"Parameterized Synthesis Case Study: AMBA AHB","volume-title":"Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23-24, 2014.","volume":"157","author":"Bloem","year":"2014"},{"issue":"3","key":"BJP+12","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","article-title":"Synthesis of Reactive(1) Designs","volume":"78","author":"Bloem","year":"2012","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"DIppolitoBPU13","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430543","article-title":"Synthesizing nonanomalous event-based controllers for liveness goals","volume":"22","author":"D'Ippolito","year":"2013","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"DAC99","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/302405.302672","article-title":"Patterns in Property Specifications for Finite-State Verification","volume-title":"ICSE","author":"Dwyer","year":"1999"},{"key":"EhlersT14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/2562059.2562128","article-title":"Resilience to intermittent assumption violations in reactive synthesis","volume-title":"17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, Berlin, Germany, April 15-17, 2014","author":"Ehlers","year":"2014"},{"key":"GodhalCH13","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10009-011-0207-9","article-title":"Synthesis of AMBA AHB from formal specification: a case study","volume":"15","author":"Godhal","year":"2013","journal-title":"STTT"},{"key":"KleinP10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-19583-9_16","article-title":"Revisiting Synthesis of GR(1) Specifications","volume-title":"Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers","volume":"6504","author":"Klein","year":"2010"},{"key":"KonighoferHB13","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/s10009-011-0221-y","article-title":"Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies","volume":"15","author":"K\u00f6nighofer","year":"2013","journal-title":"STTT"},{"key":"Kress-GazitFP07","doi-asserted-by":"publisher","first-page":"3116","DOI":"10.1109\/ROBOT.2007.363946","article-title":"Where's Waldo? Sensor-Based Temporal Logic Motion Planning","volume-title":"2007 IEEE International Conference on Robotics and Automation, ICRA 2007, 10-14 April 2007, Roma, Italy","author":"Kress-Gazit","year":"2007"},{"issue":"6","key":"Kress-GazitFP09","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","article-title":"Temporal-Logic-Based Reactive Mission and Motion Planning","volume":"25","author":"Kress-Gazit","year":"2009","journal-title":"IEEE Trans. Robotics"},{"key":"MR15patterns","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1145\/2786805.2786824","article-title":"GR(1) Synthesis for LTL Specification Patterns","volume-title":"ESEC\/FSE","author":"Maoz","year":"2015"},{"key":"MaozS11","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1960275.1960280","article-title":"AspectLTL: an aspect language for LTL specifications","volume-title":"AOSD","author":"Maoz","year":"2011"},{"key":"MaozS12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-33666-9_22","article-title":"Assume-Guarantee Scenarios: Semantics and Synthesis","volume-title":"MODELS","volume":"7590","author":"Maoz","year":"2012"},{"key":"MaozS13","first-page":"242","article-title":"Counter play-out: executing unrealizable scenario-based specifications","volume-title":"ICSE","author":"Maoz","year":"2013"},{"key":"MaozS13AOSD","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-36964-3_2","article-title":"Two-Way Traceability and Conflict Debugging for AspectLTL Programs","volume":"10","author":"Maoz","year":"2013","journal-title":"T. Aspect-Oriented Software Development"},{"key":"PitermanPS06","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","article-title":"Synthesis of Reactive(1) Designs","volume-title":"VMCAI","volume":"3855","author":"Piterman","year":"2006"},{"key":"PR89","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/75277.75293","article-title":"On the Synthesis of a Reactive Module","volume-title":"POPL","author":"Pnueli","year":"1989"},{"key":"PnueliSZ10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","article-title":"JTLV: A Framework for Developing Verification Algorithms","volume-title":"CAV","volume":"6174","author":"Pnueli","year":"2010"},{"key":"RamanPK13","doi-asserted-by":"publisher","first-page":"4075","DOI":"10.1109\/ICRA.2013.6631152","article-title":"Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations","volume-title":"2013 IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, May 6-10, 2013","author":"Raman","year":"2013"},{"key":"RRW14","series-title":"Aachener Informatik-Berichte, Software Engineering","volume-title":"Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton","volume":"20","author":"Ringert","year":"2014"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2016,2,5]],"date-time":"2016-02-05T01:03:09Z","timestamp":1454634189000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/arxiv.org\/abs\/1602.01172"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,2]]},"references-count":21,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.4204\/eptcs.202.5","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,2]]}}}