A GPGPU–based simulator for prism: statistical verification of results of PMC

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

Identyfikatory

DOI

10.16926/m.2017.22.07

• Języki publikacji: EN

Abstrakty

EN

We describe a GPGPU–based Monte Carlo simulator integrated with Prism. It supports Markov chains with discrete or continuous time and a subset of properties expressible in PCTL, CSL and their variants extended with rewards. The simulator allows an automated statistical verification of results obtained using Prism’s formal methods.

Słowa kluczowe

EN

GPGPU; Monte Carlo simulation; prism; probabilistic model checking; statistical model checking; probabilistic logics

PL

GPGPU; symulacja Monte Carlo; pryzmat; probabilistyczny model statystyczny

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2017
• Tom: Vol. 22
• Strony: 85--97
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Copik M.

• RWTH Aachen University, Schinkelstr. 2, 52062 Aachen, Germany

autor

Rataj A.

• Polish Academy of Sciences Institute of Theoretical and Applied Informatics ul. Bałtycka 5, 44-100 Gliwice, Poland

autor

Woźna-Szcześniak B.

• Jan Długosz University in Częstochowa Institute of Mathematics and Computer Science Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time markov chains. Transactions on Computational Logic (TOCL) 1(1), 162–170 (2000). DOI http://dx.doi.org/10.1145/343369.343402.
• [2] Chafik, O.: Javacl. https://github.com/nativelibs4java/JavaCL (2016)
• [3] Copik, M.: GPU-accelerated stochastic simulator engine for PRISM model checker. Bachelor’s Thesis, Silesian University of Technology, Gliwice, Poland (2014)
• [4] Fox, B.L., Glynn, P.W.: Computing poisson probabilities. Commun. ACM 31(4), 440–445 (1988). DOI http://dx.doi.org/10.1145/42404.42409
• [5] Gross, D., Miller, D.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research 32(2), 343–361 (1984). DOI http://dx.doi.org/10.1287/opre.32.2.343
• [6] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing 6(5), 512–535 (1994) DOI http://dx.doi.org/10.1007/ BF01211866
• [7] Herault, T., Lassaigne, R., Peyronnet, S.: Apmc 3.0: Approximate verification of discrete and continuous time markov chains. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST ’06, pp. 129–130. IEEE Computer Society, (2006). DOI http://dx.doi.org/10.1109/QEST.2006.5
• [8] Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM’07), LNCS, vol. 4486, pp. 220–270. Springer (2007)
• [9] Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: G. Gopalakrishnan, S. Qadeer (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV’11), LNCS, vol. 6806, pp. 585– 591. Springer (2011). DOI http://dx.doi.org/10.1007/978-3-642-22110-1_47
• [10] Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: International Conference on Runtime Verification, pp. 122–135. Springer (2010). DOI http://dx.doi.org/10.1007/978-3-642-16612-9_11
• [11] Pourranjbar, A., Hillston, J., Bortolussi, L.: Don’t just go with the flow: Cautionary tales of fluid flow approximation. In: Computer Performance Engineering - 9th European Workshop, pp. 156–171 (2012). DOI http://dx.doi.org/10.1007/ 978-3-642-36781-6_11
• [12] Salmon, J.K., Moraes, M.A., Dror, R.O., Shaw, D.E.: Parallel random numbers: As easy as 1, 2, 3. In: Proceedings of 2011 International Conference for High Performance Computing, Networking, Storage and Analysis, SC ’11, pp. 16:1–16:12. ACM, (2011). DOI http://dx.doi.org/10.1145/2063384.2063405.
• [13] Stone, J.E., Gohara, D., Shi, G.: OpenCL: A parallel programming standard for heterogeneous computing systems. Computing in science & engineering 12(1-3), 66– 73 (2010). DOI http://dx.doi.org/10.1109/MCSE.2010.69
• [14] Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT) 8(3), 216–228 (2006). DOI http://dx.doi.org/10.1007/ s10009-005-0187-8
• [15] Younes, H.L.S.: Ymer: A statistical model checker. In: Proceedings of the 17th International Conference on Computer Aided Verification, CAV’05, pp. 429– 433. Springer-Verlag, Berlin, Heidelberg (2005). DOI http://dx.doi.org/10.1007/ 11513988_43
• [16] Younes, H.L.S.: Ymer. https://github.com/hlsyounes/ymer (2016)