GR(1)*: GR(1) specifications extended with existential guarantees. (English) Zbl 1539.68147
ter Beek, Maurice H. (ed.) et al., Formal methods – the next 30 years. Third world congress/23rd symposium, FM 2019, Porto, Portugal, October 7–11, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11800, 83-100 (2019).
Summary: 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.
For the entire collection see [Zbl 1423.68040].
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.
For the entire collection see [Zbl 1423.68040].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
References:
| [1] | Alexander, I.F., Maiden, N.: Scenarios, Stories, Use Cases: Through the Systems Development Life-Cycle. 1st edn. Wiley Publishing (2004) |
| [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 |
| [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) · Zbl 1176.68152 |
| [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 · Zbl 1471.68131 |
| [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 · Zbl 1247.68050 |
| [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 · Zbl 0901.68118 |
| [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 · Zbl 0593.94022 |
| [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 · Zbl 1452.68115 |
| [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 · Zbl 1138.68442 |
| [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 · Zbl 0546.68014 |
| [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 |
| [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) |
| [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 · Zbl 0629.68020 |
| [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) · Zbl 1066.68017 |
| [19] | Jacobson, I.: Object-Oriented Software Engineering: A Use Case Driven Approach. Addison Wesley Longman Publishing Co. Inc, Redwood City (2004) |
| [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 · Zbl 1082.68055 |
| [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 |
| [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 · Zbl 0507.03005 |
| [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 |
| [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 · Zbl 1087.68596 |
| [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 · Zbl 0953.68090 |
| [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 |
| [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 · Zbl 1176.68126 |
| [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) |
| [37] | Pohl, K.: Requirements Engineering: Fundamentals, Principles, and Techniques, 1st edn. Springer Publishing Company, Incorporated (2010) |
| [38] | Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992) |
| [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) |
| [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) |
| [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) |
| [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 · Zbl 0064.26004 |
| [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) |
| [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) |
| [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) |
| [48] | Spectra Website. http://smlab.cs.tau.ac.il/syntech/spectra/ |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
