GR(1)*: GR(1) specifications extended withexistential guarantees

Alrajeh D Kramer J Russo A Uchitel S (2012) Learning from vacuously satisfiable scenario-based specifications. In: International conference on fundamental approaches to software engineering. Springer pp 377–393

Almagor S, 2017, Computer aided verification–29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part II, 353

Alexander IF, 2004, Scenarios, stories, use cases: through the systems development life-cycle, 1

Amram G, 2019, Formal methods–the next 30 years–third world congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings, 83, 10.1007/978-3-030-30942-8_7

Alur R Moarref S Topcu U(2013) Counter-strategy guided refinement of GR

(1) temporal logic specifications. In: Formal methods in computer-aided design FMCAD 2013 Portland OR USA October 20-23 2013. IEEE pp 26-33

AMBA AHB specification. http://www.arm.com/products/silicon-ip-system/embedded-system-design/amba-specifications

10.1016/j.jal.2008.10.002

10.1016/S0304-3975(96)00228-9

Bloem R, 2015, Automated technology for verification and analysis–13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015, Proceedings, 394

Bloem R Galler SJ Jobstmann B Piterman N Pnueli A Weiglhofer M (2007) Interactive presentation: automatic hardware synthesis from specifications: a case study. In: 2007 Design automation and test in Europe conference and exposition DATE 2007 Nice France April 16–20 2007 pp 1188–1193

Bloem R Jacobs S Khalimov A (2014) Parameterized synthesis case study: AMBA AHB. In: Chatterjee K Ehlers R Jha S (eds) Proceedings 3rd workshop on synthesis SYNT 2014 Vienna Austria July 23–24 2014 volume 157 of EPTCS pp 68–83

10.1016/j.jcss.2011.08.007

10.1109/TC.1986.1676819

Bloem R Schewe S Khalimov A (2017) CTL* synthesis via LTL synthesis. In: Proceedings sixth workshop on synthesis SYNT@CAV 2017 Heidelberg Germany 22nd July 2017 pp 4–22

Cavezza DG Alrajeh D (2017) Interpolation-based GR(1) assumptions refinement. In: TACAS volume 10205 of LNCS pp 281–297

Clarke EM Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logic of programs. Springer pp 52–71

Cimatti A Roveri M Schuppan V Tchaltsev A (2008) Diagnostic information for realizability. In: VMCAI volume 4905 of LNCS. Springer pp 52–67

Dwyer MB Avrunin GS Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE. ACM pp 411–420

10.1145/2430536.2430543

10.1145/4904.4999

Ehlers R (2011) Generalized Rabin(1) synthesis with applications to robust system synthesis. In: NASA formal methods volume 6617 of LNCS. Springer pp 101–115

Ehlers R Könighofer R Bloem R(2015) Synthesizing cooperative reactive mission plans. In: 2015 IEEE/RSJ international conference on intelligent robots and systems IROS 2015 Hamburg Germany September 28–October 2 2015. IEEE pp 3478–3485

Filippidis I Dathathri S Livingston SC Ozay N Murray RM (2016) Control design for hybrid systems with tulip: the temporal logic planning toolbox. In: 2016 IEEE conference on control applications CCA 2016 Buenos Aires Argentina September 19–22 2016. IEEE pp 1030–1041

10.1007/s00236-019-00351-9

10.1007/s10009-011-0207-9

Grädel E Thomas W Wilke T (2002) editors. Automata logics and infinite games: a guide to current research [outcome of a Dagstuhl seminar February 2001] volume 2500 of lecture notes in computer science. Springer

10.1142/S0129054102000935

Hopcroft JE, 2008, Introduction to automata theory, languages, and computation

Jacobson I, 2004, Object-oriented software engineering: a use case driven approach

10.1109/TRO.2009.2030225

10.1007/s10009-011-0221-y

Kugler H Harel D Pnueli A Lu Y Bontemps Y Temporal logic for scenario-based specifications. In: International conference on tools and algorithms for the construction and analysis of systems. Springer pp 445–460

Kuvent A Maoz S Ringert JO (2017) A symbolic justice violations transition system for unrealizable GR

(1) specifications. In: Bodden E Schäfer W van Deursen A Zisman A (eds) Proceedings of the 2017 11th joint meeting on foundations of software engineering ESEC/FSE 2017 Paderborn Germany September 4-8 2017. ACM pp 362-372

Kozen D (1982) Results on the propositional μ-calculus. In: Proceedings of the 9th colloquium on automata languages and programming. Springer London pp 348–359

Klein U Pnueli A (2010) Revisiting synthesis of GR

(1) specifications. In: Barner S Harris S Kroening D Raz O (eds) Hardware and software: verification and testing-6th international Haifa verification conference HVC 2010 Haifa Israel October 4-7 2010. Revised selected papers volume 6504 of lecture notes in computer science. Springer pp 161-181

10.1016/j.ic.2005.01.006

Kesten Y Pnueli A Raviv L (1998) Algorithmic verification of linear temporal logic specifications. In: International colloquium on automata languages and programming. Springer pp 1–16

10.2307/421091

Kupferman O Vardi MY (2000) Synthesis with incomplete informatio. In: Advances in temporal logic. Springer pp 109–127

10.1016/j.tcs.2010.05.009

Maoz S Pistiner O Ringert JO (2016) Symbolic BDD and ADD algorithms for energy games. In: Piskac R Dimitrova R (eds) Proceedings fifth workshop on synthesis SYNT@CAV 2016 Toronto Canada July 17–18 2016. volume 229 of EPTCS pp 35–54

Majumdar R Piterman N Schmuck A-K (2019) Environmentally–friendly GR(1) synthesis. CoRR arXiv:1902.05629

Maoz S Ringert JO (2015) GR(1) synthesis for LTL specification patterns. In: ESEC/FSE. ACM pp 96–106

Maoz S Ringert JO (2015) Synthesizing a Lego Forklift controller in GR(1): a case study. In: Proceedings of the 4th workshop on synthesis SYNT 2015 colocated with CAV 2015 volume 202 of EPTCS pp 58–72

Maoz S Ringert JO (2016) On well-separation of GR

(1) specifications. In: Zimmermann T Cleland-Huang J Su Z (eds) Proceedings of the 24th ACM SIGSOFT international symposium on foundations of software engineering FSE 2016 Seattle WA USA November 13-18 2016. ACM pp 362-372

Maoz S, 2021, Spectra: a specification language for reactive systems, Softw Syst Model

Maoz S Ringert JO Shalom R (2019) Symbolic repairs for GR

(1) specifications. In: Atlee JM Bultan T Whittle J (eds) Proceedings of the 41st international conference on software engineering ICSE 2019 Montreal QC Canada May 25-31 2019. IEEE/ACM pp 1016-1026

Maoz S Sa'ar Y (2011) AspectLTL: an aspect language for LTL specifications. In: AOSD. ACM pp 19–30

Maoz S Sa'ar Y (2012) Assume-guarantee scenarios: semantics and synthesis. In: MODELS volume 7590 of LNCS. Springer pp 335–351

Maoz S Sa'ar Y (2013) Counter play-out: executing unrealizable scenario-based specifications. In: ICSE. IEEE/ACM pp 242–251

Maoz S Shalom R (2020) Inherent vacuity for GR(1) specifications. In: ESEC/FSE. ACM pp 99–110

Maoz S Shevrin I (2020) Just-in-time reactive synthesis. In: ASE. ACM pp 635–646

Maoz S Shalom R (2021) Unrealizable cores for reactive systems specifications. In: ICSE (to appear)

Maniatopoulos S Schillinger P Pong V Conner DC Kress-Gazit H (2016) Reactive high-level behavior synthesis for an atlas humanoid robot. In: Kragic D Bicchi A De Luca A (eds) 2016 IEEE international conference on robotics and automation ICRA 2016 Stockholm Sweden May 16–21 2016. IEEE pp 4192–4199

Pnueli A (1977) The temporal logic of programs. In: 18th Annual symposium on foundations of computer science Providence Rhode Island USA 31 October–1 November 1977. IEEE Computer Society pp 46–57

10.1007/978-3-642-12578-2

Piterman N Pnueli A Sa'ar Y (2006) Synthesis of reactive(1) designs. In: VMCAI volume 3855 of LNCS. Springer pp 364–380

Pnueli A Rosner R (1989) On the synthesis of a reactive module. In: POPL. ACM Press pp 179–190

Rosner R (1992) Modular synthesis of reactive systems. PhD thesis Weizmann Institute of Science

10.1109/TSE.2012.62

10.1109/32.738340

Somenzi F (2015) CUDD: CU decision diagram package release 3.0.0. http://vlsi.colorado.edu/~fabio/CUDD/cudd.pdf

Spectra Website. http://smlab.cs.tau.ac.il/syntech/spectra/

Sibay G Uchitel S Braberman V (2008) Existential live sequence charts revisited. In: Proceedings of the 30th international conference on software engineering. ACM pp 41–50

10.2140/pjm.1955.5.285

Uchitel S Brunet G Chechik M (2007) Behaviour model synthesis from properties and scenarios. In: Proceedings of the 29th international conference on software engineering. IEEE Computer Society pp 34–43

10.1109/TSE.2008.107

Veanes M de Halleux P Tillmann N (2010) Rex: symbolic regular expression explorer. In: Third international conference on software testing verification and validation ICST 2010 Paris France April 7–9 2010 pp 498–507

Walker A Ryzhyk L (2014) Predicate abstraction for reactive synthesis. In: Formal methods in computer-aided design FMCAD 2014 Lausanne Switzerland October 21–24 2014. IEEE pp 219–226

10.1109/MS.2005.134