Geodesic
Minimization of probabilistic models of programs
Fundamentalʹnaâ i prikladnaâ matematika, Tome 19 (2014) no. 1, pp. 121-163.

Voir la notice de l'article provenant de la source Math-Net.Ru

In this paper, we consider a problem of reduction of probabilistic transition systems (PTS) in order to reduce the complexity of model checking of such systems. The problem of model checking of a PTS is to calculate truth values of formulas of the probabilistic temporal logic PCTL in an initial state of the PTS. We introduce a concept of equivalence of states of a PTS, and represent an algorithm for removing equivalent states. A result of this algorithm is a PTS such that all its properties expressed by formulas of PCTL coincide with those of the original PTS. 
@article{FPM_2014_19_1_a6,
     author = {A. M. Mironov and S. L. Frenkel},
     title = {Minimization of probabilistic models of programs},
     journal = {Fundamentalʹna\^a i prikladna\^a matematika},
     pages = {121--163},
     publisher = {mathdoc},
     volume = {19},
     number = {1},
     year = {2014},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/FPM_2014_19_1_a6/}
}
TY  - JOUR
AU  - A. M. Mironov
AU  - S. L. Frenkel
TI  - Minimization of probabilistic models of programs
JO  - Fundamentalʹnaâ i prikladnaâ matematika
PY  - 2014
SP  - 121
EP  - 163
VL  - 19
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/FPM_2014_19_1_a6/
LA  - ru
ID  - FPM_2014_19_1_a6
ER  - 
%0 Journal Article
%A A. M. Mironov
%A S. L. Frenkel
%T Minimization of probabilistic models of programs
%J Fundamentalʹnaâ i prikladnaâ matematika
%D 2014
%P 121-163
%V 19
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/FPM_2014_19_1_a6/
%G ru
%F FPM_2014_19_1_a6
A. M. Mironov; S. L. Frenkel. Minimization of probabilistic models of programs. Fundamentalʹnaâ i prikladnaâ matematika, Tome 19 (2014) no. 1, pp. 121-163. http://geodesic.mathdoc.fr/item/FPM_2014_19_1_a6/

[1] Bukharaev R. G., Osnovy teorii veroyatnostnykh avtomatov, Nauka, M., 1985 | MR | Zbl

[2] Kemeni Dzh., Snell Dzh., Konechnye tsepi Markova, Nauka, M., 1970

[3] Klark E. M., Gramberg O., Peled D., Verifikatsiya modelei programm. Model Checking, MTsNMO, M., 2002

[4] De Alfaro L., Kwiatkowska M., Norman G., Parker D., Segala R., “Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation”, Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), Lect. Notes Comput. Sci., 1785, eds. S. Graf, M. Schwartzbach, Springer, Berlin, 2000, 395–410 | DOI | Zbl

[5] D'Argenio P., Niebert P., “Partial order reduction on concurrent probabilistic programs”, Proc. 1st Int. Conf. on Quantitative Evaluation of Systems (QEST'04), IEEE Comput. Sci. Press, 2004, 240–249 | DOI

[6] Baier C., Clarke E., Hartonas-Garmhausen V., Kwiatkowska M., Ryan M., “Symbolic model checking for probabilistic processes”, Proc. 24th Int. Colloq. on Automata, Languages and Programming (ICALP' 97), Lect. Notes Comput. Sci., 1256, eds. P. Degano, R. Gorrieri, A. Marchetti-Spaccamela, Springer, Berlin, 1997, 430–440 | DOI | MR

[7] Baier C., Grösser M., Ciesinski F., “Partial order reduction for probabilistic systems”, Proc. 1st Int. Conf. on Quantitative Evaluation of Systems (QEST' 04), IEEE Comput. Sci. Press, 2004, 230–239 | DOI

[8] Baier C., Haverkort B., Hermanns H., Katoen J.-P., “Model-checking algorithms for continuous-time Markov chains”, IEEE Trans. Software Engineering, 29:6 (2003), 524–541 | DOI

[9] Bianco A., de Alfaro L., “Model checking of probabilistic and nondeterministic systems”, Proc. 15th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS' 95), Lect. Notes Comput. Sci., 1026, ed. P. Thiagarajan, Springer, Berlin, 1995, 499–513 | DOI | MR

[10] Courcoubetis C., Yannakakis M., “Verifying temporal properties of finite state probabilistic programs”, Proc. 29th Annual Symp. on Foundations of Computer Science (FOCS' 88), IEEE Comput. Soc. Press, 1988, 338–345

[11] Donaldson A., Miller A., “Symmetry reduction for probabilistic model checking using generic representatives”, Proc. 4th Int. Symp. Automated Technology for Verification and Analysis (ATVA' 06), Lect. Notes Comput. Sci., 4218, eds. S. Graf, W. Zhang, Springer, Berlin, 2006, 9–23 | DOI | MR | Zbl

[12] Hansson H., Time and Probability in Formal Design of Distributed Systems, Elsevier, Amsterdam, 1994

[13] Hansson H., Jonsson B., “A logic for reasoning about time and reliability”, Formal Aspects Computing, 6:5 (1994), 512–535 | DOI | Zbl

[14] Hart S., Sharir M., Pnueli A., “Termination of probabilistic concurrent programs”, ACM Trans. Programming Languages Systems, 5:3 (1983), 356–380 | DOI | Zbl

[15] Hermanns H., Katoen J.-P., Meyer-Kayser J., Siegle M., “A Markov chain model checker”, Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS' 00), Lect. Notes Comput. Sci., 1785, eds. S. Graf, M. Schwartzbach, Springer, Berlin, 2000, 347–362 | DOI | Zbl

[16] Kwiatkowska M., Norman G., Parker D., “Probabilistic model checking in practice: Case studies with PRISM”, ACM SIGMETRICS Performance Evaluation Review, 32:4 (2005), 16–21 | DOI

[17] Kwiatkowska M., Norman G., Parker D., “Symmetry reduction for probabilistic model checking”, Proc. 18th Int. Conf. on Computer Aided Verification (CAV' 06), Lect. Notes Comput. Sci., 4114, eds. T. Ball, R. Jones, Springer, Berlin, 2006, 234–248 | DOI | MR

[18] Kwiatkowska M., Norman G., Parker D., “PRISM 4.0: Verification of probabilistic real-time systems”, Proc. 23rd Int. Conf. on Computer Aided Verification (CAV' 11), Lect. Notes Comput. Sci., 6806, eds. G. Gopalakrishnan, S. Qadeer, Springer, Berlin, 2011, 585–591 | DOI | MR

[19] Kwiatkowska M., Parker D., Advances in Probabilistic Model Checking, http://qav.comlab.ox.ac.uk/papers/marktoberdorf11.pdf

[20] http://www.prismmodelchecker.org/

[21] http://qav.comlab.ox.ac.uk/

[22] Vardi M., “Automatic verification of probabilistic concurrent finite state programs”, Proc. 26th Annual Symp. on Foundations of Computer Science (FOCS' 85), IEEE Comput. Soc. Press, 1985, 327–338