×

A linear process-algebraic format with data for probabilistic automata. (English) Zbl 1283.68246

A novel linear process-algebraic format for probabilistic automata is presented. The key ingredient is a symbolic transformation of probabilistic process algebra terms (terms of prCRL which is restricted \(\mu \text{CRL}\) with a probabilistic choice operator) that incorporate data into this linear format while preserving strong probabilistic bisimulation. This generalizes similar techniques for traditional process algebras with data, and treats data and data-dependent probabilistic choice in a fully symbolic manner, leading to the symbolic analysis of parameterized probabilistic systems. Several reduction techniques that can be easily applied to the presented models are discussed. A validation of the presented approach is presented on a benchmark case study, namely leader election protocols. It shows significant reductions of states, transitions as well as running time.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

E-LOTOS; PRISM; MoDeST; CEGAR; CADP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Groote, J. F.; Ponse, A., The syntax and semantics of \(\mu\) CRL, (Proc. of Algebra of Communicating Processes, Workshops in Computing (1995), Springer), 26-62
[2] Garavel, H.; Sighireanu, M., Towards a second generation of formal description techniques — rationale for the design of E-LOTOS, (Proc. of the 3rd Int. Workshop on Formal Methods for Industrial Critical Systems. Proc. of the 3rd Int. Workshop on Formal Methods for Industrial Critical Systems, FMICS (1998), CWI), 198-230
[3] Hinton, A.; Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM: a tool for automatic verification of probabilistic systems, (Proc. of the 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Proc. of the 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, LNCS, vol. 3920 (2006), Springer), 441-444
[4] Baier, C.; Ciesinski, F.; Größer, M., PROBMELA: a modeling language for communicating probabilistic processes, (Proc. of the 2nd ACM/IEEE Int. Conf. on Formal Methods and Models for Co-Design. Proc. of the 2nd ACM/IEEE Int. Conf. on Formal Methods and Models for Co-Design, MEMOCODE (2004), IEEE), 57-66
[5] Bohnenkamp, H. C.; D’Argenio, P. R.; Hermanns, H.; Katoen, J.-P., MODEST: a compositional modeling formalism for hard and softly timed systems, IEEE Transactions of Software Engineering, 32, 812-830 (2006)
[6] D’Argenio, P. R.; Jeannet, B.; Jensen, H. E.; Larsen, K. G., Reachability analysis of probabilistic systems by successive refinements, (Proc. of the Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification. Proc. of the Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, PAPM-PROBMIV. Proc. of the Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification. Proc. of the Joint Int. Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, PAPM-PROBMIV, LNCS, vol. 2165 (2001), Springer), 39-56 · Zbl 1007.68131
[7] de Alfaro, L.; Roy, P., Magnifying-lens abstraction for Markov decision processes, (Proc. of the 19th Int. Conf. on Computer Aided Verification. Proc. of the 19th Int. Conf. on Computer Aided Verification, CAV. Proc. of the 19th Int. Conf. on Computer Aided Verification. Proc. of the 19th Int. Conf. on Computer Aided Verification, CAV, LNCS, vol. 4590 (2007), Springer), 325-338 · Zbl 1135.68486
[8] Henzinger, T. A.; Mateescu, M.; Wolf, V., Sliding window abstraction for infinite Markov chains, (Proc. of the 21st Int. Conf. on Computer Aided Verification. Proc. of the 21st Int. Conf. on Computer Aided Verification, CAV. Proc. of the 21st Int. Conf. on Computer Aided Verification. Proc. of the 21st Int. Conf. on Computer Aided Verification, CAV, LNCS, vol. 5643 (2009), Springer), 337-352 · Zbl 1242.60079
[9] Katoen, J.-P.; Klink, D.; Leucker, M.; Wolf, V., Three-valued abstraction for continuous-time Markov chains, (Proc. of the 19th Int. Conf. on Computer Aided Verification. Proc. of the 19th Int. Conf. on Computer Aided Verification, CAV. Proc. of the 19th Int. Conf. on Computer Aided Verification. Proc. of the 19th Int. Conf. on Computer Aided Verification, CAV, LNCS, vol. 4590 (2007), Springer), 311-324 · Zbl 1135.68476
[10] Kwiatkowska, M. Z.; Norman, G.; Parker, D., Game-based abstraction for Markov decision processes, (Proc. of the 3rd Int. Conf. on Quantitative Evaluation of Systems. Proc. of the 3rd Int. Conf. on Quantitative Evaluation of Systems, QEST (2006), IEEE), 157-166
[11] Kattenbelt, M.; Kwiatkowska, M. Z.; Norman, G.; Parker, D., A game-based abstraction-refinement framework for Markov decision processes, Formal Methods in System Design, 36, 246-280 (2010) · Zbl 1233.90276
[12] Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic CEGAR, (Proc. of the 20th Int. Conf. on Computer Aided Verification. Proc. of the 20th Int. Conf. on Computer Aided Verification, CAV. Proc. of the 20th Int. Conf. on Computer Aided Verification. Proc. of the 20th Int. Conf. on Computer Aided Verification, CAV, LNCS, vol. 5123 (2008), Springer), 162-175 · Zbl 1155.68438
[13] Kattenbelt, M.; Kwiatkowska, M. Z.; Norman, G.; Parker, D., Abstraction refinement for probabilistic software, (Proc. of the 19th Int. Conf. on Verification, Model Checking, and Abstract Interpretation. Proc. of the 19th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, VMCAI. Proc. of the 19th Int. Conf. on Verification, Model Checking, and Abstract Interpretation. Proc. of the 19th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, VMCAI, LNCS, vol. 5403 (2009), Springer), 182-197 · Zbl 1206.68090
[14] Morgan, C.; McIver, A., pGCL: formal reasoning for random algorithms, South African Computer Journal, 22, 14-27 (1999)
[15] Bezem, M.; Groote, J. F., Invariants in process algebra with data, (Proc. of the 5th Int. Conf. on Concurrency Theory. Proc. of the 5th Int. Conf. on Concurrency Theory, CONCUR. Proc. of the 5th Int. Conf. on Concurrency Theory. Proc. of the 5th Int. Conf. on Concurrency Theory, CONCUR, LNCS, vol. 836 (1994), Springer), 401-416
[16] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Information and Computation, 94, 1-28 (1991) · Zbl 0756.68035
[17] D. Bosscher, A. Ponse, Translating a process algebra with symbolic data values to linear format, in: Proc. of the 1st Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, vol. NS-95-2 BRICS Notes Series, University of Aarhus, 1995, pp. 119-130.; D. Bosscher, A. Ponse, Translating a process algebra with symbolic data values to linear format, in: Proc. of the 1st Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, vol. NS-95-2 BRICS Notes Series, University of Aarhus, 1995, pp. 119-130.
[18] Y.S. Usenko, Linearization in \(\mu \); Y.S. Usenko, Linearization in \(\mu \)
[19] van den Brand, P. C.W.; Reniers, M. A.; Cuijpers, P. J.L., Linearization of hybrid processes, Journal of Logic and Algebraic Programming, 68, 54-104 (2006) · Zbl 1088.68137
[20] Groote, J. F.; Springintveld, J., Focus points and convergent process operators: a proof strategy for protocol verification, Journal of Logic and Algebraic Programming, 49, 31-60 (2001) · Zbl 1015.68175
[21] Fokkink, W.; Pang, J.; van de Pol, J. C., Cones and foci: A mechanical framework for protocol verification, Formal Methods in System Design, 29, 1-31 (2006) · Zbl 1103.68652
[22] J.F. Groote, B. Lisser, Computer assisted manipulation of algebraic process specifications, Technical Report SEN-R0117, CWI, 2001.; J.F. Groote, B. Lisser, Computer assisted manipulation of algebraic process specifications, Technical Report SEN-R0117, CWI, 2001.
[23] van de Pol, J. C.; Timmer, M., State space reduction of linear processes using control flow reconstruction, (Proc. of the 7th Int. Symp. on Automated Technology for Verification and Analysis. Proc. of the 7th Int. Symp. on Automated Technology for Verification and Analysis, ATVA. Proc. of the 7th Int. Symp. on Automated Technology for Verification and Analysis. Proc. of the 7th Int. Symp. on Automated Technology for Verification and Analysis, ATVA, LNCS, vol. 5799 (2009), Springer), 54-68 · Zbl 1262.68133
[24] Espada, M. V.; van de Pol, J. C., An abstract interpretation toolkit for \(\mu\) CRL, Formal Methods in System Design, 30, 249-273 (2007) · Zbl 1116.68058
[25] Blom, S. C.C.; Lisser, B.; van de Pol, J. C.; Weber, M., A database approach to distributed state-space generation, Journal of Logic and Computation, 21, 45-62 (2011) · Zbl 1213.68364
[26] Blom, S. C.C.; van de Pol, J. C., Symbolic reachability for process algebras with recursive data types, (Proc. of the 5th Int. Colloquium on Theoretical Aspects of Computing. Proc. of the 5th Int. Colloquium on Theoretical Aspects of Computing, ICTAC. Proc. of the 5th Int. Colloquium on Theoretical Aspects of Computing. Proc. of the 5th Int. Colloquium on Theoretical Aspects of Computing, ICTAC, LNCS, vol. 5160 (2008), Springer), 81-95 · Zbl 1161.68613
[27] Groote, J. F.; Mateescu, R., Verification of temporal properties of processes in a setting with data, (Proc. of the 7th Int. Conf. on Algebraic Methodology and Software Technology. Proc. of the 7th Int. Conf. on Algebraic Methodology and Software Technology, AMAST. Proc. of the 7th Int. Conf. on Algebraic Methodology and Software Technology. Proc. of the 7th Int. Conf. on Algebraic Methodology and Software Technology, AMAST, LNCS, vol. 1548 (1998), Springer), 74-90 · Zbl 0926.03036
[28] Groote, J. F.; Willemse, T. A.C., Model-checking processes with data, Science of Computer Programming, 56, 251-273 (2005) · Zbl 1082.68067
[29] Blom, S. C.C.; van de Pol, J. C., State space reduction by proving confluence, (Proc. of the 14th Int. Conf. on Computer Aided Verification. Proc. of the 14th Int. Conf. on Computer Aided Verification, CAV. Proc. of the 14th Int. Conf. on Computer Aided Verification. Proc. of the 14th Int. Conf. on Computer Aided Verification, CAV, LNCS, vol. 2404 (2002), Springer), 596-609 · Zbl 1010.68527
[30] Katoen, J.-P.; van de Pol, J. C.; Stoelinga, M. I.A.; Timmer, M., A linear process-algebraic format for probabilistic systems with data, (Proc. of the 10th Int. Conf. on Application of Concurrency to System Design. Proc. of the 10th Int. Conf. on Application of Concurrency to System Design, ACSD (2010), IEEE), 213-222
[31] R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, Ph.D. thesis, MIT, 1995.; R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, Ph.D. thesis, MIT, 1995.
[32] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[33] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects of Computing, 6, 512-535 (1994) · Zbl 0820.68113
[34] Bergstra, J. A.; Klop, J. W., \(ACP_\tau \): A universal axiom system for process specification, (Algebraic Methods: Theory, Tools and Applications. Algebraic Methods: Theory, Tools and Applications, LNCS, vol. 394 (1989), Springer), 447-463
[35] Timmer, M.; Stoelinga, M. I.A.; van de Pol, J. C., Confluence reduction for probabilistic systems, (Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, LNCS, vol. 6605 (2011), Springer), 311-325 · Zbl 1316.68077
[36] M. Timmer, M.I.A. Stoelinga, J.C. van de Pol, Confluence reduction for probabilistic systems (extended version), Technical Report 1011.2314, ArXiv e-prints, 2010.; M. Timmer, M.I.A. Stoelinga, J.C. van de Pol, Confluence reduction for probabilistic systems (extended version), Technical Report 1011.2314, ArXiv e-prints, 2010. · Zbl 1316.68077
[37] Garavel, H.; Lang, F.; Mateescu, R.; Serwe, W., CADP 2010: a toolbox for the construction and analysis of distributed processes, (Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Proc. of the 17th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, LNCS, vol. 6605 (2011), Springer), 372-387 · Zbl 1316.68074
[38] Itai, A.; Rodeh, M., Symmetry breaking in distributed networks, Information and Computation, 88, 60-87 (1990) · Zbl 0705.68020
[39] Fokkink, W.; Pang, J., Simplifying Itai-Rodeh leader election for anonymous rings, (Proc. of the 4th Int. Workshop on Automated Verification of Critical Systems. Proc. of the 4th Int. Workshop on Automated Verification of Critical Systems, AVoCS. Proc. of the 4th Int. Workshop on Automated Verification of Critical Systems. Proc. of the 4th Int. Workshop on Automated Verification of Critical Systems, AVoCS, ENTCS, vol. 128(6) (2005), Elsevier), 53-68 · Zbl 1272.68041
[40] J.-P. Katoen, J.C. van de Pol, M.I.A. Stoelinga, M. Timmer, A linear process algebraic format for probabilistic systems with data (extended version), Technical Report, TR-CTIT-10-11, CTIT, University of Twente, 2010.; J.-P. Katoen, J.C. van de Pol, M.I.A. Stoelinga, M. Timmer, A linear process algebraic format for probabilistic systems with data (extended version), Technical Report, TR-CTIT-10-11, CTIT, University of Twente, 2010. · Zbl 1283.68246
[41] M.I.A. Stoelinga, Alea jacta est: verification of probabilistic, real-time and parametric systems, Ph.D. thesis, University of Nijmegen, 2002.; M.I.A. Stoelinga, Alea jacta est: verification of probabilistic, real-time and parametric systems, Ph.D. thesis, University of Nijmegen, 2002.
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.