Abstract
A continuous-time Markov chain (CTMC) execution is a continuous class of probability distributions over states. This paper proposes a probabilistic linear-time temporal logic, namely continuous-time linear logic (CLL), to reason about the probability distribution execution of CTMCs. We define the syntax of CLL on the space of probability distributions. The syntax of CLL includes multiphase timed until formulas, and the semantics of CLL allows time reset to study relatively temporal properties. We derive a corresponding model-checking algorithm for CLL formulas. The correctness of the model-checking algorithm depends on Schanuel’s conjecture, a central open problem in transcendental number theory. Furthermore, we provide a running example of CTMCs to illustrate our method.
Chapter PDF
Similar content being viewed by others
References
Achatz, M., McCallum, S., Weispfenning, V.: Deciding polynomial-exponential problems. In: Proceedings of the Twenty-first International Symposium on Symbolic and Algebraic Computation. pp. 215–222. ACM (2008)
Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.: Approximate verification of the symbolic dynamics of Markov chains. Journal of the ACM (JACM) 62(1), Â 2 (2015)
Akshay, S., Antonopoulos, T., Ouaknine, J., Worrell, J.: Reachability problems for Markov chains. Information Processing Letters 115(2), 155–158 (2015)
Almagor, S., Kelmendi, E., Ouaknine, J., Worrell, J.: Invariants for continuous linear dynamical systems. arXiv preprint arXiv:2004.11661 (2020)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proceedings of the Twenty-fifth Annual ACM Symposium on Theory of Computing. pp. 592–601 (1993)
Avellar, C.E., Hale, J.K.: On the zeros of exponential polynomials. Journal of Mathematical Analysis and Applications 73(2), 434–452 (1980)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003)
Baker, A.: Transcendental number theory. Cambridge university press (1990)
Barbot, B., Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 128–142. Springer (2011)
Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: International Conference on Formal Modeling and Analysis of Timed Systems. pp. 26–42. Springer (2011)
Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science. pp. 309–318. IEEE (2009)
Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science 7(1) (Mar 2011)
Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Observing continuous-time MDPs by 1-clock timed automata. In: International Workshop on Reachability Problems. pp. 2–25. Springer (2011)
Chonev, V., Ouaknine, J., Worrell, J.: On the skolem problem for continuous linear dynamical systems. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 55, pp. 100:1–100:13. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2016)
Cohen, H.: A course in computational algebraic number theory, vol. 138. Springer Science & Business Media (2013)
Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A STORM is coming: A modern probabilistic model checker. In: International Conference on Computer Aided Verification. pp. 592–600. Springer (2017)
Feng, Y., Katoen, J.P., Li, H., Xia, B., Zhan, N.: Monitoring CTMCs by multi-clock timed automata. In: International Conference on Computer Aided Verification. pp. 507–526. Springer (2018)
Gan, T., Chen, M., Li, Y., Xia, B., Zhan, N.: Reachability analysis for solvable dynamical systems. IEEE Transactions on Automatic Control 63(7), 2003–2018 (2017)
Guan, J., Yu, N.: A probabilistic logic for verifying continuous-time markov chains. arXiv preprint arXiv:2004.08059 (2020)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Katoen, J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 31–45. ACM (2016)
Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68(2), 90–104 (2011)
Kolmogoroff, A.: Über die analytischen methoden in der wahrscheinlichkeitsrechnung. Mathematische Annalen 104(1), 415–458 (1931)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: International Conference on Modelling Techniques and Tools for Computer Performance Evaluation. pp. 200–204. Springer (2002)
Lang, S.: Introduction to transcendental numbers. Addison-Wesley Pub. Co. (1966)
Li, J.C., Huang, C.C., Xu, M., Li, Z.B.: Positive root isolation for poly-powers. In: Proceedings of the ACM on International Symposium on Symbolic and Algebraic Computation. pp. 325–332. ACM (2016)
Macintyre, A., Wilkie, A.J.: On the decidability of the real exponential field (1996)
Majumdar, R., Salamati, M., Soudjani, S.: On decidability of time-bounded reachability in CTMDPs. In: Czumaj, A., Dawar, A., Merelli, E. (eds.) 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 168, pp. 133:1–133:19. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020)
Nesterenko, Y.: Modular functions and transcendence problems. Comptes rendus de l’Académie des sciences. Série 1, Mathématique 322(10), 909–914 (1996)
Ouaknine, J., Worrell, J.: Decision problems for linear recurrence sequences. In: International Workshop on Reachability Problems. pp. 21–28. Springer (2012)
Richardson, D.: How to recognize zero. Journal of Symbolic Computation 24(6), 627–645 (1997)
Ritt, J.F.: On the zeros of exponential polynomials. Transactions of the American Mathematical Society 31(4), 680–686 (1929)
Strzebonski, A.: Real root isolation for exp-log functions. In: Proceedings of the Twenty-first International Symposium on Symbolic and Algebraic Computation. pp. 303–314 (2008)
Strzebonski, A.: Real root isolation for tame elementary functions. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation. pp. 341–350 (2009)
Terzo, G.: Some consequences of Schanuel’s conjecture in exponential rings. Communications in Algebra® 36(3), 1171–1189 (2008)
Tijdeman, R.: On the number of zeros of general exponential polynomials. In: Indagationes Mathematicae (Proceedings). vol. 74, pp. 1–7. North-Holland (1971)
Xu, M., Deng, Y.: Time-bounded termination analysis for probabilistic programs with delays. Information and Computation 275, 104634 (2020)
Xu, M., Mei, J., Guan, J., Yu, N.: Model checking quantum continuous-time Markov chains. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 203, pp. 13:1–13:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2021)
Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Automata-based CSL model checking. In: International Colloquium on Automata, Languages, and Programming. pp. 271–282. Springer (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Guan, J., Yu, N. (2022). A Probabilistic Logic for Verifying Continuous-time Markov Chains. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)