Advertisement

Formalizing and Reasoning about Quality

  • Shaull Almagor
  • Udi Boker
  • Orna Kupferman
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)

Abstract

Traditional formal methods are based on a Boolean satisfaction notion: a reactive system satisfies, or not, a given specification. We generalize formal methods to also address the quality of systems. As an adequate specification formalism we introduce the linear temporal logic LTL[\({\cal F}\)]. The satisfaction value of an LTL[\({\cal F}\)] formula is a number between 0 and 1, describing the quality of the satisfaction. The logic generalizes traditional LTL by augmenting it with a (parameterized) set \({\cal F}\) of arbitrary functions over the interval [0,1]. For example, \({\cal F}\) may contain the maximum or minimum between the satisfaction values of subformulas, their product, and their average.

The classical decision problems in formal methods, such as satisfiability, model checking, and synthesis, are generalized to search and optimization problems in the quantitative setting. For example, model checking asks for the quality in which a specification is satisfied, and synthesis returns a system satisfying the specification with the highest quality. Reasoning about quality gives rise to other natural questions, like the distance between specifications. We formalize these basic questions and study them for LTL[\({\cal F}\)]. By extending the automata-theoretic approach for LTL to a setting that takes quality into an account, we are able to solve the above problems and show that reasoning about LTL[\({\cal F}\)] has roughly the same complexity as reasoning about traditional LTL.

Keywords

Model Check Temporal Logic Atomic Proposition Kripke Structure Tree Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Almagor, S., Boker, U., Kupferman, O.: What’s decidable about weighted automata? In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 482–491. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: 26th LICS, pp. 43–52 (2011)Google Scholar
  4. 4.
    Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Černý, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative Synthesis for Concurrent Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Clarke, E., Henzinger, T.A., Veith, H.: Handbook of Model Checking. Elsvier (2013)Google Scholar
  7. 7.
    de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. TCS 345(1), 139–170 (2005)zbMATHCrossRefGoogle Scholar
  8. 8.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled markov processes. TCS 318(3), 323–354 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    Droste, M., Kuich, W., Rahonis, G.: Multi-valued MSO logics over words and trees. Fundamenta Informaticae 84(3-4), 305–327 (2008)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. TCS 410(37), 3481–3494 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On Temporal Logic and Signal Processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92–106. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    Droste, M., Werner, K., Heiko, V.: Handbook of Weighted Automata. Springer (2009)Google Scholar
  13. 13.
    Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: On branching versus linear time. Journal of the ACM 33(1), 151–178 (1986)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Emerson, E.A., Lei, C.L.: Modalities for model checking: Branching time logic strikes back. In: Proc. 12th POPL, pp. 84–96 (1985)Google Scholar
  15. 15.
    Faella, M., Legay, A., Stoelinga, M.: Model Checking Quantitative Linear Time Logic. TCS 220(3), 61–77 (2008)Google Scholar
  16. 16.
    Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Trans. on Robotics 25(6), 1370–1381 (2009)CrossRefGoogle Scholar
  17. 17.
    Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. International Journal of Algebra and Computation 4(3), 405–425 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199–213. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, pp. 531–540 (2005)Google Scholar
  20. 20.
    Kwiatkowska, M.Z.: Quantitative verification: models techniques and tools. In: FSE, pp. 449–458 (2007)Google Scholar
  21. 21.
    Mohri, M.: Finite-state transducers in language and speech processing. Computational Linguistics 23(2), 269–311 (1997)MathSciNetGoogle Scholar
  22. 22.
    Moon, S., Lee, K.H., Lee, D.: Fuzzy branching temporal logic. IEEE Transactions on Systems, Man, and Cybernetics, Part B 34(2), 1045–1055 (2004)CrossRefGoogle Scholar
  23. 23.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc.16th POPL, pp. 179–190 (1989)Google Scholar
  24. 24.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, pp. 133–191 (1990)Google Scholar
  25. 25.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332–344 (1986)Google Scholar
  26. 26.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C 115(1), 1–37 (1994)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Shaull Almagor
    • 1
  • Udi Boker
    • 2
  • Orna Kupferman
    • 1
  1. 1.The Hebrew UniversityJerusalemIsrael
  2. 2.IST AustriaKlosterneuburgAustria

Personalised recommendations