Document Open Access Logo

On Frequency LTL in Probabilistic Systems

Authors Vojtech Forejt, Jan Krcal

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.184.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Vojtech Forejt
Jan Krcal

Cite AsGet BibTex

Vojtech Forejt and Jan Krcal. On Frequency LTL in Probabilistic Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 184-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.184

Abstract

We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator G^p expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended "until" and "globally" operator, leading to undecidability of most interesting problems. For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound p to be 1 and negations not to be outside any G^p operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.
Keywords
  • Markov chains
  • Markov decision processes
  • LTL
  • controller synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking continuous-time Markov chains by transient analysis. In CAV, volume 1855 of LNCS. Springer, 2000. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. Weight monitoring with linear temporal logic: Complexity and decidability. In CSL-LICS, page 11. ACM, 2014. Google Scholar
  4. Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In CAV, pages 140-156. Springer, 2009. Google Scholar
  5. Udi Boker, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. In LICS 2011, pages 43-52. IEEE, 2011. Google Scholar
  6. Benedikt Bollig, Normann Decker, and Martin Leucker. Frequency linear-time temporal logic. In TASE'12, pages 85-92, Beijing, China, July 2012. IEEE Computer Society Press. Google Scholar
  7. Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014, volume 8704 of LNCS, pages 266-280. Springer, 2014. Google Scholar
  8. Tomáš Brázdil, Vojtěch Forejt, and Antonín Kučera. Controller synthesis and verification for markov decision processes with qualitative branching time objectives. In ICALP 2008, volume 5126 of LNCS, pages 148-159. Springer, 2008. Google Scholar
  9. Krishnendu Chatterjee and Laurent Doyen. Energy and mean-payoff parity Markov decision processes. In MFCS 2011, pages 206-218. Springer, 2011. Google Scholar
  10. Krishnendu Chatterjee and Laurent Doyen. Games and markov decision processes with mean-payoff parity and energy parity objectives. In MEMICS, pages 37-46. Springer, 2012. Google Scholar
  11. Krishnendu Chatterjee, Thomas A Henzinger, and Marcin Jurdzinski. Mean-payoff parity games. In LICS 2005, pages 178-187. IEEE, 2005. Google Scholar
  12. Kai-lai Chung. A Course in Probability Theory. Academic Press, 3 edition, 2001. Google Scholar
  13. Luca De Alfaro. How to specify and verify the long-run average behaviour of probabilistic systems. In LICS 1998, pages 454-465. IEEE, 1998. Google Scholar
  14. Vojtěch Forejt and Jan Krčál. On frequency LTL in probabilistic systems. CoRR, abs/1501.05561, 2015. Google Scholar
  15. J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. Springer, 2nd edition, 1976. Google Scholar
  16. Antonín Kučera and Oldřich Stražovský. On the controller synthesis for finite-state Markov decision processes. In FSTTCS 2005, pages 541-552. Springer, 2005. Google Scholar
  17. M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic verification of herman’s self-stabilisation algorithm. Formal Aspects of Computing, 24(4):661-670, 2012. Google Scholar
  18. J. R. Norris. Markov chains. Cambridge University Press, 1998. Google Scholar
  19. V. Shmatikov. Probabilistic model checking of an anonymity system. Journal of Computer Security, 12(3/4):355-377, 2004. Google Scholar
  20. Takashi Tomita, Shigeki Hagihara, and Naoki Yonezaki. A probabilistic temporal logic with frequency operators and its model checking. In INFINITY, volume 73 of EPTCS, pages 79-93, 2011. Google Scholar
  21. Takashi Tomita, Shin Hiura, Shigeki Hagihara, and Naoki Yonezaki. A temporal logic with mean-payoff constraints. In Formal Methods and Soft. Eng., volume 7635 of LNCS. Springer, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact