Advertisement

Verifying Quantitative Properties Using Bound Functions

  • Arindam Chakrabarti
  • Krishnendu Chatterjee
  • Thomas A. Henzinger
  • Orna Kupferman
  • Rupak Majumdar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

We define and study a quantitative generalization of the traditional boolean framework of model-based specification and verification. In our setting, propositions have integer values at states, and properties have integer values on traces. For example, the value of a quantitative proposition at a state may represent power consumed at the state, and the value of a quantitative property on a trace may represent energy used along the trace. The value of a quantitative property at a state, then, is the maximum (or minimum) value achievable over all possible traces from the state. In this framework, model checking can be used to compute, for example, the minimum battery capacity necessary for achieving a given objective, or the maximal achievable lifetime of a system with a given initial battery capacity. In the case of open systems, these problems require the solution of games with integer values.

Quantitative model checking and game solving is undecidable, except if bounds on the computation can be found. Indeed, many interesting quantitative properties, like minimal necessary battery capacity and maximal achievable lifetime, can be naturally specified by quantitative-bound automata, which are finite automata with integer registers whose analysis is constrained by a bound function f that maps each system K to an integer f(K). Along with the linear-time, automaton-based view of quantitative verification, we present a corresponding branching-time view based on a quantitative-bound μ-calculus, and we study the relationship, expressive power, and complexity of both views.

Keywords

Model Check Recursive Function Quantitative Property Symbolic Model Check Bound Model Check 
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.

References

  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)Google Scholar
  3. 3.
    Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Bouyer, P., Petit, A., Thérien, D.: An algebraic approach to data languages and timed languages. Information & Computation 182, 137–162 (2003)zbMATHCrossRefGoogle Scholar
  5. 5.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information & Computation 98, 142–170 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  8. 8.
    Dam, M.: CTL* and ECTL* as fragments of the modal μ-calculus. Theoretical Computer Science 126, 77–96 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for ω-regular objectives. In: LICS, pp. 279–290. IEEE, Los Alamitos (2001)Google Scholar
  10. 10.
    de Alfaro, L., Majumdar, R.: Quantitative solution of concurrent games. J. Computer & Systems Sciences 68, 374–397 (2004)zbMATHCrossRefGoogle Scholar
  11. 11.
    Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional μ-calculus. In: LICS, pp. 267–278. IEEE, Los Alamitos (1986)Google Scholar
  12. 12.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)Google Scholar
  13. 13.
    Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: LICS, pp. 111–122. IEEE, Los Alamitos (1997)Google Scholar
  14. 14.
    Ibarra, O.H., Su, J., Dang, Z., Bultan, T., Kemmerer, R.A.: Counter machines: Decidable properties and applications to verification problems. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 426–435. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    McIver, A., Morgan, C.: Games, probability, and the quantitative μ-calculus. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 292–310. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Vardi, M.Y.: A temporal fixpoint calculus. In: POPL, pp. 250–259. ACM, New York (1988)Google Scholar
  18. 18.
    Xie, G., Dang, Z., Ibarra, O.H., Pietro, P.S.: Dense counter machines and verification problems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 93–105. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Arindam Chakrabarti
    • 1
  • Krishnendu Chatterjee
    • 1
  • Thomas A. Henzinger
    • 1
    • 4
  • Orna Kupferman
    • 2
  • Rupak Majumdar
    • 3
  1. 1.UC BerkeleyUSA
  2. 2.Hebrew UniversityIsrael
  3. 3.UC Los AngelesUSA
  4. 4.EPFLSwitzerland

Personalised recommendations