×

zbMATH — the first resource for mathematics

Three-valued abstraction for probabilistic systems. (English) Zbl 1277.68219
Summary: This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (probabilistic computation tree logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (continuous stochastic logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs.

MSC:
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
Software:
MRMC; PEPA; PRISM; SMART_; Ymer
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ash, R.B.; Doléans-Dade, C.A., Probability & measure theory, (2000), Academic Press · Zbl 0944.60004
[2] Aziz, A.; Sanwal, K.; Singhal, V.; Brayton, R., Model-checking continuous time Markov chains, ACM tocl, 1, 1, 162-170, (2000) · Zbl 1365.68313
[3] Baier, C.; Katoen, J.-P., Principles of model checking, (2008), The MIT Press
[4] Baier, C.; Clarke, E.; Hartonas-Garmhausen, V.; Kwiatkowska, M.; Ryan, M., Symbolic model checking for probabilistic processes, (), 430-440 · Zbl 1401.68180
[5] Baier, C.; Engelen, B.; Majster-Cederbaum, M.E., Deciding bisimilarity and similarity for probabilistic processes, J. comput. system sci., 60, 1, 187-231, (2000) · Zbl 1073.68690
[6] Baier, C.; Haverkort, B.; Hermanns, H.; Katoen, J.-P., Model-checking algorithms for continuous-time Markov chains, Ieee tse, 29, 6, 524-541, (2003)
[7] Baier, C.; Ciesinski, F.; Größer, M., Probmela and verification of Markov decision processes, Perform. eval. rev., 32, 4, 22-27, (2005)
[8] Baier, C.; Katoen, J.-P.; Hermanns, H.; Wolf, V., Comparative branching-time semantics for Markov chains, Inform. and comput., 200, 2, 149-214, (2005) · Zbl 1101.68053
[9] Baier, C.; Hermanns, H.; Katoen, J.P.; Haverkort, B.R., Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes, Tcs, 345, 1, 2-26, (2005) · Zbl 1081.90066
[10] Barbuti, R.; Levi, F.; Milazzo, P.; Scatena, G., Probabilistic model checking of biological systems with uncertain kinetic rates, (), 78 · Zbl 1260.68226
[11] F. Bause, P.S. Kritzinger, Stochastic Petri nets: an introduction to the theory, SIGMETRICS Performance Eval. Rev. 26 (2), http://dx.doi.org/http://doi.acm.org/10.1145/288197.581194. · Zbl 1013.60065
[12] Bellman, R.E., Dynamic programming, (1957), Princeton University Press
[13] BenMamoun, M.; Pekergin, N.; Younès, S., Model checking of continuous-time Markov chains by closed-form bounding distributions, (), 189-198
[14] Böde, E.; Herbstritt, M.; Hermanns, H.; Johr, S.; Peikenkamp, T.; Pulungan, R.; Rakow, J.; Wimmer, R.; Becker, B., Compositional dependability evaluation for \scstatemate, Ieee tse, 35, 2, 274-292, (2009)
[15] Bremaud, P., Markov chains, (2001), Springer
[16] Chatterjee, K.; Sen, K.; Henzinger, T.A., Model-checking omega-regular properties of interval Markov chains, (), 302-317 · Zbl 1138.68441
[17] Ciardo, G.; Jones, R.L.; Miner, A.; Siminiceanu, R., Logic and stochastic modeling with SMART, (), 78-97
[18] Clarke, E.M.; Emerson, E.A.; Sistla, A.P., Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach, (), 117-126 · Zbl 0591.68027
[19] D’Aprile, D.; Donatelli, S.; Sproston, J., CSL model checking for the great SPN tool, (), 543-553
[20] D’Argenio, P.R.; Jeannet, B.; Jensen, H.E.; Larsen, K.G., Reachability analysis of probabilistic systems by successive refinements, (), 39-56 · Zbl 1007.68131
[21] L. deAlfaro, Formal verification of probabilistic systems, Ph.D. Thesis, Stanford University, 1998.
[22] deAlfaro, L.; Pritam, R., Magnifying-Lens abstraction for Markov decision processes, (), 325-338 · Zbl 1135.68486
[23] Fecher, H.; Leucker, M.; Wolf, V., Don’t know in probabilistic systems, (), 71-88 · Zbl 1178.68341
[24] Feller, W., An introduction to probability theory and its applications, vol. I, (1968), John Wiley & Sons Inc. · Zbl 0155.23101
[25] Gilmore, S.; Hillston, J., The PEPA workbench: a tool to support a process algebra-based approach to performance modelling, (), 353-368
[26] Groesser, M.; Baier, C., Partial order reduction for Markov decision processes: a survey, (), 408-427 · Zbl 1196.68137
[27] Gross, D.; Miller, D., The randomization technique as a modeling tool and solution procedure for transient Markov chains, Oper. res., 32, 2, 343-361, (1984) · Zbl 0536.60078
[28] Grumberg, O.; Lange, M.; Leucker, M.; Shoham, S., Don’t know in the μ-calculus, (), 233 · Zbl 1112.68090
[29] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal aspects comput., 6, 5, 512-535, (1994) · Zbl 0820.68113
[30] Haverkort, B.R., Performance of computer communication systems: A model-based approach, (1998), John Wiley & Sons, Inc. New York
[31] Henzinger, T.; Mateescu, M.; Wolf, V., Sliding window abstraction for infinite Markov chains, (), 337-352 · Zbl 1242.60079
[32] Huth, M., An abstraction framework for mixed non-deterministic and probabilistic systems, (), 419-444 · Zbl 1203.68099
[33] Huth, M., On finite-state approximants for probabilistic computation tree logic, Tcs, 346, 1, 113-134, (2005) · Zbl 1080.68064
[34] Huth, M.; Jagadeesan, R.; Schmidt, D., Modal transition systems: a foundation for three-valued program analysis, Lecture notes in comput. sci., 2028, 155-169, (2001) · Zbl 0987.68849
[35] Huth, M.; Piterman, N.; Wagner, D., Three-valued abstractions of Markov chains: completeness for a sizeable fragment of PCTL, (), 205-216 · Zbl 1252.03037
[36] Jansen, D.N.; Katoen, J.-P.; Oldenkamp, M.; Stoelinga, M.; Zapreev, I.S., How fast and fat is your probabilistic model checker? an experimental comparison, (), 69-85
[37] Jonsson, B.; Larsen, K., Specification and refinement of probabilistic processes, (), 266-277
[38] Katoen, J.-P.; Kemna, T.; Zapreev, I.; Jansen, D.N., Bisimulation minimisation mostly speeds up probabilistic model checking, (), 87-102 · Zbl 1186.68296
[39] Katoen, J.-P.; Klink, D.; Leucker, M.; Wolf, V., Three-valued abstraction for continuous-time Markov chains, (), 316-329
[40] Katoen, J.-P.; Klink, D.; Leucker, M.; Wolf, V., Abstraction for stochastic systems by erlang’s method of stages, (), 279-294 · Zbl 1160.68469
[41] Katoen, J.P.; Hahn, E.M.; Hermanns, H.; Jansen, D.N.; Zapreev, I.S., The ins and outs of the probabilistic model checker MRMC, (), 167-176
[42] Klink, D.; Remke, A.; Haverkort, B.R.; Katoen, J.-P., Probabilistic model checking of biological systems with uncertain kinetic rates, (), 133-142
[43] Kozine, I.O.; Utkin, L.V., Interval-valued finite Markov chains, Reliab. comput., 8, 2, 97-113, (2002) · Zbl 1001.65007
[44] Kwiatkowska, M.; Norman, G.; Parker, D., Probabilistic symbolic model checking with PRISM: a hybrid approach, Int. J. STTT, 6, 2, 128-142, (2004)
[45] Kwiatkowska, M.; Norman, G.; Parker, D., Symmetry reduction for probabilistic model checking, (), 234-248 · Zbl 1188.68194
[46] Kwiatkowska, M.; Norman, G.; Parker, D., Game-based abstraction for Markov decision processes, (), 157-166
[47] Larsen, K.; Thomsen, B., A modal process logic, (), 203-210
[48] F. Moller, The Edinburgh Concurrency Workbench (Version 6.1), Department of Computer Science, University of Edinburgh, October 1992.
[49] Neuhäußer, M.; Stoelinga, M.; Katoen, J.-P., Delayed nondeterminism in continuous-time Markov decision processes, (), 364-379 · Zbl 1234.68320
[50] Penna, G.D.; Intrigila, B.; Melatti, I.; Tronci, E.; Zilli, M.V., Finite horizon analysis of Markov chains with the murφ verifier, Int. J. STTT, 8, 4, 397-409, (2006)
[51] Puterman, M.L., Markov decision processes: discrete stochastic dynamic programming, (1994), John Wiley & Sons, Inc. New York · Zbl 0829.90134
[52] Ross, S., Stochastic processes, (1996), John Wiley & Sons
[53] Sen, K.; Viswanathan, M.; Agha, G., Model-checking Markov chains in the presence of uncertainties, (), 394-410 · Zbl 1180.68179
[54] Skulj, D., Finite DTMCs with interval probabilities, (), 299-306 · Zbl 1106.60066
[55] Wolovick, N.; Johr, S., A characterization of meaningful schedulers for continuous-time Markov decision processes, (), 352-367 · Zbl 1141.68517
[56] Yi, W., Algebraic reasoning for real-time probabilistic processes with uncertain information, (), 680-693
[57] Younes, H., Ymer: a statistical model checker, (), 429-433 · Zbl 1081.68642
[58] Zhang, L.; Hermanns, H.; Eisenbrand, F.; Jansen, D.N., Flow faster: efficient decision algorithms for probabilistic simulations, Logical methods comput. sci., 4, 4, (2008) · Zbl 1161.68473
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.