Probabilistic Timed Automata with Clock-Dependent Probabilities

• Autorzy: Sproston Jeremy

Identyfikatory

DOI

10.3233/FI-2021-2000

• Języki publikacji: EN

Abstrakty

EN

Probabilistic timed automata are classical timed automata extended with discrete probability distributions over edges. We introduce clock-dependent probabilistic timed automata, a variant of probabilistic timed automata in which transition probabilities can depend linearly on clock values. Clock-dependent probabilistic timed automata allow the modelling of a continuous relationship between time passage and the likelihood of system events. We show that the problem of deciding whether the maximum probability of reaching a certain location is above a threshold is undecidable for clock-dependent probabilistic timed automata. On the positive side, we show that the maximum and minimum probability of reaching a certain location in clock-dependent probabilistic timed automata can be approximated using a region-graph-based approach.

Słowa kluczowe

EN

probabilistic model checking; timed automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 178, nr 1/2
• Strony: 101--138
• Opis fizyczny: Bibliogr. 24 poz., rys., wykr.

Twórcy

autor

Sproston Jeremy

• Dipartimento di Informatica, University of Turin, Italy

Bibliografia

• [1] Gregersen H, Jensen HE. Formal Design of Reliable Real Time Systems. Master’s thesis, Department of Mathematics and Computer Science, Aalborg University, 1995. ID: 61083485.
• [2] Kwiatkowska M, Norman G, Segala R, Sproston J. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 2002. 286:101-150. doi:10.1016/S0304-3975(01)00046-9.
• [3] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994. 126(2):183-235. doi:10.1016/0304-3975(94)90010-8.
• [4] Puterman ML. Markov Decision Processes. J. Wiley & Sons, 1994. ISBN:9780471619772, 9780470316887.
• [5] Segala R. Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, Massachusetts Institute of Technology, 1995.
• [6] Kwiatkowska M, Norman G, Parker D, Sproston J. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. Formal Methods in System Design, 2006. 29:33-78. doi:10.1007/s10703-006-0005-2.
• [7] Norman G, Parker D, Sproston J. Model Checking for Probabilistic Timed Automata. Formal Methods in System Design, 2013. 43(2):164-190. doi:10.1007/s10703-012-0177-x.
• [8] Abate A, Katoen J, Lygeros J, Prandini M. Approximate Model Checking of Stochastic Hybrid Systems. European Journal of Control, 2010. 16(6):624-641. doi:10.3166/ejc.16.624-641.
• [9] Akshay S, Bouyer P, Krishna SN, Manasa L, Trivedi A. Stochastic Timed Games Revisited. In: Proc. 41st International Symposium on Mathematical Foundations of Computer Science (MFCS’16), volume 58 of LIPIcs. Leibniz-Zentrum für Informatik, 2016 pp. 8:1-8:14. doi:10.4230/LIPIcs.MFCS.2016.8.
• [10] Bouyer P, Brinksma E, Larsen KG. Optimal Infinite Scheduling for Multi-Priced Timed Automata. Formal Methods in System Design, 2008. 32(1):2-23. doi:10.1007/s10703-007-0043-4.
• [11] Sproston J. Probabilistic Timed Automata with Clock-Dependent Probabilities. In: Hague M, Potapov I (eds.), Proc. RP 2017, volume 10506 of LNCS. Springer, 2017 pp. 144-159. doi:10.1007/978-3-319-67089-8_11.
• [12] Hahn EM. Model checking stochastic hybrid systems. Ph.D. thesis, Universität des Saarlandes, 2013.
• [13] Kemeny JG, Snell JL, Knapp AW. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer, 2nd edition, 1976.
• [14] Jurdziński M, Laroussinie F, Sproston J. Model Checking Probabilistic Timed Automata with One or Two Clocks. Logical Methods in Computer Science, 2008. 4(3):1-28. doi:10.2168/LMCS-4(3:12)2008.
• [15] Minsky M. Computation: Finite and Infinite Machines. Prentice Hall International, 1967.
• [16] Bouyer P. On the optimal reachability problem in weighted timed automata and games. In: Proc. 7th Workshop on Non-Classical Models of Automata and Applications (NCMA’15), volume 318 of [e-mail]. Austrian Computer Society, 2015 pp. 11-36.
• [17] Desharnais J, Laviolette F, Tracol M. Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games. In: Proc. 5th International Conference on the Quantitative Evaluaiton of Systems (QEST’08). IEEE Computer Society, 2008 pp. 264-273. doi:10.1109/QEST.2008.42.
• [18] Bian G, Abate A. On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context. In: Proc. of the 20th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’17), volume 10203 of LNCS. 2017 pp. 321-337. doi:10.1007/978-3-662-54458-7_19.
• [19] Tripakis S, Yovine S, Bouajjani A. Checking Timed Büchi Automata Emptiness Efficiently. Formal Methods in System Design, 2005. 26(3):267-292. doi:10.1007/s10703-005-1632-8.
• [20] Baier C, Katoen J. Principles of model checking. MIT Press, 2008.
• [21] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS. Springer, 2011 pp. 585-591. doi:10.1007/978-3-642-22110-1_47.
• [22] Sproston J. Qualitative Reachability for Open Interval Markov Chains. In: Potapov I, Reynier PA (eds.), Proc. RP 2018, volume 11123 of LNCS. Springer, 2018 pp. 146-160. doi:10.1007/978-3-030-00250-3_11.
• [23] Basset N, Asarin E. Thin and Thick Timed Regular Languages. In: Proc. of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS’11), volume 6919 of LNCS. Springer, 2011 pp. 113-128. doi:10.1007/978-3-642-24310-3_9.
• [24] Bohnenkamp HC, D’Argenio PR, Hermanns H, Katoen J. MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE Transactions on Software Engineering, 2006. 32(10):812-830. doi:10.1109/TSE.2006.104.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).