Extrapolation of an Optimal Policy using Statistical Probabilistic Model Checking

• Autorzy: Rataj A. , Woźna-Szcześniak B.

Identyfikatory

DOI

10.3233/FI-2018-1637

• Języki publikacji: EN

Abstrakty

EN

We present different ways of an approximate extrapolation of an optimal policy of a small model to that of a large equivalent of the model, which itself is too large to find its exact policy directly using probabilistic model checking (PMC). In particular, we obtain a global optimal resolution of non-determinism in several small Markov Decision Processes (MDP) or its extensions like Stochastic Multi-player Games (SMG) using PMC. We then use that resolution to form a hypothesis about an analytic decision boundary representing a respective policy in an equivalent large MDP/SMG. The resulting hypothetical decision boundary is then statistically approximately verified, if it is locally optimal and if it indeed represents a “good enough” policy. The verification either weakens or strengthens the hypothesis. The criterion of the optimality of the policy can be expressed in any modal logic that includes a version of the probabilistic operator P~p[·], and for which a PMC method exists.

Słowa kluczowe

EN

extrapolation; non-determinism; optimal policy; probabilistic model checking; statistical model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 157, nr 4
• Strony: 443--461
• Opis fizyczny: Bibliogr. 23 poz., rys., tab., wykr.

Twórcy

autor

Rataj A.

• IITiS, Polish Academy of Sciences, ul. Bałtycka 5, 44-100 Gliwice, Poland

autor

Woźna-Szcześniak B.

• IMCS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] Alur R, Henzinger T, and Kupferman O. Alternating-time temporal logic. Journal of the ACM 2002; 49(5):672-713. doi:10.1145/585265.585270.
• [2] Chen T, Forejt V, Kwiatkowska M, Parker D, and Simaitis A. Automatic verification of competitive stochastic systems. Formal Methods in System Design 2013;43(1):61-92. doi:10.1007/s10703-013-0183-7.
• [3] Chen T, Forejt V, Kwiatkowska M, Parker D, and Simaitis A. PRISM-games: A model checker for stochastic multi-player games. In: Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13), LNCS, vol. 7795, Springer 2013 pp. 185-191. URL https://doi.org/10.1007/978-3-642-36742-7_13.
• [4] Chen T, Forejt V, Kwiatkowska M, Parker D, and Simaitis A. PRISM-games: A model checker for stochastic multi-player games. In: Proc. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13), LNCS, vol. 7795, Springer 2013 pp. 185-191. URL https://doi.org/10.1007/978-3-642-36742-7_13.
• [5] Chen T, Lu J. Probabilistic alternating-time temporal logic and model checking algorithm. In: Proceedings of the Fourth International Conference on Fuzzy Systems and Knowledge Discovery-vol. 02, FSKD ’07, pp. 35-39. IEEE Computer Society 2007. doi:10.1109/FSKD.2007.458.
• [6] Clarke EM, Grumberg O, and Peled D. Model checking. MIT press 1999. ISBN:0-262-03270-8.
• [7] Dijkstra EW. Hierarchical ordering of sequential processes. Acta Informatica 1971;1(2):115-138. URL https://doi.org/10.1007/BF00289519.
• [8] Forejt V, Kwiatkowska M, Norman G, and Parker D. Automated verification techniques for probabilistic systems. In: Proceedings of the 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM’2011), vol. 6659 of LNCS. Springer 2011 pp. 53-113. doi:10.1007/978-3-642-21455-4_3.
• [9] Hansen N, Müller SD, and Koumoutsakos P. Reducing the time complexity of the derandomized evolution strategy with covariance matrix adaptation (cma-es). Evolutionary computation 2003;11(1):1-18. doi:10.1162/106365603321828970.
• [10] Hansson H, and Jonsson B. A logic for reasoning about time and reliability. Formal aspects of computing 1994;6(5):512-535. URL https://doi.org/10.1007/BF01211866.
• [11] Kwiatkowska M, Norman G, and Parker D. Advances and challenges of probabilistic model checking. In: Proc. of 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton), IEEE 2010 pp. 1691-1698. doi:10.1109/ALLERTON.2010.5707120.
• [12] Kwiatkowska M, Norman G, and Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In: Proc. 23rd International Conference on Computer Aided Verification (CAV’11), vol. 6806 of LNCS, Springer 2011 pp. 585-591. URL https://doi.org/10.1007/978-3-642-22110-1_47.
• [13] Kwiatkowska M, and Parker D. Advances in probabilistic model checking. In: Software Safety and Security-Tools for Analysis and Verification, NATO Science for Peace and Security Series-D: Information and Communication Security, IOS Press 2012 vol. 33, pp. 126-151. URL https://hal.inria.fr/hal-00664777.
• [14] Kwiatkowska M, and Parker D. Automated verification and strategy synthesis for probabilistic systems. In: Proc. 11th International Symposium on Automated Technology for Verification and Analysis (ATVA’13), vol. 8172 of LNCS, Springer 2013 pp. 5-22. URL https://doi.org/10.1007/978-3-319-02444-8_2.
• [15] Legay A, Delahaye B, and Bensalem, S. Statistical model checking: An overview. In: International Conference on Runtime Verification, Springer 2010 pp. 122-135. URL https://doi.org/10.1007/978-3-642-16612-9_11.
• [16] Nelder JA, Mead R. A Simplex Method for Function Minimization. The Computer Journal 1965;7(4):308-313. doi:10.1093/comjnl/7.4.308.
• [17] Nimal V. Statistical Approaches for Probabilistic Model Checking. Master’s thesis, Oxford University 2010.
• [18] Powell MJ. The bobyqa algorithm for bound constrained optimization without derivatives. Cambridge NA Report NA2009/06, University of Cambridge, Cambridge 2009.
• [19] Rataj A. More flexible models using a new version of the translator of Java sources to timed automatons J2TADD. Theoretical and Applied Informatics 2009;21(2):107-114.
• [20] Rataj A. Fractional genetic programming for a more gradual evolution. In: Proceedings of the 22nd International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, 2013 pp. 371-382.
• [21] Rataj A, Wozna B, and Zbrzezny, A. A translator of Java programs to TADDs. Fundamenta Informaticae 2009;93(1-3):305-324. doi:10.3233/FI-2009-0104.
• [22] Sondik EJ. The optimal control of partially observable markov processes. Tech. rep., DTIC Document 1971.
• [23] Younes H, Kwiatkowska M, Norman G, and Parker D. Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT) 2006;8(3):216-228. URL https://doi.org/10.1007/s10009-005-0187-8.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).