Abstract
Multi-Terminal Binary Decision Diagrams (MTBDDs) have been successfully applied in symbolic model checking of probabilistic systems. In this paper we propose an encoding method for Probabilistic Timed Automata (PTA) based on MTBDDs. The timing information is encoded via placeholders stored in the MTBDDs that are independent of how the timing information is represented. Using the Colorado University Decision Diagrams (CUDD) package, an experimental model checker is implemented, which supports probabilistic reachability model checking via the forward algorithm. We use Difference Bound Matrices (DBMs) and Difference Decision Diagrams (DDDs) for representing timing information and present experimental results on three case studies. Our key contribution is a general placeholder encoding method for Probabilistic Timed Automata and an experimental MTBDD-based model checker which has been partly integrated with PRISM. This is the first symbolic implementation of the forward probabilistic reachability algorithm.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
PRISM WebSite, http://www.cs.bham.ac.uk/~dxp/prism/
Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)
Bengtsson, J., Griffioen, W., Kristoffersen, K., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Automated verification of an audio-control protocol using UPPAAL. Journal of Logic and Algebric Programming 52(3), 163–181 (2002)
Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: Proc. 18TH IEEE Real-Time Systems Symposium, pp. 25–34. IEEE CS Press, Los Alamitos (1997)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677–691 (1986)
Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: Proc. IWLS 1993, pp. 1–15 (1993); Also available in Formal Methods in System Design 10(2/3), 149–169 (1997)
Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. In: Proc. 7th FMICS 2002. Electronic Notes in Theoretical Computer Science, vol. 66(2). Elsevier, Amsterdam (2002)
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000)
Hermanns, H., Kwiatkowska, M., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming 56(1-2), 23–67 (2003)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002)
Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 105–120. Springer, Heidelberg (2004)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 101–150 (2002)
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Special Issue of Formal Aspects of Computing 14, 295–318 (2003)
Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 293–308. Springer, Heidelberg (2004)
Møller, J., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Fully symbolic model checking of timed systems using difference decision diagrams. In: Workshop on Symbolic Model Checking, The IT University of Copenhagen, Denmark, June 1999, vol. 23 (1999)
Seshia, S.A., Bryant, R.E.: A boolean approach to unbounded, fully symbolic model checking of timed automata. Technical Report CMU-CS-03-117, Carnegie Mellon University (2003)
Somenzi, F.: CUDD: CU Decision Diagram Package Release (1998)
Wang, F.: Efficient verification of timed automata with BDD-like data-structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 189–205. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, F., Kwiatkowska, M. (2005). An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_29
Download citation
DOI: https://doi.org/10.1007/11562948_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)