Advertisement

A Weakness Measure for GR(1) Formulae

  • Davide Giacomo Cavezza
  • Dalal Alrajeh
  • András György
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

In spite of the theoretical and algorithmic developments for system synthesis in recent years, little effort has been dedicated to quantifying the quality of the specifications used for synthesis. When dealing with unrealizable specifications, finding the weakest environment assumptions that would ensure realizability is typically a desirable property; in such context the weakness of the assumptions is a major quality parameter. The question of whether one assumption is weaker than another is commonly interpreted using implication or, equivalently, language inclusion. However, this interpretation does not provide any further insight into the weakness of assumptions when implication does not hold. To our knowledge, the only measure that is capable of comparing two formulae in this case is entropy, but even it fails to provide a sufficiently refined notion of weakness in case of GR(1) formulae, a subset of linear temporal logic formulae which is of particular interest in controller synthesis. In this paper we propose a more refined measure of weakness based on the Hausdorff dimension, a concept that captures the notion of size of the omega-language satisfying a linear temporal logic formula. We identify the conditions under which this measure is guaranteed to distinguish between weaker and stronger GR(1) formulae. We evaluate our proposed weakness measure in the context of computing GR(1) assumptions refinements.

Notes

Acknowledgments

The support of the EPSRC HiPEDS Centre for Doctoral Training (EP/L016796/1) is gratefully acknowledged. We also thank our reviewers for their insightful comments and suggestions.

References

  1. 1.
  2. 2.
    Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. ACM SIGPLAN Notices 51(1), 789–801 (2016)CrossRefGoogle Scholar
  3. 3.
    Almagor, S., Avni, G., Kupferman, O.: Automatic generation of quality specifications. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 479–494. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_32CrossRefGoogle Scholar
  4. 4.
    Alur, R., Moarref, S., Topcu, U.: Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Formal Methods in Computer-Aided Design, pp. 26–33 (2013)Google Scholar
  5. 5.
    Alur, R., Moarref, S., Topcu, U.: Pattern-based refinement of assume-guarantee specifications in reactive synthesis. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 501–516. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_49CrossRefGoogle Scholar
  6. 6.
    Asarin, E., Blockelet, M., Degorre, A.: Entropy model checking. In: 12th Workshop on Quantitative Aspects of Programming Languages - Joint with European Joint Conference On Theory and Practice of Software (2014)Google Scholar
  7. 7.
    Asarin, E., Blockelet, M., Degorre, A., Dima, C., Mu, C.: Asymptotic behaviour in temporal logic. In: Joint Meeting CSL/LICS, pp. 1–9. ACM Press (2014)Google Scholar
  8. 8.
    Barnat, J., Bauch, P., Beneš, N., Brim, L., Beran, J., Kratochvíla, T.: Analysing sanity of requirements for avionics systems. Form. Asp. Comput. 28(1), 45–63 (2016)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Berman, A., Plemmons, R.: Nonnegative Matrices in the Mathematical Sciences. Society for Industrial and Applied Mathematics (1994)Google Scholar
  10. 10.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_14CrossRefGoogle Scholar
  11. 11.
    Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electron. Notes Theor. Comput. Sci. 190(4), 3–16 (2007)CrossRefGoogle Scholar
  12. 12.
    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)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Braberman, V., D’Ippolito, N., Piterman, N., Sykes, D., Uchitel, S.: Controller synthesis: from modelling to enactment. In: International Conference on Software Engineering, pp. 1347–1350. IEEE (2013)Google Scholar
  14. 14.
    Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, New York (2008)CrossRefGoogle Scholar
  15. 15.
    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_16CrossRefGoogle Scholar
  16. 16.
    Cavezza, D.G., Alrajeh, D., György, A.: A weakness measure for GR(1) formulae. CoRR abs/1805.03151 (2018). http://arxiv.org/abs/1805.03151
  17. 17.
    Chatterjee, K., De Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: International Conference on the Quantitative Evaluation of Systems, pp. 179–188 (2006)Google Scholar
  18. 18.
    Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 147–161. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85361-9_14CrossRefGoogle Scholar
  19. 19.
    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_9CrossRefGoogle Scholar
  20. 20.
    Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36577-X_24CrossRefzbMATHGoogle Scholar
  21. 21.
    D’Ippolito, N., Braberman, V., Sykes, D., Uchitel, S.: Robust degradation and enhancement of robot mission behaviour in unpredictable environments. In: Proceedings of the 1st International Workshop on Control Theory for Software Engineering, pp. 26–33 (2015)Google Scholar
  22. 22.
    Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_8CrossRefGoogle Scholar
  23. 23.
    Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata. Formal Methods Syst. Des. 49(3), 219–271 (2016)CrossRefGoogle Scholar
  24. 24.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)CrossRefGoogle Scholar
  25. 25.
    Henzinger, T.: From Boolean to quantitative notions of correctness. ACM SIGPLAN Notices 45(1), 157 (2010)CrossRefGoogle Scholar
  26. 26.
    Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 273–287. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40184-8_20CrossRefGoogle Scholar
  27. 27.
    Konighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: Formal Methods in Computer-Aided Design, pp. 152–159 (2009)Google Scholar
  28. 28.
    Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 88–98. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27660-6_8CrossRefGoogle Scholar
  29. 29.
    Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: Joint Meeting on Foundations of Software Engineering - ESEC/FSE 2015, p. 449. ACM Press (2007)Google Scholar
  30. 30.
    Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: International Conference on Formal Methods and Models for Codesign, pp. 43–50 (2011)Google Scholar
  31. 31.
    Lomuscio, A., Strulo, B., Walker, N., Wu, P.: Assume-guarantee reasoning with local specifications. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 204–219. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16901-4_15CrossRefGoogle Scholar
  32. 32.
    Lutz, A.D.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1/2), 31 (2014)CrossRefGoogle Scholar
  33. 33.
    Maoz, S., Ringert, J.O.: GR(1) synthesis for LTL specification patterns. In: Joint Meeting on Foundations of Software Engineering - ESEC/FSE 2015, pp. 96–106. ACM Press (2015)Google Scholar
  34. 34.
    Merzenich, W., Staiger, L.: Fractals, dimension, and formal languages. Informatique théorique et applications 28(3–4), 361–386 (1994)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Nam, W., Alur, R.: Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 170–185. Springer, Heidelberg (2006).  https://doi.org/10.1007/11901914_15CrossRefGoogle Scholar
  36. 36.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Principles of Programming Languages, pp. 179–190 (1989)Google Scholar
  37. 37.
    Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, pp. 46–57 (1977)Google Scholar
  38. 38.
    Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Three SCC-based emptiness checks for generalized Büchi automata. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), pp. 668–682 (2013)CrossRefGoogle Scholar
  39. 39.
    Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. IEEE 103(11), 2036–2051 (2015)CrossRefGoogle Scholar
  40. 40.
    Staiger, L.: The hausdorff measure of regular \(\omega \)-languages is computable. Martin-Luther-Universität, Technical report, August 1998Google Scholar
  41. 41.
    Staiger, L.: On the Hausdorff measure of regular omega-languages in Cantor space. Technical report 1, Martin-Luther-Universität Halle-Wittenberg (2015)Google Scholar
  42. 42.
    Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Proceedings of the IEEE International Conference on Information Reuse and Integration, pp. 493–498 (2004)Google Scholar
  43. 43.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60915-6_6CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Davide Giacomo Cavezza
    • 1
  • Dalal Alrajeh
    • 1
  • András György
    • 1
  1. 1.Imperial College LondonLondonUK

Personalised recommendations