Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process
Pages 229 - 244
Abstract
Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and compositional verification such as assume-guarantee reasoning are two promising techniques to overcome this barrier. In this paper, we propose a probabilistic symbolic compositional verification approach (PSCV) to verify probabilistic systems where each component is a Markov decision process (MDP). PSCV starts by encoding implicitly the system components using compact data structures. To establish the symbolic compositional verification process, we propose a sound and complete symbolic assume-guarantee reasoning rule. To attain completeness of the symbolic assume-guarantee reasoning rule, we propose to model assumptions using interval MDP. In addition, we give a symbolic MTBDD-learning algorithm to generate automatically the symbolic assumptions. Moreover, we propose to use causality to generate small counterexamples in order to refine the conjecture assumptions. Experimental results suggest promising outlooks for our probabilistic symbolic compositional approach.
References
[1]
Abate A, Prandini M, Lygeros J, Sastry S (2008) Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11):2724---2734
[2]
Aljazzar H, Leue S (2011) $$K^{*}$$K?: a heuristic search algorithm for finding the k shortest paths. Artif Intell 175(18):2129---2154
[3]
Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87---106
[4]
Baier C, Katoen JP, Larsen KG (2008) Principles of model checking. MIT Press, Cambridge
[5]
Baier C, Kwiatkowska M (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125---155
[6]
Benedikt M, Lenhardt R, Worrell J (2013) LTL model checking of interval Markov chains. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 32---46
[7]
Bouchekir R, Boukhedouma S, Boukala MC (2016) Symbolic probabilistic analysis and verification of inter-organizational workflow. In: International conference on information technology for organizations development (IT4OD). IEEE, pp 1---8
[8]
Bouchekir R, Boukhedouma S, Boukala M (2016) Automatic compositional verification of probabilistic safety properties for inter-organisational workflow processes. In: Proceedings of the 6th international conference on simulation and modeling methodologies, technologies and applications--vol 1: SIMULTECH, ISBN:978-989-758-199-1, pp 244---253
[9]
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: $$10^{20}$$1020 states and beyond. Inf Comput 98(2):142---170
[10]
Chatterjee K, Sen K, Henzinger TA (2008) Model-checking $$\omega $$?-regular properties of interval Markov chains. In: International conference on foundations of software science and computational structures. Springer, Berlin, pp 302---317
[11]
Chen YF, Clarke M, Farzan A, Tsai M, Tsay YK, Wang BY (2010) Automated assume-guarantee reasoning through implicit learning. In: International conference on computer aided verification. Springer, Berlin, pp 511---526
[12]
Ciesinski F, Baier C, Grober M, Parker D (2008) Generating compact MTBDD-representations from Probmela specifications. In: International SPIN workshop on model checking of software. Springer, Berlin, pp 60---76
[13]
Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 331---346
[14]
Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logic of programs. Springer, Berlin, pp 52---71
[15]
Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst (TOPLAS) 8(2):244---263
[16]
Debbi H, Debbi A, Bourahla M (2016) Debugging of probabilistic systems using structural equation modelling. Int J Crit Comput Based Syst 6(4):250---274
[17]
Debbi H, Bourahla M (2013) Generating diagnoses for probabilistic model checking using causality. CIT. J Comput Inf Technol 21(1):13---22
[18]
Duflot M, Fribourg L, Picaronny C (2004) Randomized dining philosophers without fairness assumption. Distrib Comput 17(1):65---76
[19]
Fujita M, McGeer PC, Yang JY (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form Methods Syst Des 10(2---3):149---169
[20]
Fehnker A, Gao P (2006) Formal verification and simulation for performance analysis for probabilistic broadcast protocols. In: International conference on ad-hoc networks and wireless. Springer, Berlin, pp 128---141
[21]
Feng L, Kwiatkowska M, Parker D (2010) Compositional verification of probabilistic systems using learning. In: Seventh international conference on the quantitative evaluation of systems (QEST). IEEE, pp 133---142
[22]
Feng L (2013) On learning assumptions for compositional verification of probabilistic systems. Doctoral dissertation, University of Oxford
[23]
Hasson H, Jonsson B (1994) A logic for reasoning about time and probability. Form Asp Comput 6:512---535
[24]
Hart S (1984) Probabilistic temporal logics for finite and bounded models. In: Proceedings of the sixteenth annual ACM symposium on theory of computing. ACM, pp 1---13
[25]
He F, Gao X, Wang M, Wang BY, Zhang L (2016) Learning weighted assumptions for compositional verification of Markov decision processes. ACM Trans Softw Eng Methodol 25(3):21
[26]
Hermanns H, Kwiatkowska M, Norman G, Parker D, Siegle M (2003) On the use of MTBDDs for performability analysis and verification of stochastic systems. J Log Algebr Program 56(1---2):23---67
[27]
Hurd J (2003) Formal verification of probabilistic algorithms (No. UCAM-CL-TR-566). University of Cambridge, Computer Laboratory
[28]
Israeli A, Jalfon M (1990) Token management schemes and random walks yield self-stabilizing mutual exclusion. In: Proceedings of the ninth annual ACM symposium on principles of distributed computing. ACM, pp 119---131
[29]
Jansen N, Wimmer R, Abraham E, Zajzon B, Katoen JP, Becker B, Schuster J (2014) Symbolic counterexample generation for large discrete-time Markov chains. Sci Comput Program 91:90---114
[30]
Knuth D (1979) The complexity of nonuniform random number generation. In: Algorithm and complexity, new directions and results. Academic press, pp 357---428
[31]
Komuravelli A, Pasareanu CS, Clarke EM (2012) Learning probabilistic systems from tree samples. In: Proceedings of the 2012 27th annual IEEE/ACM symposium on logic in computer science. IEEE Computer Society, pp 441---450
[32]
Kwiatkowska M, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 23---37
[33]
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: International conference on computer aided verification. Springer, Berlin, pp 585---591
[34]
Lehmann D, Shelah S (1982) Reasoning with time and chance. Inf Control 53(3):165---198
[35]
Lehmann D, Rabin MO (1981) On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 133---138
[36]
Larsen KG, Pettersson P, Yi W (1995) Compositional and symbolic model-checking of real-time systems. In: 16th IEEE proceedings of real-time systems symposium, 1995. IEEE, pp 76---87
[37]
Mao M, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B (2012) Learning Markov decision processes for model checking. arXiv preprint arXiv:1212.3873
[38]
McMillan KL (1993) Symbolic model checking. In: Symbolic model checking. Springer, New York, pp 25---60
[39]
Parker DA (2002) Implementation of symbolic model checking for probabilistic systems. Doctoral dissertation, University of Birmingham
[40]
Pnueli A, Zuck L (1986) Verification of multiprocess probabilistic protocols. Distrib Comput 1(1):53---72
[41]
Pasareanu CS, Giannakopoulou D, Bobaru MG, Cobleigh JM, Barringer H (2008) Learning to divide and conquer: applying the $$L^{*}$$L? algorithm to automate assume-guarantee reasoning. Form Methods Syst Des 32(3):175---205
[42]
Segala R (1995) Modelling and verification of randomized distributed real time systems. Ph.D. thesis, Massachusetts Institute of Technology
[43]
Steel G (2006) Formal analysis of PIN block attacks. Theor Comput Sci 367(1---2):257---270
[44]
Vardi MY (1985) Automatic verification of probabilistic concurrent finite state programs. In: 26th annual symposium on foundations of computer science. IEEE, pp 327---338
[45]
Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1---37
[46]
Vardi MY (1999) Probabilistic linear-time model checking: an overview of the automata-theoretic approach. In: International AMAST workshop on aspects of real-time systems and concurrent and distributed software. Springer, Berlin, pp 265---276
- Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process
Recommendations
Symbolic assume-guarantee reasoning through BDD learning
ICSE 2014: Proceedings of the 36th International Conference on Software EngineeringBoth symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the ...
Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes
Probabilistic models are widely deployed in various systems. To ensure their correctness, verification techniques have been developed to analyze probabilistic systems. We propose the first sound and complete learning-based compositional verification ...
Automatic symbolic compositional verification by learning assumptions
Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2018 Springer-Verlag London Ltd., part of Springer Nature.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 September 2018
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 14 Nov 2024
Other Metrics
Citations
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in