Skip to main content
SpringerLink
Log in

Weighted versus Probabilistic Logics

  • Conference paper
Developments in Language Theory (DLT 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5583))

Included in the following conference series:

Abstract

While a mature theory around logics such as MSO, LTL, and CTL has been developed in the pure boolean setting of finite automata, weighted automata lack such a natural connection with (temporal) logic and related verification algorithms. In this paper, we will identify weighted versions of MSO and CTL that generalize the classical logics and even other quantitative extensions such as probabilistic CTL. We establish expressiveness results on our logics giving translations from weighted and probabilistic CTL into weighted MSO.

Partially supported by projects ARCUS Île de France-Inde and ANR-06-SETIN-003 DOTS.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Baier, C., Bertrand, N., Größer, M.: On decision problems for probabilistic Büchi automata. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 287–301. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Baier, C., Größer, M.: Recognizing ω-regular languages with probabilistic automata. In: Proceedings of LICS 2005, pp. 137–146. IEEE Computer Society Press, Los Alamitos (2005)

    Google Scholar 

  5. Bollig, B., Leucker, M.: Verifying qualitative properties of probabilistic programs. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 124–146. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Buchholz, P., Kemper, P.: Model checking for a class of weighted automata. Discrete Event Dynamic Systems (to appear, 2009)

    Google Scholar 

  8. Büchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66–92 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  9. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the International Congress on Logic, Methodology and Philosophy, pp. 1–11. Standford University Press (1962)

    Google Scholar 

  10. Ciesinski, F., Größer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Clarke, E.M., Emerson, E.A.: 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)

    Chapter  Google Scholar 

  12. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  13. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  14. Culik, K., Kari, J.: Image compression using weighted finite automata. Computer and Graphics 17(3), 305–313 (1993)

    Article  Google Scholar 

  15. de Alfaro, L.: Formal verification of probabilistic systems. Technical report, Stanford University, PhD thesis (1998)

    Google Scholar 

  16. Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoretical Computer Science 380(1-2), 69–86 (2007); Special issue of ICALP 2005

    Article  MathSciNet  MATH  Google Scholar 

  17. Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Kuich, W., Vogler, H., Droste, M. (eds.) Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (to appear, 2009)

    Chapter  Google Scholar 

  18. Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. In: Holub, J., Žďárek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 73–84. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Droste, M., Vogler, H.: Weighted tree automata and weighted logics. Theoretical Computer Science 366(3), 228–247 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  20. Eisner, J.: Expectation semirings: Flexible EM for learning finite-state transducers. In: Proceedings of the ESSLLI workshop on finite-state methods in NLP (2001)

    Google Scholar 

  21. Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–52 (1961)

    Article  MathSciNet  MATH  Google Scholar 

  22. Fischer, D., Grädel, E., Kaiser, L.: Model checking games for the quantitative μ-calculus. Theory of Computing Systems (2009); Special Issue of STACS 2008

    Google Scholar 

  23. Größer, M., Norman, G., Baier, C., Ciesinski, F., Kwiatkowska, M., Parker, D.: On reduction criteria for probabilistic reward models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 309–320. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

  25. Knopp, K.: Theory and Application of Infinite Series. Dover Publications, New York (1990); Republication of the second English edn. (1951)

    MATH  Google Scholar 

  26. Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  27. Kuich, W., Salomaa, A.: Semirings, Automata and Languages. Springer, Heidelberg (1985)

    MATH  Google Scholar 

  28. Kuich, W., Vogler, H., Droste, M. (eds.): Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2009)

    MATH  Google Scholar 

  29. Meinecke, I.: A weighted μ-calculus on words. In: Diekert, V., Nowotka, D. (eds.) DLT 2009. LNCS, vol. 5583. Springer, Heidelberg (2009)

    Google Scholar 

  30. Mohri, M.: Finite-state transducers in language and speech processing. Computational Linguistics 23(2), 269–311 (1997)

    MathSciNet  Google Scholar 

  31. Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS 1977, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)

    Google Scholar 

  32. Puterman, M.L.: Markov Decision Processes. John Wiley & Sons, Inc., New York (1994)

    Book  MATH  Google Scholar 

  33. Rabin, M.O.: Probabilistic automata. Information and Control 6, 230–245 (1963)

    Article  MATH  Google Scholar 

  34. Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64–78. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  35. Thomas, W.: Languages, automata and logic. In: Salomaa, A., Rozenberg, G. (eds.) Handbook of Formal Languages. Beyond Words, vol. 3, pp. 389–455. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  36. van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Information and Computation 121(1), 59–80 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  37. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS 1985, pp. 327–338. IEEE, Los Alamitos (1985)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan, CNRS, INRIA Saclay, France

    Benedikt Bollig & Paul Gastin

Authors
  1. Benedikt Bollig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul Gastin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Formale Methoden der Informatik, FMI, Universität Stuttgart, Universitätsstrasse 38, 70569, Stuttgart, Germany

    Volker Diekert  & Dirk Nowotka  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bollig, B., Gastin, P. (2009). Weighted versus Probabilistic Logics. In: Diekert, V., Nowotka, D. (eds) Developments in Language Theory. DLT 2009. Lecture Notes in Computer Science, vol 5583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02737-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02737-6_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02736-9

  • Online ISBN: 978-3-642-02737-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation