Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2019: Formal Methods – The Next 30 Years pp 83–100Cite as

GR(1)*: GR(1) Specifications Extended with Existential Guarantees

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

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 the 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, and induces only a minor additional cost in terms of time complexity, proportional to the extended length of the formula.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In fact, they are equal, but we do not use this observation in the correctness proof of the algorithm.

  2. 2.

    Even though the algorithm is deterministic, we performed multiple runs since JVM garbage collection and the default automatic variable reordering of CUDD add variance to running times.

References

  1. Alexander, I.F., Maiden, N.: Scenarios, Stories, Use Cases: Through the Systems Development Life-Cycle. 1st edn. Wiley Publishing (2004)

    Google Scholar 

  2. Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: Learning from vacuously satisfiable scenario-based specifications. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 377–393. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28872-2_26

    Chapter  Google Scholar 

  3. Alrajeh, D., Ray, O., Russo, A., Uchitel, S.: Using abduction and induction for operational requirements elaboration. J. Appl. Logic 7(3), 275–288 (2009)

    Article  MathSciNet  Google Scholar 

  4. Alur, R., Moarref, S., Topcu, U.: Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 26–33. IEEE (2013). https://doi.org/10.1109/FMCAD.2013.6679387

  5. Bloem, R., Ehlers, R., Könighofer, R.: Cooperative reactive synthesis. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 394–410. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24953-7_29

    Chapter  Google Scholar 

  6. 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). https://doi.org/10.1016/j.jcss.2011.08.007

  7. Bloem, R., Schewe, S., Khalimov, A.: CTL* synthesis via LTL synthesis. In: Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22 July 2017, pp. 4–22 (2017). https://doi.org/10.4204/EPTCS.260.4

  8. 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). https://doi.org/10.1016/S0304-3975(96)00228-9

    Article  MathSciNet  MATH  Google Scholar 

  9. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986). https://doi.org/10.1109/TC.1986.1676819

    Article  MATH  Google Scholar 

  10. Cavezza, D.G., Alrajeh, D.: Interpolation-based GR(1) assumptions refinement. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 281–297. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_16

    Chapter  Google Scholar 

  11. Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 52–67. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78163-9_9

    Chapter  Google Scholar 

  12. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

  13. 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). https://doi.org/10.1145/2430536.2430543

    Article  Google Scholar 

  14. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411–420. ACM (1999)

    Google Scholar 

  15. Ehlers, R., Könighofer, R., Bloem, R.: Synthesizing cooperative reactive mission plans. In: 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2015, Hamburg, Germany, 28 September - 2 October 2015, pp. 3478–3485. IEEE (2015). https://doi.org/10.1109/IROS.2015.7353862

  16. Emerson, E.A., Halpern, J.Y.: “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986). https://doi.org/10.1145/4904.4999

    Article  MathSciNet  MATH  Google Scholar 

  17. Filippidis, I., Dathathri, S., Livingston, S.C., Ozay, N., Murray, R.M.: Control design for hybrid systems with tulip: the temporal logic planning toolbox. In: 2016 IEEE Conference on Control Applications, CCA 2016, Buenos Aires, Argentina, 19–22 September 2016, pp. 1030–1041. IEEE (2016). https://doi.org/10.1109/CCA.2016.7587949

  18. Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. Int. J. Found. Comput. Sci. 13(01), 5–51 (2002)

    Article  MathSciNet  Google Scholar 

  19. Jacobson, I.: Object-Oriented Software Engineering: A Use Case Driven Approach. Addison Wesley Longman Publishing Co. Inc, Redwood City (2004)

    Google Scholar 

  20. Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf. Comput. 200(1), 35–61 (2005). http://www.sciencedirect.com/science/article/pii/S0890540105000234

  21. 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). https://doi.org/10.1007/s10009-011-0221-y

    Article  Google Scholar 

  22. Kozen, D.: Results on the propositional \(\mu \)-calculus. In: Proceedings of the 9th Colloquium on Automata, Languages and Programming, pp. 348–359. Springer, London (1982). http://dl.acm.org/citation.cfm?id=646236.682866

  23. 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). https://doi.org/10.1109/TRO.2009.2030225

    Article  Google Scholar 

  24. Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal logic for scenario-based specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_29

    Chapter  MATH  Google Scholar 

  25. Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (eds.) Advances in Temporal Logic, vol. 16, pp. 109–127. Springer, Dordrecht (2000). https://doi.org/10.1007/978-94-015-9586-5_6

    Chapter  Google Scholar 

  26. Majumdar, R., Piterman, N., Schmuck, A.: Environmentally-friendly GR(1) synthesis. CoRR abs/1902.05629 (2019). http://arxiv.org/abs/1902.05629

  27. Maniatopoulos, S., Schillinger, P., Pong, V., Conner, D.C., Kress-Gazit, H.: Reactive high-level behavior synthesis for an atlas humanoid robot. In: Kragic, D., Bicchi, A., Luca, A.D. (eds.) 2016 IEEE International Conference on Robotics and Automation, ICRA 2016, Stockholm, Sweden, 16–21 May 2016, pp. 4192–4199. IEEE (2016). https://doi.org/10.1109/ICRA.2016.7487613

  28. Maoz, S., Ringert, J.O.: GR(1) synthesis for LTL specification patterns. In: ESEC/FSE, pp. 96–106. ACM (2015). https://doi.org/10.1145/2786805.2786824

  29. Maoz, S., Ringert, J.O.: 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, 13–18 November 2016, pp. 362–372. ACM (2016). https://doi.org/10.1145/2950290.2950300

  30. Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. CoRR abs/1904.06668 (2019). http://arxiv.org/abs/1904.06668

  31. Maoz, S., Ringert, J.O., Shalom, R.: Symbolic repairs for GR(1) specifications. In: Mussbacher, G., Atlee, J.M., Bultan, T. (eds.) Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, 25–31 May 2019, pp. 1016–1026. IEEE/ACM (2019). https://dl.acm.org/citation.cfm?id=3339632

  32. Maoz, S., Sa’ar, Y.: AspectLTL: an aspect language for LTL specifications. In: AOSD, pp. 19–30. ACM (2011). https://doi.org/10.1145/1960275.1960280

  33. Maoz, S., Sa’ar, Y.: Assume-guarantee scenarios: semantics and synthesis. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) Model Driven Engineering Languages and Systems. MODELS 2012 LNCS, vol. 7590, pp. 335–351. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33666-9_22

    Chapter  Google Scholar 

  34. Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive (1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_24

    Chapter  Google Scholar 

  35. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October – 1 November 1977, pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32

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

    Google Scholar 

  37. Pohl, K.: Requirements Engineering: Fundamentals, Principles, and Techniques, 1st edn. Springer Publishing Company, Incorporated (2010)

    Google Scholar 

  38. Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)

    Google Scholar 

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

    Google Scholar 

  40. 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)

    Article  Google Scholar 

  41. Somenzi, F.: CUDD: CU Decision Diagram Package Release 3.0.0 (2015). http://vlsi.colorado.edu/~fabio/CUDD/cudd.pdf

  42. Sutcliffe, A.G., Maiden, N.A., Minocha, S., Manuel, D.: Supporting scenario-based requirements engineering. IEEE Trans. Softw. Eng. 24(12), 1072–1088 (1998)

    Article  Google Scholar 

  43. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955). https://doi.org/10.2140/pjm.1955.5.285

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  45. Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng. 35(3), 384–406 (2009)

    Article  Google Scholar 

  46. Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21–24 October 2014, pp. 219–226. IEEE (2014). https://doi.org/10.1109/FMCAD.2014.6987617

  47. Zachos, K., Maiden, N., Tosar, A.: Rich-media scenarios for discovering requirements. IEEE Softw. 22(5), 89–97 (2005)

    Article  Google Scholar 

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

Download references

Acknowledgements

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).

Author information

Authors and Affiliations

  1. Tel Aviv University, Tel Aviv, Israel

    Gal Amram, Shahar Maoz & Or Pistiner

Authors
  1. Gal Amram
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shahar Maoz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Or Pistiner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Shahar Maoz .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Amram, G., Maoz, S., Pistiner, O. (2019). GR(1)*: GR(1) Specifications Extended with Existential Guarantees. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation