Abstract
The purpose of the paper is to provide an automatic transformation of parallel programs of an imperative probabilistic guarded command language (called Probmela) into probabilistic reactive module specifications. The latter serve as basis for the input language of the symbolic MTBDD-based probabilistic model checker PRISM, while Probmela is the modeling language of the model checker LiQuor which relies on an enumerative approach and supports partial order reduction and other reduction techniques. By providing the link between the model checkers PRISM and LiQuor, our translation supports comparative studies of different verification paradigms and can serve to use the (more comfortable) guarded command language for a MTBDD-based quantitative analysis. The challenges were (1) to ensure that the translation preserves the Markov decision process semantics, (2) the efficiency of the translation and (3) the compactness of the symbolic BDD-representation of the generated PRISM-language specifications.
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.
References
Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods in System Design: An International Journal 15(1), 7–48 (1999)
Baier, C., Ciesinski, F., Größer, M.: Probmela: a modeling language for communicating probabilistic systems. In: Proceeding MEMOCODE (2004)
Baldamus, M., Schröder-Babo, J.: p2b: a translation utility for linking promela and symbolic model checking (tool paper). In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 183–191. Springer, Heidelberg (2001)
Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST, pp. 131–132. IEEE CS Press, Los Alamitos (2007)
Ciesinski, F., Baier, C., Groesser, M., Klein, J.: Reduction techniques for model checking markov decision processes (submitted for publication, 2008)
Clarke, E., Fujita, M., McGeer, P., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: International Workshop on Logic Synthesis, Tahoe City (1993)
Größer, M., Norman, G., Baier, C., Ciesinski, F., Kwiatkoswka, M., Parker, D.: On reduction criteria for probabilistic reward models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 309–320. Springer, Heidelberg (2006)
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: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems 56(1-2), 23–67 (2003)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Minato, S.i., Ishiura, N., Yajima, S.: Shared binary decision diagram with attributed edges for efficient boolean function manipulation. In: DAC 1990: Proceedings of the 27th ACM/IEEE conference on Design automation, pp. 52–57. ACM Press, New York (1990)
Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation 88(1) (1990)
Lehmann, D., Rabin, M.O.: On the advantage of free choice: A symmetric and fully distributed solution to the Dining Philosophers problem (extended abstract). In: Proc. Eighth Ann. ACM Symp. on Principles of Programming Languages, pp. 133–138 (1981); A classic paper in the area of randomized distributed algorithms. They show there is no deterministic, deadlock-free, truly distributed and symmetric solution to the Dining Philosophers problem, and describe a simple probabilistic alternative.
Malik, S., Wang, A.R., Brayton, R.K.: Logic verification using binary decision diagrams in a logic synthesis environment. In: ICCAD 1988: Digest of technical papers, pp. 6–9. IEEE Press, Los Alamitos (1988)
McMillan, K.L.: The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)
Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design: OBDD-Foundations and Applications. Springer, Heidelberg (1998)
Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)
PRISM web site, http://www.prismmodelchecker.org
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic Decision Diagrams and Their Applications. In: IEEE /ACM International Conference on CAD, Santa Clara, California, November 1993, pp. 188–191. ACM/IEEE, IEEE Computer Society Press (1993)
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2(2), 250–273 (1995)
Beaudenon, V., Encrenaz, E., Taktak, S.: Data decision diagrams for promela systems analysis. In: Software Tools and Technology Transfert (accepted for publication, 2008)
Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Applications. In: Monographs on Discrete Mathematics and Applications. Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciesinski, F., Baier, C., Größer, M., Parker, D. (2008). Generating Compact MTBDD-Representations from Probmela Specifications. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)