×

zbMATH — the first resource for mathematics

Local abstraction refinement for probabilistic timed programs. (English) Zbl 1359.68187
Summary: We consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstractions generated and the complexity of operations needed, in comparison to previous approaches of this kind. We implement the techniques and evaluate them on a selection of large case studies, including some infinite-state probabilistic real-time models, demonstrating improvements over existing tools in several cases.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
CEGAR; MathSAT; PASS; PRISM
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Lamport, L., The existence of refinement mappings, Theor. Comput. Sci., 82, 2, 253-284, (1991) · Zbl 0728.68083
[2] Bengtsson, J.; Yi, W., Timed automata: semantics, algorithms and tools, (Lectures on Concurrency and Petri Nets, (2003)), 87-124 · Zbl 1088.68119
[3] Berendsen, J.; Jansen, D.; Vaandrager, F., Fortuna: model checking priced probabilistic timed automata, (Proc. QEST’10, (2010)), 273-281
[4] Bruttomesso, R.; Cimatti, A.; Franzén, A.; Griggio, A.; Sebastiani, R., The mathsat 4 SMT solver, (Proc. CAV’08, (2008), Springer), 299-303
[5] Cimatti, A.; Griggio, A.; Sebastiani, R., Efficient generation of Craig interpolants in satisfiability modulo theories, ACM Trans. Comput. Log., 12, 1, (2010) · Zbl 1351.68247
[6] D’Argenio, P.; Jeannet, B.; Jensen, H.; Larsen, K., Reachability analysis of probabilistic systems by successive refinements, (Proc. PAPM/PROBMIV’01, (2001), Springer), 39-56 · Zbl 1007.68131
[7] Esparza, J.; Gaiser, A., Probabilistic abstractions with arbitrary domains, (Proc. SAS’11, (2011)), 334-350
[8] Ferrer Fioriti, L. M.; Hermanns, H., Heuristics for probabilistic timed automata with abstraction refinement, (Proc. MMB/DFT’12, (2012)), 151-165
[9] Hahn, E. M.; Hermanns, H.; Wachter, B.; Zhang, L., PASS: abstraction refinement for infinite probabilistic models, (Proc. TACAS’10, (2010))
[10] Hartmanns, A.; Hermanns, H., A modest approach to checking probabilistic timed automata, (Proc. QEST’09, (2009), IEEE), 187-196
[11] Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic CEGAR, (Proc. CAV’08, LNCS, vol. 5123, (2008), Springer), 162-175 · Zbl 1155.68438
[12] Kattenbelt, M.; Kwiatkowska, M.; Norman, G.; Parker, D., Abstraction refinement for probabilistic software, (Proc. VMCAI’09, (2009)) · Zbl 1206.68090
[13] Kattenbelt, M.; Kwiatkowska, M.; Norman, G.; Parker, D., A game-based abstraction-refinement framework for Markov decision processes, Form. Methods Syst. Des., 36, 3, 246-280, (2010) · Zbl 1233.90276
[14] Kemeny, J.; Snell, J.; Knapp, A., Denumerable Markov chains, (1976), Springer-Verlag · Zbl 0348.60090
[15] Komuravelli, A.; Pasareanu, C.; Clarke, E., Assume-guarantee abstraction refinement for probabilistic systems, (Proc. CAV’12, (2012)), 310-326
[16] Kwiatkowska, M.; Norman, G.; Parker, D., Stochastic games for verification of probabilistic timed automata, (Proc. FORMATS’09, (2009)), 212-227 · Zbl 1262.68125
[17] Kwiatkowska, M.; Norman, G.; Parker, D., A framework for verification of software with time and probabilities, (Proc. FORMATS’10, (2010)), 25-45 · Zbl 1290.68035
[18] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (Proc. CAV’11, (2011)), 585-591
[19] Kwiatkowska, M.; Norman, G.; Parker, D.; Sproston, J., Performance analysis of probabilistic timed automata using digital clocks, Form. Methods Syst. Des., 29, 33-78, (2006) · Zbl 1105.68063
[20] Kwiatkowska, M.; Norman, G.; Segala, R.; Sproston, J., Automatic verification of real-time systems with discrete probability distributions, Theor. Comput. Sci., 282, 101-150, (2002) · Zbl 1050.68094
[21] Kwiatkowska, M.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, Inf. Comput., 205, 7, 1027-1077, (2007) · Zbl 1122.68075
[22] Norris, J., Markov chains, Cambridge Series in Statistical and Probabilistic Mathematics, (1998), Cambridge University Press · Zbl 0938.60058
[23] Tripakis, S., Verifying progress in timed systems, (Proc. ARTS’99, LNCS, vol. 1601, (1999), Springer), 299-314
[24] Wachter, B.; Zhang, L., Best probabilistic transformers, (Proc. VMCAI’10, LNCS, vol. 5944, (2010), Springer), 362-379 · Zbl 1273.68244
[25] Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H.; Hahn, E. M., Safety verification for probabilistic hybrid systems, (Proc. CAV’08, (2008))
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.