Compositional Branching-Time Measurements

  • Radu Grosu
  • Doron Peled
  • C. R. Ramakrishnan
  • Scott A. Smolka
  • Scott D. Stoller
  • Junxing Yang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8415)


Formal methods are used to increase the reliability of software and hardware systems. Methods such as model checking, verification and testing are used to search for design and coding errors, integrated in the process of system design. Beyond checking whether a system satisfies a particular specification, we may want to measure some of its quantitative properties. Earlier works on system measurements suggest extending model checking techniques to measure quantitative artifacts, based on weights associated with the transitions of a transition system. Other works allow counting while performing model checking or runtime verification. This paper presents a simple and efficient compositional measuring framework based on quantitative state testers. The framework allows combining multiple measures, such as distance and power consumption, using a variety of functions, such as min, max, and average. This supports calculation of interesting compound measures that quantitatively characterize a system’s behavior.


  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.
    Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Log. 2(3), 388–407 (2001)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers, vol. 58. Academic Press (2003)Google Scholar
  4. 4.
    Chakrabarti, A., Chatterjee, K., Henzinger, T.A., Kupferman, O., Majumdar, R.: Verifying Quantitative Properties Using Bound Functions. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 50–64. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and Closure Properties for Quantitative Languages. Logical Methods in Computer Science 6(3) (2010)Google Scholar
  6. 6.
    Clarke, E.M., Allen Emerson, E.: 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)CrossRefGoogle Scholar
  7. 7.
    Allen Emerson, E., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  8. 8.
    Faymonville, P., Finkbeiner, B., Peled, D.: Monitoring Parametric Temporal Logic. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 357–375. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  9. 9.
    Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  10. 10.
    Kesten, Y., Pnueli, A., Raviv, L.-O.: Algorithmic Verification of Linear Temporal Logic Specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Queille, J.-P., Sifakis, J.: Iterative Methods for the Analysis of Petri Nets. In: Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets. LNCS, vol. 51, pp. 161–167. Springer (1981)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Radu Grosu
    • 1
  • Doron Peled
    • 2
  • C. R. Ramakrishnan
    • 3
  • Scott A. Smolka
    • 3
  • Scott D. Stoller
    • 3
  • Junxing Yang
    • 3
  1. 1.Vienna University of TechnologyAustria
  2. 2.Bar Ilan UniversityIsrael
  3. 3.Stony Brook UniversityUSA

Personalised recommendations