Skip to main content
SpringerLink
Log in

A Weakness Measure for GR(1) Formulae

  • Conference paper
  • First Online:
Formal Methods (FM 2018)

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

Included in the following conference series:

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.

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

Access this chapter

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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

Institutional subscriptions

References

  1. https://gitlab.doc.ic.ac.uk/dgc14/WeakestAssumptions

  2. Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. ACM SIGPLAN Notices 51(1), 789–801 (2016)

    Article  Google Scholar 

  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_32

    Chapter  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, pp. 26–33 (2013)

    Google Scholar 

  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_49

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  9. Berman, A., Plemmons, R.: Nonnegative Matrices in the Mathematical Sciences. Society for Industrial and Applied Mathematics (1994)

    Google Scholar 

  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_14

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, New York (2008)

    Book  Google Scholar 

  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_16

    Chapter  Google Scholar 

  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. 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. 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_14

    Chapter  Google Scholar 

  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_9

    Chapter  Google Scholar 

  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_24

    Chapter  MATH  Google Scholar 

  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. 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_8

    Chapter  Google Scholar 

  23. Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata. Formal Methods Syst. Des. 49(3), 219–271 (2016)

    Article  Google Scholar 

  24. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)

    Article  Google Scholar 

  25. Henzinger, T.: From Boolean to quantitative notions of correctness. ACM SIGPLAN Notices 45(1), 157 (2010)

    Article  Google Scholar 

  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_20

    Chapter  Google Scholar 

  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. 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_8

    Chapter  Google Scholar 

  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. 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. 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_15

    Chapter  Google Scholar 

  32. Lutz, A.D.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1/2), 31 (2014)

    Article  Google Scholar 

  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. Merzenich, W., Staiger, L.: Fractals, dimension, and formal languages. Informatique théorique et applications 28(3–4), 361–386 (1994)

    Article  MathSciNet  Google Scholar 

  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_15

    Chapter  Google Scholar 

  36. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Principles of Programming Languages, pp. 179–190 (1989)

    Google Scholar 

  37. Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, pp. 46–57 (1977)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  39. Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. IEEE 103(11), 2036–2051 (2015)

    Article  Google Scholar 

  40. Staiger, L.: The hausdorff measure of regular \(\omega \)-languages is computable. Martin-Luther-Universität, Technical report, August 1998

    Google Scholar 

  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. 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. 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_6

    Chapter  Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. Imperial College London, London, UK

    Davide Giacomo Cavezza, Dalal Alrajeh & András György

Authors
  1. Davide Giacomo Cavezza
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dalal Alrajeh
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. András György
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Davide Giacomo Cavezza .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cavezza, D.G., Alrajeh, D., György, A. (2018). A Weakness Measure for GR(1) Formulae. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation