Abstract
Several formal models combine probabilistic and nondeterministic features. To allow their probabilistic simulation and statistical model checking by means of pseudo-random number sampling, all sources of nondeterminism must first be quantified. However, current tools offer limited flexibility for the user to define how the nondeterminism should be quantified. In this paper, we propose an expressive probabilistic strategy language that allows the user to define complex strategies for quantifying the nondeterminism in probabilistic rewrite theories. We have implemented PSMaude, a tool that extends Maude with a probabilistic simulator and a statistical model checker for our language. We illustrate the convenience of being able to define different probabilistic strategies on top of a system by a cloud computing example, where different load balancing policies can be specified by different probabilistic strategies. We then use PSMaude to analyze the QoS provided by different policies.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Agha, G.A., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. ENTCS 153(2) (2006)
AlTurki, M., Meseguer, J.: PVeStA: A parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)
AlTurki, M., Meseguer, J., Gunter, C.A.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. ENTCS 234 (2009)
Bentea, L.: The PSMaude tool home page: http://folk.uio.no/lucianb/prob-strat/
Bentea, L., Ölveczky, P.C.: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing. Manuscript: http://folk.uio.no/lucianb/publications/2012/pstrat-cloud.pdf
Bernardo, M., De Nicola, R., Loreti, M.: Uniform labeled transition systems for nondeterministic, probabilistic, and stochastic processes. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010. LNCS, vol. 6084, pp. 35–56. Springer, Heidelberg (2010)
Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: A compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812–830 (2006)
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.E., Ringeissen, C.: An overview of ELAN. Electronic Notes in Theoretical Computer Science 15 (1998)
Bournez, O., Kirchner, C.: Probabilistic rewrite strategies. Applications to ELAN. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 252–266. Springer, Heidelberg (2002)
Bruni, R., Corradini, A., Gadducci, F., Lluch Lafuente, A., Vandin, A.: Modelling and analyzing adaptive self-assembly strategies with Maude. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 118–138. Springer, Heidelberg (2012)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011)
Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78–93. Springer, Heidelberg (2012)
Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Logic in Computer Science, pp. 342–351 (2010)
Eker, S., Martí-Oliet, N., Meseguer, J., Verdejo, A.: Deduction, strategies, and rewriting. Electronic Notes in Theoretical Computer Science 174(11), 3–25 (2007)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6 (1994)
Katelman, M., Meseguer, J., Hou, J.: Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 150–169. Springer, Heidelberg (2008)
Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic rewrite theories: Unifying models, logics and tools. Technical report UIUCDCS-R-2003-2347, Department of Computer Science, University of Illinois at Urbana-Champaign (2003)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)
Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with generalized stochastic Petri nets. SIGMETRICS Performance Evaluation Review 26(2), 2 (1998)
Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoretical Computer Science 285(2) (2002)
Martí-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. Electronic Notes in Theoretical Computer Science 117, 417–441 (2005)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1) (1992)
Meseguer, J.: A rewriting logic sampler. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 1–28. Springer, Heidelberg (2005)
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005)
Sen, K., Viswanathan, M., Agha, G.A.: VeStA: A statistical model-checker and analyzer for probabilistic systems. In: QEST 2005. IEEE Computer Society (2005)
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Bentea, L., Ölveczky, P.C. (2013). A Probabilistic Strategy Language for Probabilistic Rewrite Theories and Its Application to Cloud Computing. In: Martí-Oliet, N., Palomino, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2012. Lecture Notes in Computer Science, vol 7841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37635-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-37635-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37634-4
Online ISBN: 978-3-642-37635-1
eBook Packages: Computer ScienceComputer Science (R0)