Parameter synthesis for Markov models: covering the parameter space. (English) Zbl 07873310
Summary: Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not – or only partially – known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov chain analysis relies on a single, fixed set of probabilities, analysing parametric Markov models focuses on synthesising parameter values that establish a given safety or performance specification \(\varphi\). Examples are: what component failure rates ensure the probability of a system breakdown to be below 0.00000001?, or which failure rates maximise the performance, for instance the throughput, of the system? This paper presents various analysis algorithms for parametric discrete-time Markov chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy \(\varphi\)?, (b) which regions satisfy \(\varphi\) and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values. We give a detailed account of the various algorithms, present a software tool realising these techniques, and report on an extensive experimental evaluation on benchmarks that span a wide range of applications.
MSC:
| 68-XX | Computer science |
Keywords:
formal methods; verification; model checking; probabilistic systems; parameter synthesis; Markov chainsSoftware:
PRISM-PSY; GiNaC; PARAM; PROPhESY; z3; PRISM; SMT-LIB; CoCoALib; FACT; Prophet; Storm; Eigen; SMT-RAT; SylvanReferences:
| [1] | (1999) IEEE wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) specification |
| [2] | Abbott J, Bigatti AM (2022) CoCoALib: a c++ library for doing computations in commutative algebra. http://cocoa.dima.unige.it/cocoalib |
| [3] | Aflaki S, Volk M, Bonakdarpour B, Katoen JP, Storjohann A (2017) Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS. IEEE Computer Society, pp 94-103 |
| [4] | Amparore EG, Beccuti M, Donatelli S (2014) (Stochastic) model checking in GreatSPN. In: Petri Nets, LNCS, vol 8489. Springer, Berlin, pp 354-363 |
| [5] | Andova S, Hermanns H, Katoen JP (2003) Discrete-time rewards model-checked. In: FORMATS, LNCS, vol 2791. Springer, Berlin, pp 88-104 · Zbl 1099.68652 |
| [6] | André É, Delahaye B (2016) Consistency in parametric interval probabilistic timed automata. In: TIME. IEEE Computer Society, pp 110-119 |
| [7] | Angluin D (1980) Local and global properties in networks of processors (extended abstract). In: STOC. ACM, pp 82-93 |
| [8] | Arming S, Bartocci E, Sokolova A (2017) SEA-PARAM: exploring schedulers in parametric MDPs. In: QAPL@ETAPS, EPTCS, vol 250, pp 25-38 |
| [9] | Arming S, Bartocci E, Chatterjee K, Katoen JP, Sokolova A (2018) Parameter-independent strategies for pMDPs via POMDPs. In: QEST, LNCS, vol 11024. Springer, Berlin, pp 53-70 · Zbl 1514.68190 |
| [10] | Bacci G, Delahaye B, Larsen KG, Mariegaard A (2021) Quantitative analysis of interval Markov chains. In: Model checking, synthesis, and learning, LNCS, vol 13030. Springer, Berlin, pp 57-77 · Zbl 1522.68296 |
| [11] | Badings, TS; Cubuktepe, M.; Jansen, N.; Junges, S.; Katoen, J.; Topcu, U., Scenario-based verification of uncertain parametric MDPs, Int J Softw Tools Technol Transf, 24, 5, 803-819, 2022 |
| [12] | Badings TS, Jansen N, Junges S, Stoelinga M, Volk M (2022) Sampling-based verification of CTMCs with uncertain rates. In: CAV (2), LNCS, vol 13372. Springer, Berlin, pp 26-47 · Zbl 1514.68117 |
| [13] | Baier, C.; Katoen, JP, Principles of model checking, 2008, Cambridge: MIT Press, Cambridge · Zbl 1179.68076 |
| [14] | Baier C, Clarke EM, Hartonas-Garmhausen V, Kwiatkowska MZ, Ryan M (1997) Symbolic model checking for probabilistic processes. In: ICALP, LNCS, vol 1256. Springer, Berlin, pp 430-440 · Zbl 1401.68180 |
| [15] | Baier C, Klein J, Klüppelholz S, Märcker S (2014) Computing conditional probabilities in Markovian models efficiently. In: TACAS, LNCS, vol 8413. Springer, Berlin, pp 515-530 |
| [16] | Baier C, de Alfaro L, Forejt V, Kwiatkowska M (2018) Model checking probabilistic systems. In: Handbook of model checking. Springer, Berlin, pp 963-999 · Zbl 1392.68227 |
| [17] | Baier, C.; Hensel, C.; Hutschenreiter, L.; Junges, S.; Katoen, J.; Klein, J., Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Inf Comput, 272, 104, 504, 2020 · Zbl 1443.68101 |
| [18] | Barrett C, Fontaine P, Tinelli C (2016) The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org |
| [19] | Bart, A.; Delahaye, B.; Fournier, P.; Lime, D.; Monfroy, E.; Truchet, C., Reachability in parametric interval Markov chains using constraints, Theor Comput Sci, 747, 48-74, 2018 · Zbl 1400.68118 |
| [20] | Bartocci E, Grosu R, Katsaros P, Ramakrishnan C, Smolka SA (2011) Model repair for probabilistic systems. In: TACAS, LNCS, vol 6605. Springer, Berlin, pp 326-340 · Zbl 1316.68070 |
| [21] | Basu, S.; Pollack, R.; Roy, MF, Algorithms in real algebraic geometry (algorithms and computation in mathematics), 2006, New York: Springer, New York · Zbl 1102.14041 |
| [22] | Bauer, C.; Frink, A.; Kreckel, R., Introduction to the Ginac framework for symbolic computation within the C++ programming language, J Symb Comput, 33, 1, 1-12, 2002 · Zbl 1017.68163 |
| [23] | Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of satisfiability, frontiers in artificial intelligence and applications, 2009, Amsterdam: IOS Press, Amsterdam · Zbl 1183.68568 |
| [24] | Bobbio, A.; Trivedi, KS, Reliability and availability engineering: modeling, analysis, and applications, 2017, Cambridge: Cambridge University Press, Cambridge |
| [25] | Bortolussi L, Silvetti S (2018) Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: TACAS (2), LNCS, vol 10806. Springer, Berlin, pp 396-413 · Zbl 1423.68322 |
| [26] | Bortolussi, L.; Milios, D.; Sanguinetti, G., Smoothed model checking for uncertain continuous-time Markov chains, Inf Comput, 247, 235-253, 2016 · Zbl 1336.68162 |
| [27] | Boudali, H.; Crouzen, P.; Stoelinga, M., A rigorous, compositional, and extensible framework for dynamic fault tree analysis, IEEE Trans Depend Secure Comput, 7, 2, 128-143, 2010 |
| [28] | Bozzano, M.; Villafiorita, A., Design and safety assessment of critical systems, 2010, Cambridge: CRC Press, Cambridge |
| [29] | Bozzano, M.; Cimatti, A.; Katoen, JP; Katsaros, P.; Mokos, K.; Nguyen, VY; Noll, T.; Postma, B.; Roveri, M., Spacecraft early design validation using formal methods, Reliab Eng Syst Saf, 132, 20-35, 2014 |
| [30] | Brim L, Ceska M, Drazan S, Safránek D (2013) Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: CAV, LNCS, vol 8044. Springer, Berlin, pp 107-123 |
| [31] | Bruttomesso R, Cimatti A, Franzén A, Griggio A, Sebastiani R (2008) The MathSAT 4 SMT solver. In: CAV, LNCS, vol 5123. Springer, Berlin, pp 299-303 |
| [32] | Budde CE, Dehnert C, Hahn EM, Hartmanns A, Junges S, Turrini A (2017) JANI: quantitative model and tool interaction. In: TACAS (2), LNCS, vol 10206, pp 151-168 |
| [33] | Calinescu, R.; Ghezzi, C.; Johnson, K.; Pezzè, M.; Rafiq, Y.; Tamburrelli, G., Formal verification with confidence intervals to establish quality of service properties of software systems, IEEE Trans Reliab, 65, 1, 107-125, 2016 |
| [34] | Calinescu R, Johnson K, Paterson C (2016) FACT: a probabilistic model checker for formal verification with confidence intervals. In: TACAS, LNCS, vol 9636. Springer, Berlin, pp 540-546 |
| [35] | Calinescu, R.; Ceska, M.; Gerasimou, S.; Kwiatkowska, M.; Paoletti, N., Efficient synthesis of robust models for stochastic systems, J Syst Softw, 143, 140-158, 2018 |
| [36] | Campi, MC; Garatti, S., The exact feasibility of randomized solutions of uncertain convex programs, SIAM J Optim, 19, 3, 1211-1230, 2008 · Zbl 1180.90235 |
| [37] | Campi, MC; Garatti, S., A sampling-and-discarding approach to chance-constrained optimization: feasibility and optimality, J Optim Theory Appl, 148, 2, 257-280, 2011 · Zbl 1211.90146 |
| [38] | Cerotti D, Donatelli S, Horváth A, Sproston J (2006) CSL model checking for generalized stochastic Petri nets. In: QEST. IEEE Computer Society, pp 199-210 |
| [39] | Ceska M, Dannenberg F, Kwiatkowska MZ, Paoletti N (2014) Precise parameter synthesis for stochastic biochemical systems. In: CMSB, LNCS, vol 8859. Springer, Berlin, pp 86-98 |
| [40] | Ceska M, Pilar P, Paoletti N, Brim L, Kwiatkowska MZ (2016) PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: TACAS, LNCS, vol 9636. Springer, Berlin, pp 367-384 |
| [41] | Ceska M, Jansen N, Junges S, Katoen J (2019) Shepherding hordes of Markov chains. In: TACAS (2), Lecture Notes in Computer Science, vol 11428. Springer, Berlin, pp 172-190 · Zbl 1527.68144 |
| [42] | Chatzieleftheriou, G.; Katsaros, P., Abstract model repair for probabilistic systems, Inf Comput, 259, 1, 142-160, 2018 · Zbl 1388.68185 |
| [43] | Chen T, Hahn EM, Han T, Kwiatkowska M, Qu H, Zhang L (2013) Model repair for Markov decision processes. In: TASE. IEEE Computer Society, pp 85-92 |
| [44] | Chen T, Feng Y, Rosenblum DS, Su G (2014) Perturbation analysis in verification of discrete-time Markov chains. In: CONCUR, LNCS, vol 8704. Springer, Berlin, pp 218-233 · Zbl 1417.68100 |
| [45] | Chonev V (2017) Reachability in augmented interval Markov chains. CoRR arXiv:1701.02996 |
| [46] | Clarke, EM; Grumberg, O.; Peled, D., Model checking, 1999, Cambridge: MIT Press, Cambridge |
| [47] | Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: CAV, LNCS, vol 1855. Springer, Berlin, pp 154-169 · Zbl 0974.68517 |
| [48] | Condon A (1990) On algorithms for simple stochastic games. In: Advances in computational complexity theory, DIMACS/AMS, DIMACS series in discrete mathematics and theoretical computer science, vol 13, pp 51-72 · Zbl 0808.90141 |
| [49] | Cook B (2018) Formal reasoning about the security of Amazon web services. In: CAV, LNCS, vol 10981. Springer, Berlin, pp 38-47 |
| [50] | Coppit D, Sullivan KJ, Dugan JB (2000) Formal semantics of models for computational engineering: a case study on Dynamic Fault Trees. In: ISSRE. IEEE Computer Society, pp 270-282. doi:10.1109/ISSRE.2000.885878 |
| [51] | Cormen, TH; Leiserson, CE; Rivest, RL; Stein, C., Introduction to algorithms, 2009, Cambridge: MIT Press, Cambridge · Zbl 1187.68679 |
| [52] | Corzilius F, Kremer G, Junges S, Schupp S, Ábrahám E (2015) SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: SAT, LNCS, vol 9340. Springer, Berlin, pp 360-368 · Zbl 1471.68241 |
| [53] | Costen C, Rigter M, Lacerda B, Hawes N (2023) Planning with hidden parameter polynomial MDPs. In: AAAI. AAAI Press, Pomona, pp 11,963-11,971 |
| [54] | Courcoubetis C, Yannakakis M (1988) Verifying temporal properties of finite-state probabilistic programs. In: FOCS. IEEE Computer Society, pp 338-345 |
| [55] | Cousineau, D., Fitting the three-parameter Weibull distribution: review and evaluation of existing and new methods, IEEE Trans Dielectr Electr Insul, 16, 1, 281-288, 2009 |
| [56] | Cubuktepe M, Jansen N, Junges S, Katoen JP, Papusha I, Poonawala HA, Topcu U (2017) Sequential convex programming for the efficient verification of parametric MDPs. In: TACAS (2), LNCS, vol 10206, pp 133-150 · Zbl 1452.68117 |
| [57] | Cubuktepe M, Jansen N, Junges S, Katoen JP, Topcu U (2018) Synthesis in pMDPs: a tale of 1001 parameters. In: ATVA, LNCS, vol 11138. Springer, Berlin, pp 160-176 · Zbl 1517.68227 |
| [58] | Cubuktepe M, Jansen N, Junges S, Katoen J, Topcu U (2020) Scenario-based verification of uncertain MDPs. In: TACAS (1), LNCS, vol 12078. Springer, Berlin, pp 287-305 · Zbl 1507.68182 |
| [59] | Cubuktepe M, Jansen N, Junges S, Marandi A, Suilen M, Topcu U (2021) Robust finite-state controllers for uncertain POMDPs. In: AAAI. AAAI Press, Pomona, pp 11,792-11,800 |
| [60] | Cubuktepe, M.; Jansen, N.; Junges, S.; Katoen, J.; Topcu, U., Convex optimization for parameter synthesis in MDPs, IEEE Trans Autom Control, 67, 12, 6333-6348, 2022 · Zbl 07742136 |
| [61] | D’Argenio PR, Katoen JP, Ruys TC, Tretmans J (1997) The bounded retransmission protocol must be on time! In: TACAS, LNCS, vol 1217. Springer, Berlin, pp 416-431 |
| [62] | D’Argenio PR, Jeannet B, Jensen HE, Larsen KG (2001) Reachability analysis of probabilistic systems by successive refinements. In: PAPM-PROBMIV, LNCS, vol 2165. Springer, Berlin, pp 39-56 · Zbl 1007.68131 |
| [63] | de Moura LM, Bjørner N (2008) Z3: An efficient SMT solver. In: TACAS, LNCS, vol 4963. Springer, Berlin, pp 337-340 |
| [64] | Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC, LNCS, vol 3407. Springer, Berlin, pp 280-294 · Zbl 1108.68497 |
| [65] | Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, Katoen JP, Ábrahám E (2015) Prophesy: a probabilistic parameter synthesis tool. In: CAV, LNCS, vol 9206. Springer, Berlin, pp 214-231 |
| [66] | Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: a modern probabilistic model checker. In: CAV, LNCS, vol 10427. Springer, Berlin, pp 592-600 |
| [67] | Delgado, KV; Sanner, S.; de Barros, LN, Efficient solutions to factored MDPs with imprecise transition probabilities, Artif Intell, 175, 9-10, 1498-1527, 2011 · Zbl 1230.90115 |
| [68] | Delgado, KV; de Barros, LN; Dias, DB; Sanner, S., Real-time dynamic programming for Markov decision processes with imprecise probabilities, Artif Intell, 230, 192-223, 2016 · Zbl 1344.68246 |
| [69] | Droste, M.; Kuich, W.; Vogler, H., Handbook of weighted automata, 2009, Berlin: Springer, Berlin · Zbl 1200.68001 |
| [70] | Duflot, M.; Kwiatkowska, MZ; Norman, G.; Parker, D., A formal analysis of bluetooth device discovery, STTT, 8, 6, 621-632, 2006 |
| [71] | Dugan, JB; Bavuso, SJ; Boyd, MA, Dynamic fault-tree models for fault-tolerant computer systems, Trans Reliab, 41, 3, 363-377, 1992 · Zbl 0825.68162 · doi:10.1109/24.159800 |
| [72] | Filieri, A.; Tamburrelli, G.; Ghezzi, C., Supporting self-adaptation via quantitative verification and sensitivity analysis at run time, IEEE Trans Software Eng, 42, 1, 75-99, 2016 |
| [73] | Gainer P, Hahn EM, Schewe S (2018) Accelerated model checking of parametric Markov chains. In: ATVA, LNCS, vol 11138. Springer, Berlin, pp 300-316 · Zbl 1517.68235 |
| [74] | Givan, R.; Leach, SM; Dean, TL, Bounded-parameter Markov decision processes, Artif Intell, 122, 1-2, 71-109, 2000 · Zbl 0948.68171 |
| [75] | Gouberman, A.; Siegle, M.; Tati, B., Markov chains with perturbed rates to absorption: theory and application to model repair, Perform Evaluat, 130, 32-50, 2019 |
| [76] | Guennebaud G, Jacob B et al (2010) Eigen v3. http://eigen.tuxfamily.org |
| [77] | Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PARAM: a model checker for parametric Markov models. In: CAV, LNCS, vol 6174. Springer, Berlin, pp 660-664 |
| [78] | Hahn, EM; Hermanns, H.; Zhang, L., Probabilistic reachability for parametric Markov models, STTT, 13, 1, 3-19, 2010 |
| [79] | Hahn EM, Han T, Zhang L (2011) Synthesis for PCTL in parametric Markov decision processes. In: NASA formal methods, LNCS, vol 6617. Springer, Berlin, pp 146-161 |
| [80] | Hahn, EM; Hartmanns, A.; Hermanns, H.; Katoen, JP, A compositional modelling and analysis framework for stochastic hybrid systems, Formal Methods Syst Des, 43, 2, 191-232, 2013 · Zbl 1291.68293 |
| [81] | Hahn EM, Hashemi V, Hermanns H, Lahijanian M, Turrini A (2017) Multi-objective robust strategy synthesis for interval Markov decision processes. In: QEST, LNCS, vol 10503. Springer, Berlin, pp 207-223 · Zbl 1421.90160 |
| [82] | Hahn EM, Hashemi V, Hermanns H, Lahijanian M, Turrini A (2019) Interval Markov decision processes with multiple objectives: From robust strategies to pareto curves. ACM Trans Model Comput Simul 29(4):27:1-27:31 · Zbl 07908621 |
| [83] | Han T, Katoen JP, Mereacre A (2008) Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS. IEEE Computer Society, pp 173-182 |
| [84] | Han, Y., State elimination heuristics for short regular expressions, Fundam Inform, 128, 4, 445-462, 2013 · Zbl 1285.68086 |
| [85] | Haselman, M.; Hauck, S., The future of integrated circuits: a survey of nanoelectronics, Proc IEEE, 98, 1, 11-38, 2010 |
| [86] | Heck L, Spel J, Junges S, Moerman J, Katoen J (2022) Gradient-descent for randomized controllers under partial observability. In: VMCAI, LNCS, vol. 13182. Springer, Berlin, pp 127-150 · Zbl 1498.68159 |
| [87] | Helmink L, Sellink MPA, Vaandrager FW (1993) Proof-checking a data link protocol. In: TYPES, LNCS, vol 806. Springer, Berlin, pp 127-165 |
| [88] | Herman, T., Probabilistic self-stabilization, Inf Process Lett, 35, 2, 63-67, 1990 · Zbl 0697.68027 |
| [89] | Holtzen S, Junges S, Vazquez-Chanlatte M, Millstein TD, Seshia SA, den Broeck GV (2021) Model checking finite-horizon Markov chains with probabilistic inference. In: CAV (2), LNCS, vol 12760. Springer, Berlin, pp 577-601 · Zbl 1493.68210 |
| [90] | Hopcroft, JE; Motwani, R.; Ullman, JD, Introduction to automata theory, languages, and computation, 2003, Boston: Addison-Wesley, Boston |
| [91] | Jansen N, Corzilius F, Volk M, Wimmer R, Ábrahám E, Katoen JP, Becker B (2014) Accelerating parametric probabilistic verification. In: QEST, LNCS, vol 8657. Springer, Berlin, 404-420 |
| [92] | Jonsson B, Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS. IEEE Computer Society, pp 266-277 |
| [93] | Jovanovic, D.; de Moura, LM, Cutting to the chase—solving linear integer arithmetic, J Autom Reason, 51, 1, 79-108, 2013 · Zbl 1314.90053 |
| [94] | Junges S (2020) Parameter synthesis in Markov models. Ph.D. thesis, RWTH Aachen University, Germany |
| [95] | Junges S, Spaan MTJ (2022) Abstraction-refinement for hierarchical probabilistic models. In: CAV (1), LNCS, vol 13371. Springer, Berlin, pp 102-123 · Zbl 1514.68029 |
| [96] | Junges S, Jansen N, Wimmer R, Quatmann T, Winterer L, Katoen JP, Becker B (2018) Finite-state controllers of POMDPs using parameter synthesis. In: UAI. AUAI Press, pp 519-529 |
| [97] | Junges, S.; Katoen, J.; Pérez, GA; Winkler, T., The complexity of reachability in parametric Markov decision processes, J Comput Syst Sci, 119, 183-210, 2021 · Zbl 1477.68124 |
| [98] | Katoen JP (2016) The probabilistic model checking landscape. In: LICS. ACM · Zbl 1401.68201 |
| [99] | Knuth D, Yao A (1976) Algorithms and complexity: new directions and recent results. Academic Press, chap The complexity of nonuniform random number generation · Zbl 0363.00013 |
| [100] | Kozine, I.; Utkin, LV, Interval-valued finite Markov chains, Reliable Comput, 8, 2, 97-113, 2002 · Zbl 1001.65007 |
| [101] | Kurshan RP (2018) Transfer of model checking to industrial practice. In: Handbook of model checking. Springer, Berlin, pp 763-793 · Zbl 1392.68256 |
| [102] | Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: CAV, LNCS, vol 6806. Springer, Berlin, pp 585-591 |
| [103] | Kwiatkowska M, Norman G, Parker D (2012a) The PRISM benchmark suite. In: QEST. IEEE Computer Society, pp 203-204 |
| [104] | Kwiatkowska, MZ; Norman, G.; Parker, D., Using probabilistic model checking in systems biology, SIGMETRICS Perform Eval Rev, 35, 4, 14-21, 2008 |
| [105] | Kwiatkowska, MZ; Norman, G.; Parker, D., Probabilistic verification of Herman’s self-stabilisation algorithm, Formal Asp Comput, 24, 4-6, 661-670, 2012 · Zbl 1259.68130 |
| [106] | Lanotte, R.; Maggiolo-Schettini, A.; Troina, A., Parametric probabilistic transition systems for system design and analysis, Formal Asp Comput, 19, 1, 93-109, 2007 · Zbl 1111.68084 |
| [107] | Long F, Rinard M (2016) Automatic patch generation by learning correct code. In: POPL. ACM, pp 298-312 |
| [108] | Mannor S, Mebel O, Xu H (2012) Lightning does not strike twice: robust MDPs with coupled uncertainty. In: ICML. icml.cc/Omnipress |
| [109] | Marsan, MA; Balbo, G.; Conte, G.; Donatelli, S.; Franceschinis, G., Modelling with generalized stochastic petri nets, SIGMETRICS Perform Evaluat Rev, 26, 2, 2, 1998 |
| [110] | McGlynn MJ, Borbash SA (2001) Birthday protocols for low energy deployment and flexible neighbor discovery in ad hoc wireless networks. In: MobiHoc. ACM, pp 137-145 |
| [111] | Meedeniya, I.; Moser, I.; Aleti, A.; Grunske, L., Evaluating probabilistic models with uncertain model parameters, Softw Syst Model, 13, 4, 1395-1415, 2014 |
| [112] | Mushkin, M.; Bar-David, I., Capacity and coding for the Gilbert-Elliot channels, IEEE Trans Inf Theory, 35, 6, 1277-1290, 1989 · Zbl 0695.94006 |
| [113] | Neary C, Verginis CK, Cubuktepe M, Topcu U (2022) Verifiable and compositional reinforcement learning systems. In: ICAPS. AAAI Press, Pomona, pp 615-623 |
| [114] | Norman, G.; Shmatikov, V., Analysis of probabilistic contract signing, J Comput Secur, 14, 6, 561-589, 2006 |
| [115] | Norman, G.; Parker, D.; Kwiatkowska, M.; Shukla, S., Evaluating the reliability of NAND multiplexing with PRISM, IEEE Trans Comput Aided Des Integr Circuits Syst, 24, 10, 1629-1637, 2005 |
| [116] | Norman, G.; Parker, D.; Zou, X., Verification and control of partially observable probabilistic systems, Real-Time Syst, 53, 3, 354-402, 2017 · Zbl 1425.68266 |
| [117] | Pathak S, Ábrahám E, Jansen N, Tacchella A, Katoen J (2015) A greedy approach for the efficient repair of stochastic models. In: NFM, LNCS, vol. 9058. Springer, Berlin, pp 295-309 |
| [118] | Petrucci L, van de Pol J (2018) Parameter synthesis algorithms for parametric interval Markov chains. In: FORTE, LNCS, vol. 10854. Springer, Berlin, pp 121-140 · Zbl 1508.68256 |
| [119] | Polgreen E, Wijesuriya VB, Haesaert S, Abate A (2016) Data-efficient bayesian verification of parametric Markov chains. In: QEST, LNCS, vol. 9826. Springer, Berlin, pp 35-51 · Zbl 1377.68136 |
| [120] | Puggelli A, Li W, Sangiovanni-Vincentelli AL, Seshia SA (2013) Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: CAV, LNCS, vol 8044. Springer, Berlin, pp 527-542 · Zbl 1435.68202 |
| [121] | Puterman, ML, Markov decision processes: discrete stochastic dynamic programming, 1994, New York: Wiley, New York · Zbl 0829.90134 |
| [122] | Quatmann T, Dehnert C, Jansen N, Junges S, Katoen JP (2016) Parameter synthesis for Markov models: Faster than ever. In: ATVA, LNCS, vol 9938, pp 50-67 · Zbl 1398.68346 |
| [123] | Ruijters, E.; Stoelinga, M., Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools, Comput Sci Rev, 15-16, 29-62, 2015 · Zbl 1315.90013 |
| [124] | Russell SJ, Norvig P (2010) Artificial intelligence—a modern approach (3. internat. ed.). Pearson Education, London |
| [125] | Sakarovitch J (2005) The language, the expression, and the (small) automaton. In: CIAA, LNCS, vol 3845. Springer, Berlin, pp 15-30 · Zbl 1172.68526 |
| [126] | Salmani B, Katoen J (2021) Fine-tuning the odds in bayesian networks. In: ECSQARU, LNCS, vol 12897. Springer, Berlin, pp 268-283 · Zbl 07542348 |
| [127] | Segala R, Turrini A (2005) Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: QEST. IEEE Computer Society, pp 44-53 |
| [128] | Shapley, LS, Stochastic games, Proc Natl Acad Sci, 39, 10, 1095-1100, 1953 · Zbl 0051.35805 |
| [129] | Spel J, Junges S, Katoen J (2019) Are parametric Markov chains monotonic? In: ATVA, LNCS, vol 11781. Springer, Berlin, pp 479-496 · Zbl 1437.68121 |
| [130] | Spel J, Junges S, Katoen J (2021) Finding provably optimal Markov chains. In: TACAS (1), LNCS, vol 12651. Springer, Berlin, pp 173-190 · Zbl 1467.68095 |
| [131] | Su, G.; Feng, Y.; Chen, T.; Rosenblum, DS, Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters, IEEE Trans Software Eng, 42, 7, 623-639, 2016 |
| [132] | Suilen M, Jansen N, Cubuktepe M, Topcu U (2020) Robust policy synthesis for uncertain POMDPs via convex optimization. In: IJCAI, ijcai.org, pp 4113-4120 |
| [133] | Suilen M, Simão TD, Parker D, Jansen N (2022) Robust anytime learning of Markov decision processes. In: NeurIPS |
| [134] | Tappler M, Aichernig BK, Bacci G, Eichlseder M, Larsen KG (2019) L \({}^{\text{*}} \)-based learning of markov decision processes. In: FM, Lecture Notes in Computer Science, vol 11800. Springer, Berlin, pp 651-669 · Zbl 1539.68123 |
| [135] | van Dijk, T.; van de Pol, J., Sylvan: multi-core framework for decision diagrams, STTT, 19, 6, 675-696, 2017 |
| [136] | Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: FOCS. IEEE Computer Society, pp 327-338 |
| [137] | Vesely W, Stamatelatos M (2002) Fault tree handbook with aerospace applications. Tech. rep, NASA Headquarters, USA |
| [138] | Volk M, Junges S, Katoen JP (2016) Advancing dynamic fault tree analysis—get succinct state spaces fast and synthesise failure rates. In: SAFECOMP, LNCS, vol 9922. Springer, Berlin, pp 253-265 |
| [139] | Volk, M.; Junges, S.; Katoen, JP, Fast dynamic fault tree analysis by model checking techniques, IEEE Trans Ind Inform, 14, 1, 370-379, 2018 |
| [140] | von Neumann, J.; Shannon, C.; McCarthy, J., Probabilistic logics and synthesis of reliable organisms from unreliable components, Automata studies, 43-98, 1956, Princeton: Princeton University Press, Princeton |
| [141] | Wiesemann, W.; Kuhn, D.; Rustem, B., Robust Markov decision processes, Math Oper Res, 38, 1, 153-183, 2013 · Zbl 1291.90295 |
| [142] | Winkler T, Junges S, Pérez GA, Katoen J (2019) On the complexity of reachability in parametric Markov decision processes. In: CONCUR, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol 140, pp 14:1-14:17 · Zbl 07649922 |
| [143] | Yang L, Murugesan S, Zhang J (2011) Real-time scheduling over Markovian channels: when partial observability meets hard deadlines. In: GLOBECOM. IEEE, pp 1-5 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
