Skip to main content
SpringerLink
Log in

Quantitative Monitor Automata

  • Conference paper
  • First Online:
Static Analysis (SAS 2016)

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

Included in the following conference series:

Abstract

In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted \(\omega \)-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted \(\omega \)-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted \(\omega \)-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted \(\omega \)-automata with monitors generalize weighted \(\omega \)-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties.

This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.

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

Notes

  1. 1.

    We use the term “quantitative” in a non-probabilistic sense, which assigns a quantitative value to each infinite run of a system, representing long-run average or maximal response time, or power consumption, or the like, rather than taking a probabilistic average over different runs.

References

  1. Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: \’{A}brahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 424–439. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  2. Alur, R., D’Antoni, L., Deshmukh, J.V., Raghothaman, M., Yuan, Y.: Regular functions and cost register automata. In: LICS 2013, pp. 13–22 (2013)

    Google Scholar 

  3. Baier, C., Dubslaff, C., Klüppelholz, S.: Trade-off analysis meets probabilistic model checking. In: CSL-LICS 2014, pp. 1:1–1:10 (2014)

    Google Scholar 

  4. Baier, C., Klein, J., Klüppelholz, S., Wunderlich, S.: Weight monitoring with linear temporal logic: complexity and decidability. In: CSL-LICS 2014, pp. 11:1–11:10 (2014)

    Google Scholar 

  5. Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. ACM TOCL 15(4), 1–25 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bollig, B., Gastin, P., Monmege, B., Zeitoun, M.: Pebble weighted automata and transitive closure logics. In: Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G., Abramsky, S. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 587–598. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Bouyer, P., Markey, N., Matteplackel, R.M.: Averaging in LTL. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 266–280. Springer, Heidelberg (2014)

    Google Scholar 

  8. Brázdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: LICS 2011, pp. 33–42 (2011)

    Google Scholar 

  9. Brázdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Multigain: a controller synthesis tool for MDPs with multiple mean-payoff objectives. In: TACAS 2015, pp. 181–187 (2015)

    Google Scholar 

  10. Chatterjee, K.: Markov decision processes with multiple long-run average objectives. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 473–484. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Chatterjee, K., Doyen, L.: Energy and mean-payoff parity Markov decision processes. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 206–218. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T.A., Rannou, P.: Mean-payoff automaton expressions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 269–283. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  13. Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. LMCS, 6(3) (2010)

    Google Scholar 

  14. Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM TOCL 11(4), 23 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  15. Chatterjee, K., Forejt, V., Wojtczak, D.: Multi-objective discounted reward verification in graphs and MDPs. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 228–242. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted limit-average automata of bounded width. To appear at MFCS 2016 (2016)

    Google Scholar 

  17. Chatterjee, K., Henzinger, T.A., Otop, J.: Quantitative automata under probabilistic semantics. To appear at LICS 2016 (2016)

    Google Scholar 

  18. Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted automata. In: LICS 2015, pp. 725–737 (2015)

    Google Scholar 

  19. Chatterjee, K., Komárková, Z., Kretínský, J.: Unifying two views on multiple mean-payoff objectives in Markov Decision Processes. In: LICS 2015, pp. 244–256 (2015)

    Google Scholar 

  20. Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 325–336. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Degorre, A., Doyen, L., Gentilini, R., Raskin, J.-F., Toruńczyk, S.: Energy and mean-payoff games with imperfect information. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 260–274. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer, Heidelberg (2009)

    Book  MATH  Google Scholar 

  23. Droste, M., Rahonis, G.: Weighted automata and weighted logics on infinite words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 49–58. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1996)

    Book  MATH  Google Scholar 

  25. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112–127. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

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

    Google Scholar 

  27. Puterman, M.L., Processes, M.D.: Discrete Stochastic Dynamic Programming, 1st edn. Wiley, New York (1994)

    Google Scholar 

  28. Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. b, pp. 133–191. MIT Press, Cambridge (1990)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IST Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee & Thomas A. Henzinger

  2. University of Wroclaw, Wroclaw, Poland

    Jan Otop

Authors
  1. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas A. Henzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jan Otop
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Krishnendu Chatterjee .

Editor information

Editors and Affiliations

  1. Ecole Normale Supérieure , Paris, France

    Xavier Rival

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag GmbH Germany

About this paper

Cite this paper

Chatterjee, K., Henzinger, T.A., Otop, J. (2016). Quantitative Monitor Automata. In: Rival, X. (eds) Static Analysis. SAS 2016. Lecture Notes in Computer Science(), vol 9837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-53413-7_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-53412-0

  • Online ISBN: 978-3-662-53413-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation