Lập luận giả thiết-đảm bảo dựa trên học tập cho quá trình quyết định Markov sử dụng quá trình Markov khoảng

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 Aljazzar H, Leue S (2011) \(K^{*}\): a heuristic search algorithm for finding the k shortest paths. Artif Intell 175(18):2129–2154 Angluin D (1987) Learning regular sets from queries and counterexamples. Inf Comput 75(2):87–106 Baier C, Katoen JP, Larsen KG (2008) Principles of model checking. MIT Press, Cambridge Baier C, Kwiatkowska M (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125–155 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 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 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 Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: \(10^{20}\) states and beyond. Inf Comput 98(2):142–170 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 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 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 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 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 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 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 Debbi H, Bourahla M (2013) Generating diagnoses for probabilistic model checking using causality. CIT. J Comput Inf Technol 21(1):13–22 Duflot M, Fribourg L, Picaronny C (2004) Randomized dining philosophers without fairness assumption. Distrib Comput 17(1):65–76 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 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 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 Feng L (2013) On learning assumptions for compositional verification of probabilistic systems. Doctoral dissertation, University of Oxford Hasson H, Jonsson B (1994) A logic for reasoning about time and probability. Form Asp Comput 6:512–535 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 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 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 Hurd J (2003) Formal verification of probabilistic algorithms (No. UCAM-CL-TR-566). University of Cambridge, Computer Laboratory 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 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 Knuth D (1979) The complexity of nonuniform random number generation. In: Algorithm and complexity, new directions and results. Academic press, pp 357–428 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 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 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 Lehmann D, Shelah S (1982) Reasoning with time and chance. Inf Control 53(3):165–198 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 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 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 McMillan KL (1993) Symbolic model checking. In: Symbolic model checking. Springer, New York, pp 25–60 Parker DA (2002) Implementation of symbolic model checking for probabilistic systems. Doctoral dissertation, University of Birmingham Pnueli A, Zuck L (1986) Verification of multiprocess probabilistic protocols. Distrib Comput 1(1):53–72 Pasareanu CS, Giannakopoulou D, Bobaru MG, Cobleigh JM, Barringer H (2008) Learning to divide and conquer: applying the \(L^{*}\) algorithm to automate assume-guarantee reasoning. Form Methods Syst Des 32(3):175–205 Segala R (1995) Modelling and verification of randomized distributed real time systems. Ph.D. thesis, Massachusetts Institute of Technology Steel G (2006) Formal analysis of PIN block attacks. Theor Comput Sci 367(1–2):257–270 Vardi MY (1985) Automatic verification of probabilistic concurrent finite state programs. In: 26th annual symposium on foundations of computer science. IEEE, pp 327–338 Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1–37 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