Abstract
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains. A common form of providing system's requirements is through use cases, which are existential in nature. However, GR(1), as a fragment of LTL, is limited to universal properties. In this paper we introduce GR(1)*, which extends GR(1) with existential guarantees. We show that GR(1)* is strictly more expressive than GR(1) as it enables the expression of guarantees that are inexpressible in LTL. We solve the realizability problem for GR(1)* and present a symbolic strategy construction algorithm for GR(1)* specifications. Importantly, in comparison to GR(1), GR(1)* remains efficient: the time complexity of our realizability checking and synthesis procedures for GR(1)* is identical to the time complexity of the known corresponding procedures for GR(1).
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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., Kupferman, O., Ringert, J.O., Velner, Y.: Quantitative assume guarantee synthesis. In: Rupak, M., Viktor, K. (eds.) Computer aided verification–29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part II. lecture notes in computer science, vol. 10427, pp. 353–374. Springer (2017)
Alexander, I.F., Maiden, N.: Scenarios, stories, use cases: through the systems development life-cycle, 1st edn. Wiley (2004)
Amram, G., Maoz, S., Pistiner, O.: GR(1)*: GR(1) specifications extended with existential guarantees. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal methods–the next 30 years–third world congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings. lecture notes in computer science, vol. 11800, pp. 83–100. Springer (2019)
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
Alrajeh, D., Ray, O., Russo, A., Uchitel, S.: Using abduction and induction for operational requirements elaboration. J Appl Logic 7(3), 275–288 (2009)
Browne, A., Clarke, E.M., Jha, S., Long, D.E., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. Theor Comput Sci 178(1–2), 237–255 (1997)
Bloem, R., Ehlers, R., Könighofer, R.: Cooperative reactive synthesis. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated technology for verification and analysis–13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015, Proceedings. lecture notes in computer science, vol. 9364, pp. 394–410. Springer (2015)
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
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa'ar, Y.: Synthesis of reactive(1) designs. J Comput Syst Sci 78(3), 911–938 (2012)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8), 677–691 (1986)
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
D'Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S.: Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans Softw Eng Methodol 22(1), 9 (2013)
Emerson, A.E., Halpern, J.Y.: "sometimes" and "not never" revisited: on branching versus linear time temporal logic. J ACM 33(1), 151–178 (1986)
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
Firman, E., Maoz, S., Ringert, J.O.: Performance heuristics for GR(1) synthesis and related algorithms. Acta Inform 57(1–2), 37–79 (2020)
Godhal, Y., Chatterjee, K., Henzinger, T.A.: Synthesis of AMBA AHB from formal specification: a case study. STTT 15(5–6), 585–601 (2013)
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
Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. Int J Found Comput Sci 13(01), 5–51 (2002)
Hopcroft, J.E.: Introduction to automata theory, languages, and computation. Pearson Education, India (2008)
Jacobson, I.: Object-oriented software engineering: a use case driven approach. Addison Wesley, Redwood City (2004)
Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans Robot 25(6), 1370–1381 (2009)
Könighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. STTT 15(5–6), 563–583 (2013)
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 \(\mu \)-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
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf Comput 200(1), 35–61 (2005)
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
Kupferman, O., Vardi, M.Y.: Church's problem revisited. Bull Symb Logic 5(2), 245–263 (1999)
Kupferman O, Vardi MY (2000) Synthesis with incomplete informatio. In: Advances in temporal logic. Springer, pp 109–127
Mateescu, R., Monteiro, P.T., Dumas, E., de Jong, H.: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. Theor Comput Sci 412(26), 2854–2883 (2011)
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., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw Syst Model (2021). https://doi.org/10.1007/s10270-021-00868-z
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
Pohl, K.: Requirements engineering: fundamentals, principles, and techniques, 1st edn. Springer (2010)
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
Sibay, G.E., Braberman, V., Uchitel, S., Kramer, J.: Synthesizing modal transition systems from triggered scenarios. IEEE Trans Softw Eng 39(7), 975–1001 (2013)
Sutcliffe, A.G., Maiden, N.A.M., Minocha, S., Manuel, D.: Supporting scenario-based requirements engineering. IEEE Trans Softw Eng 24(12), 1072–1088 (1998)
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
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2), 285–309 (1955)
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
Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng 35(3), 384–406 (2009)
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
Zachos, K., Maiden, N., Tosar, A.: Rich-media scenarios for discovering requirements. IEEE Softw 22(5), 89–97 (2005)
Author information
Authors and Affiliations
Corresponding author
Additional information
Annabelle McIver, Maurice ter Beek and Cliff Jones
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Amram, G., Maoz, S. & Pistiner, O. GR(1)*: GR(1) specifications extended with existential guarantees. Form Asp Comp 33, 729–761 (2021). https://doi.org/10.1007/s00165-021-00535-6
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-021-00535-6