Abstract
This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.
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
Baier, C., D’Argenio, P.R., Größer, M.: Partial order reduction for probabilistic branching time. In: Proc. of the 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL). ENTCS, vol. 153(2), pp. 97–116 (2006)
Baier, C., Größer, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: Proc. of the 1st International Conference on Quantitative Evaluation of Systems (QEST), pp. 230–239. IEEE Computer Society, Los Alamitos (2004)
Blom, S.C.C.: Partial τ-confluence for efficient state space generation. Technical Report SEN-R0123, CWI, Amsterdam (2001)
Blom, S.C.C., van de Pol, J.C.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 596–609. Springer, Heidelberg (2002)
D’Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: Proc. of the 1st International Conference on Quantitative Evaluation of Systems (QEST), pp. 240–249. IEEE Computer Society, Los Alamitos (2004)
Fokkink, W., Pang, J.: Simplifying Itai-Rodeh leader election for anonymous rings. In: Proc. of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS). ENTCS, vol. 128(6), pp. 53–68 (2005)
Giro, S., D’Argenio, P.R., Ferrer Fioriti, L.M.: Partial order reduction for probabilistic systems: A revision for distributed schedulers. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 338–353. Springer, Heidelberg (2009)
Groote, J.F., Sellink, M.P.A.: Confluence for process verification. Theoretical Computer Science 170(1-2), 47–81 (1996)
Größer, M.: Reduction Methods for Probabilistic Model Checking. PhD thesis, Technische Universität Dresden (2008)
Katoen, J.-P., van de Pol, J.C., Stoelinga, M.I.A., Timmer, M.: A linear process-algebraic format for probabilistic systems with data. In: Proc. of the 10th International Conference on Application of Concurrency to System Design (ACSD), pp. 213–222. IEEE Computer Society, Los Alamitos (2010)
De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Pace, G.J., Lang, F., Mateescu, R.: Calculating τ-confluence compositionally. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 446–459. Springer, Heidelberg (2003)
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computation 2(2), 250–273 (1995)
Stoelinga, M.I.A.: Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen (2002)
Timmer, M., Stoelinga, M.I.A., van de Pol, J.C.: Confluence reduction for probabilistic systems (extended version). Technical Report 1011.2314, ArXiv e-prints (2010)
van de Pol, J.C., Timmer, M.: State space reduction of linear processes using control flow reconstruction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 54–68. Springer, Heidelberg (2009)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Timmer, M., Stoelinga, M., van de Pol, J. (2011). Confluence Reduction for Probabilistic Systems. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)