| [1] |
Andova S, Hermanns H, Katoen J-P (2003) Discrete-time rewards model-checked. In: Larsen KG, Niebert P (eds) Formal modelling and analysis of timed systems, volume 2791 of Lecture notes in computer science. Springer, pp 88-104 · Zbl 1099.68652 |
| [2] |
Aziz A, Singhal V, Balarin F (1995) It usually works: The temporal logic of stochastic systems. In: Proceedings of the 7th international conference on computer aided verification, London, UK. Springer, pp 155-165 |
| [3] |
Baier, C; Cloth, L; Haverkort, BR; Kuntz, M; Siegle, M, Model checking Markov chains with actions and state labels, IEEE Trans Softw Eng, 33, 209-224, (2007) · doi:10.1109/TSE.2007.36 |
| [4] |
Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Proceedings of the 15th conference on foundations of software technology and theoretical computer science, Berlin, Heidelberg. Springer, pp 499-513 · Zbl 1354.68167 |
| [5] |
Beaudry DM (1978) Performance-related reliability measures for computing systems. IEEE Trans Comput C-27(6):540-547 · Zbl 0377.68006 |
| [6] |
Borgerson BR, Freitas RF (1975) A reliability model for gracefully degrading and standby-sparing systems. IEEE Trans Comput C-24(5):517-525 · Zbl 0304.68056 |
| [7] |
Baier C, Haverkort BR, Hermanns H, Katoen J-P (2000) On the logical characterisation of performability properties. In: Proceedings of the 27th international colloquium on automata, languages and programming, London, UK. Springer, pp 780-792 · Zbl 0973.68014 |
| [8] |
Baier, C; Haverkort, B; Hermanns, H; Katoen, J-P, Model-checking algorithms for continuous-time Markov chains, IEEE Trans Softw Eng, 29, 524-541, (2003) · Zbl 0974.68017 · doi:10.1109/TSE.2003.1205180 |
| [9] |
Bertsekas, DP; Tsitsiklis, JN, An analysis of stochastic shortest path problems, Math Oper Res, 16, 580-595, (1991) · Zbl 0751.90077 · doi:10.1287/moor.16.3.580 |
| [10] |
Çinlar, E.: Introduction to stochastic processes. Prentice-Hall, Englewood Cliffs (1975) · Zbl 0341.60019 |
| [11] |
Clark G, Gilmore S, Hillston J (1999) Specifying performance measures for PEPA. In: Proceedings of the 5th international AMAST workshop on formal methods for real-time and probabilistic systems, London, UK. Springer, pp 211-227 |
| [12] |
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999) |
| [13] |
Chung KL (1979) Elementary probability theory with stochastic processes. Undergraduate texts in mathematics, 3rd edn. Springer, Orlando · Zbl 0404.60002 |
| [14] |
Ciardo, G; Jones, RL; Miner, AS; Siminiceanu, R, Logic and stochastic modeling with SMART, Perform Eval, 63, 578-608, (2006) · doi:10.1016/j.peva.2005.06.001 |
| [15] |
Cohn, D.L.: Measure theory. Birkhäuser, Boston (1980) · Zbl 0436.28001 · doi:10.1007/978-1-4899-0399-0 |
| [16] |
Courcoubetis, C; Yannakakis, M, The complexity of probabilistic verification, J ACM, 42, 857-907, (1995) · Zbl 0885.68109 · doi:10.1145/210332.210339 |
| [17] |
de Alfaro L (1997) Temporal logics for the specification of performance and reliability. In: Proceedings of the 14th annual symposium on theoretical aspects of computer science, London, UK. Springer, pp 165-176 · Zbl 1498.68155 |
| [18] |
de Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Proceedings of the 10th international conference on concurrency theory, London, UK. Springer, pp 66-81 · Zbl 0949.93082 |
| [19] |
Alfaro, L; Faella, M; Henzinger, TA; Majumdar, R; Stoelinga, M, Model checking discounted temporal properties, Theoret Comput Sci, 345, 139-170, (2005) · Zbl 1079.68062 · doi:10.1016/j.tcs.2005.07.033 |
| [20] |
Donatelli, S; Haddad, S; Sproston, J, Model checking timed and stochastic properties with CSL\(^{{\text{TA}}}\), IEEE Trans Softw Eng, 35, 224-240, (2009) · doi:10.1109/TSE.2008.108 |
| [21] |
Dijkstra, EW, Hierarchical ordering of sequential processes, Acta Inform, 1, 115-138, (1971) · doi:10.1007/BF00289519 |
| [22] |
Emerson EA (1990) Temporal and modal logic. In: Handbook of theoretical computer science. Elsevier, pp 995-1072 · Zbl 0900.03030 |
| [23] |
Gaonkar, S; Keefe, K; Lamprecht, R; Rozier, E; Kemper, P; Sanders, WH, Performance and dependability modeling with Möbius, SIGMETRICS Perform Eval Rev, 36, 16-21, (2009) · doi:10.1145/1530873.1530878 |
| [24] |
Grinstead CM, Snell JL (2003) Introduction to probability. American Mathematical Society |
| [25] |
Haverkort BR, Cloth L, Hermanns H, Katoen J-P (2002) Model checking performability properties. In: Proceedings of the 2002 international conference on dependable systems and networks, Washington, DC, USA. IEEE Computer Society, pp 103-112 |
| [26] |
Hansson, H; Jonsson, B, A logic for reasoning about time and reliability, Form Asp Comput, 6, 512-535, (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866 |
| [27] |
Harrison, PG; Knottenbelt, WJ, Passage time distributions in large Markov chains, SIGMETRICS Perform Eval Rev, 30, 77-85, (2002) · doi:10.1145/511399.511345 |
| [28] |
Jing Yaping (2015) A formal language towards the unification of model checking and performance evaluation. PhD thesis, Iowa State University, Ames, IA |
| [29] |
Kwiatkowska, M; Norman, G; Parker, D, Prism: probabilistic model checking for performance and reliability analysis, SIGMETRICS Perform Eval Rev, 36, 40-45, (2009) · doi:10.1145/1530873.1530882 |
| [30] |
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of 23rd international conference on computer aided verification, volume 6806 of LNCS. Springer, pp 585-591 |
| [31] |
Kwiatkowska M, Norman G, Parker D, Sproston J (2003) Performance analysis of probabilistic timed automata using digital clocks. In: Proceedings of formal modeling and analysis of timed systems, volume 2791 of LNCS. Springer, pp 105-120 · Zbl 1099.68534 |
| [32] |
Kemeny, J.G., Snell, J.L.: Finite Markov Chains. D. Van Nostrand Company Inc, Princeton (1960) · Zbl 0089.13704 |
| [33] |
Kwiatkowska M (2007) Quantitative verification: models techniques and tools. In: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, New York, NY, USA, ACM, pp 449-458 |
| [34] |
Laroussinie, F; Sproston, J; Vladimiro, S (ed.), Model checking durational probabilistic systems, No. 3441, 140-154, (2005), Heidelberg · Zbl 1118.68548 |
| [35] |
Liu Y, Trivedi KS (2004) A general framework for network survivability quantification. In: Peter B, Ralf L, Michal P (eds) MMB. VDE Verlag, pp 369-378 |
| [36] |
Muppala JK, Ciardo G, Trivedi KS (1993) Modeling using stochastic reward nets. In: Proceedings of the international workshop on modeling, analysis, and simulation on computer and telecommunication systems. Society for Computer Simulation, pp 367-372 |
| [37] |
Meyer JF (1980) On evaluating the performability of degradable computing systems. IEEE Trans Comput C-29(8):720-731 · Zbl 0435.68007 |
| [38] |
Miner, AS, Implicit GSPN reachability set generation using decision diagrams, Perform Eval, 56, 145-165, (2004) · doi:10.1016/j.peva.2003.07.005 |
| [39] |
Miner AS, Jing Y (2010) A formal language toward the unification of model checking and performance evaluation. In: Analytical and stochastic modeling techniques and applications, pp 130-144 |
| [40] |
Obal, WD; Sanders, WH, State-space support for path-based reward variables, Perform Eval, 35, 233-251, (1999) · Zbl 1051.68527 · doi:10.1016/S0166-5316(99)00010-3 |
| [41] |
Pnueli, A, The temporal semantics of concurrent programs, Theoret Comput Sci, 13, 45-60, (1981) · Zbl 0441.68010 · doi:10.1016/0304-3975(81)90110-9 |
| [42] |
Ross, S.M.: Introduction to probability models, 9th edn. Academic, Orlando (2006) · Zbl 1118.60002 |
| [43] |
Suto T, Bradley JT, Knottenbelt WJ (2007) Performance trees: Expressiveness and quantitative semantics. In: Proceedings of the fourth international conference on quantitative evaluation of systems, Washington, DC, USA. IEEE Computer Society, pp 41-50 |
| [44] |
Schnoebelen P (2002) The complexity of temporal logic model checking. In: Advances in modal logic, pp 393-436 · Zbl 1084.03013 |
| [45] |
Stewart WJ (1994) Introduction to the numerical solution of Markov Chains. Princeton University Press · Zbl 0821.65099 |
| [46] |
Trivedi, KS; Ciardo, G; Malhotra, M; Sahner, RA, Dependability and performability analysis, 587-612, (1993), London · doi:10.1007/BFb0013869 |
