Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

Taolue Chen; Tingting Han; Joost-Pieter Katoen; Alexandru Mereacre

doi:10.2168/LMCS-7(1:12)2011

Taolue Chen ; Tingting Han ; Joost-Pieter Katoen ; Alexandru Mereacre - Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

lmcs:697 - Logical Methods in Computer Science, March 29, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:12)2011

Model Checking of Continuous-Time Markov Chains Against Timed Automata SpecificationsArticle

Authors: Taolue Chen ; Tingting Han ; Joost-Pieter Katoen ; Alexandru Mereacre

We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.

https://doi.org/10.2168/LMCS-7(1:12)2011

Source: arXiv.org:1101.3694

Volume: Volume 7, Issue 1

Published on: March 29, 2011

Imported on: December 25, 2009

Keywords: Computer Science - Logic in Computer Science,D.2.4

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Modeling, verification and control of complex systems: From foundations to power network applications; Funder: European Commission; Code: 257005

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Publications

Has review

Review available on zbMATH Open, by Gabriel V. Orman (Braşov) (English)

1 zbMATH Open

Bibliographic References

31 Documents citing this article

Anton Hampus;Mattias Nyberg, 2024, Formally verifying decompositions of stochastic specifications, International Journal on Software Tools for Technology Transfer, 26, 2, pp. 207-228, 10.1007/s10009-024-00742-5, https://doi.org/10.1007/s10009-024-00742-5.

Anton Hampus;Mattias Nyberg, Lecture notes in computer science, Verifying Refinement of Probabilistic Contracts Using Timed Automata, pp. 95-113, 2023, 10.1007/978-3-031-35257-7_6.

Anton Hampus;Mattias Nyberg, Lecture notes in computer science, Formally Verifying Decompositions of Stochastic Specifications, pp. 193-210, 2022, 10.1007/978-3-031-15008-1_13.

Ji Guan;Nengkun Yu, Lecture notes in computer science, A Probabilistic Logic for Verifying Continuous-time Markov Chains, pp. 3-21, 2022, 10.1007/978-3-030-99527-0_1, https://doi.org/10.1007/978-3-030-99527-0_1.

Susmoy Das;Arpit Sharma, Lecture notes in computer science, State Space Minimization Preserving Embeddings for Continuous-Time Markov Chains, pp. 44-61, 2021, 10.1007/978-3-030-91825-5_3.

Arpit Sharma, 2020, The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism, Theoretical Computer Science, 850, pp. 148-167, 10.1016/j.tcs.2020.11.001.

Susanna Donatelli;Serge Haddad, Lecture notes in computer science, Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models, pp. 170-183, 2020, 10.1007/978-3-030-40608-0_11, https://doi.org/10.1007/978-3-030-40608-0_11.

E.G. Amparore;S. Donatelli, 2018, Efficient model checking of the stochastic logic CSLTA, Performance Evaluation, 123-124, pp. 1-34, 10.1016/j.peva.2018.03.002.

Hongfei Fu;Yi Li;Jianlin Li, arXiv (Cornell University), Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties, pp. 122-139, 2018, 10.1007/978-3-319-99154-2_8, http://arxiv.org/abs/1712.00275.

Kristof Marussy;Istvan Majzik, 2022 IEEE 18th International Conference on Automation Science and Engineering (CASE), Constructing Dependability Analysis Models of Reconfigurable Production Systems, pp. 1158-1163, 2018, Munich, Germany, 10.1109/coase.2018.8560551.

Yijun Feng;Joost-Pieter Katoen;Haokun Li;Bican Xia;Naijun Zhan, Lecture notes in computer science, Monitoring CTMCs by Multi-clock Timed Automata, pp. 507-526, 2018, 10.1007/978-3-319-96145-3_27.

Guoxin Su;Taolue Chen;Yuan Feng;David S. Rosenblum, 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE), ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains, 13, pp. 484-495, 2017, Buenos Aires, 10.1109/icse.2017.51.

Paolo Ballarini;Marco Beccuti;Enrico Bibbona;Andras Horvath;Roberta Sirovich;et al., Analysis of Timed Properties Using the Jump-Diffusion Approximation, pp. 69-84, 2017, 10.1007/978-3-319-66583-2_5, https://hal.archives-ouvertes.fr/hal-01817472.

Joost-Pieter Katoen, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, The Probabilistic Model Checking Landscape, 2016, New York NY USA, 10.1145/2933575.2934574.

Sadegh Esmaeil Zadeh Soudjani;Rupak Majumdar;Alessandro Abate, Oxford University Research Archive (ORA) (University of Oxford), Safety Verification of Continuous-Space Pure Jump Markov Processes, pp. 147-163, 2016, 10.1007/978-3-662-49674-9_9, https://ora.ox.ac.uk/objects/uuid:9e7778d1-49b2-4467-8b5e-08d66c7f7278.

Giorgio Bacci;Giovanni Bacci;Kim Guldstrand Larsen;Radu Mardare, Lecture notes in computer science, On the Total Variation Distance of Semi-Markov Chains, pp. 185-199, 2015, 10.1007/978-3-662-46678-0_12, https://doi.org/10.1007/978-3-662-46678-0_12.

Luca Bortolussi;Jane Hillston, 2015, Model checking single agent behaviours by fluid approximation, Information and Computation, 242, pp. 183-226, 10.1016/j.ic.2015.03.002, https://doi.org/10.1016/j.ic.2015.03.002.

Luca Bortolussi;Roberta Lanciani, arXiv (Cornell University), Fluid Model Checking of Timed Properties, pp. 172-188, 2015, 10.1007/978-3-319-22975-1_12, http://arxiv.org/abs/1506.05909.

Christel Baier;Clemens Dubslaff;Joachim Klein;Sascha Klüppelholz;Sascha Wunderlich, Lecture notes in computer science, Probabilistic Model Checking for Energy-Utility Analysis, pp. 96-123, 2014, 10.1007/978-3-319-06880-0_5.

Elvio Gilberto Amparore;Susanna Donatelli, Institutional Research Information System University of Turin (University of Turin), Improving and Assessing the Efficiency of the MC4CSLTA Model Checker, pp. 206-220, 2013, 10.1007/978-3-642-40725-3_16, http://hdl.handle.net/2318/1624731.

Elvio Gilberto Amparore;Susanna Donatelli, 2013, A component-based solution for reducible Markov regenerative processes, Performance Evaluation, 70, 6, pp. 400-422, 10.1016/j.peva.2013.02.002.

Hongfei Fu, arXiv (Cornell University), Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata, 2013, Philadelphia Pennsylvania USA, 10.1145/2461328.2461376, https://arxiv.org/abs/1210.4787.

Luca Bortolussi;Jane Hillston, Edinburgh Research Explorer (University of Edinburgh), Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation, pp. 113-149, 2013, 10.1007/978-3-642-38874-3_4, http://hdl.handle.net/20.500.11820/dfc05e9d-0cdf-41fb-b4d3-9f78691ecafb.

Luca Bortolussi;Roberta Lanciani, Lecture notes in computer science, Model Checking Markov Population Models by Central Limit Approximation, pp. 123-138, 2013, 10.1007/978-3-642-40196-1_9.

Taolue Chen;Marco Diciolla;Marta Kwiatkowska;Alexandru Mereacre, 2013, Verification of linear duration properties over continuous-time markov chains, ACM Transactions on Computational Logic, 14, 4, pp. 1-35, 10.1145/2528935.

Joost-Pieter Katoen, 2012 12th International Conference on Application of Concurrency to System Design, GSPNs Revisited: Simple Semantics and New Analysis Algorithms, pp. 6-11, 2012, Hamburg, TBD, Germany, 10.1109/acsd.2012.30.

Linar Mikeev;Martin R. Neuhäußer;David Spieler;Verena Wolf, 2012, On-the-fly verification and optimization of DTA-properties for large Markov chains, Formal Methods in System Design, 43, 2, pp. 313-337, 10.1007/s10703-012-0165-1.

Luminita Manuela Bujorianu, Communications and control engineering/Communications and control engineering series, Hybrid Systems: Deterministic to Stochastic Perspectives, pp. 31-53, 2012, 10.1007/978-1-4471-2795-6_3.

Patricia Bouyer;Thomas Brihaye;Marcin Jurdzinski;Quentin Menet, CiteSeer X (The Pennsylvania State University), Almost-Sure Model-Checking of Reactive Timed Automata, pp. 138-147, 2012, London, United Kingdom, 10.1109/qest.2012.10, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397.63.

Yang Gao;Ming Xu;Naijun Zhan;Lijun Zhang, 2012, Model checking conditional CSL for continuous-time Markov chains, Technical University of Denmark, DTU Orbit (Technical University of Denmark, DTU), 113, 1-2, pp. 44-50, 10.1016/j.ipl.2012.09.009, https://orbit.dtu.dk/en/publications/c81f9b57-e7d3-4029-a3c5-f831d4ee8eb2.

Taolue Chen;Tingting Han;Joost-Pieter Katoen;Alexandru Mereacre, CiteSeer X (The Pennsylvania State University), Reachability probabilities in Markovian Timed Automata, pp. 7075-7080, 2011, Orlando, FL, USA, 10.1109/cdc.2011.6160992, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.728.1301.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1813 times.

This article's PDF has been downloaded 791 times.