Cited By
View all- Mccabe-Dansted JReynolds M(2017)To be fair, use bundlesAnnals of Mathematics and Artificial Intelligence10.1007/s10472-017-9546-x80:3-4(317-364)Online publication date: 1-Aug-2017
Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications
Abstract
In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In fact, PCTLK enjoys two epistemic modalities Ki for knowledge and PrźbKi$Pr_{\triangledown b}K_{i}$ for probabilistic knowledge. The approach presented for verifying PCTLK specifications in such concurrent systems is based on a transformation technique. More precisely, we convert PCTLK model checking into the problem of model checking Probabilistic Branching Time Logic (PBTL), which enjoys path quantifiers in the range of adversaries. We then prove that model checking a formula of PCTLK in concurrent probabilistic programs is PSPACE-complete. Furthermore, we represent models associated with PCTLK logic symbolically with Multi-Terminal Binary Decision Diagrams (MTBDDs), which are supported by the probabilistic model checker PRISM. Finally, an application, namely the NetBill online shopping payment protocol, and an example about synchronization illustrated through the dining philosophers problem are implemented with the MTBDD engine of this model checker to verify probabilistic epistemic properties and evaluate the practical complexity of this verification.
References
[1]
Akers SB (1978) Binary decision diagrams. IEEE Trans Comput 100(6):509---516
[2]
Al-Saqqar F, Bentahar J, Sultan K, El-Menshawy M (2014) On the interaction between knowledge and social commitments in multi-agent systems. Appl Intell 41(1):235---259
[3]
Anciutti I (2009) A learning classifier system for emergent team behavior in real-time POMDP. In: 2009 IEEE international conference on intelligent computing and intelligent systems (ICIS 2009), vol 1. Piscataway, pp 733---738
[4]
Baier C, Katoen J-P (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]
Belardinelli F, Lomuscio A (2008) A complete first-order logics of knowledge and time. AAAI Press, pp 705---714
[7]
Bentahar J, El-Menshawy M, Qu H, Dssouli R (2012) Model checking communicative agent-based systems. Knowl-Based Syst 35:21---34
[8]
Bernholtz O, Vardi MY, Wolper P (1994) An automata-theoretic approach to branching-time model checking. In: Computer aided verification. Springer, pp 142---155
[9]
Bianco A, De Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Foundations of software technology and theoretical computer science. Springer, pp 499--- 513
[10]
Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117---148
[11]
Burch J, Clarke EM, Long D (1991) Symbolic model checking with partitioned transition relations. Computer Science Department, p 435
[12]
Campos S, Clarke EM, Minea M (1997) The verus tool: a quantitative approach to the formal verification of real-time systems. In: Computer aided verification. Springer, pp 452---455
[13]
Cao Z (2006) Model checking for epistemic and temporal properties of uncertain agents. Agent Computing and Multi-Agent Systems, pp 46---58
[14]
Cassandra AR, Kaelbling LP, Littman ML (1995) Acting optimally in partially observable stochastic domains. In: Proceedings of the national conference on artificial intelligence, vol 2. Cambridge, pp 1023---1023, 31,07-4,08
[15]
Chatterjee K, Sen K, Henzinger TA (2008) Model-checking ¿-regular properties of interval Markov chains. In: Foundations of software science and computational structures. Springer, pp 302---317
[16]
Ciesinski F, Baier C, Größer M, Parker D (2008) Generating compact MTBDD-representations from Probmela specifications. In: Model checking software. Springer, pp 60---76
[17]
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
[18]
Clarke EM, Grumberg O, Long DE (1994) Model checking and abstraction. ACM Trans Program Lang Syst (TOPLAS) 16(5):1512---1542
[19]
Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
[20]
Cohen M, Dam M, Lomuscio A, Qu H (2009) A symmetry reduction technique for model checking temporal-epistemic logic. In: IJCAI, vol 9, pp 721---726
[21]
de Alfaro L, Kwiatkowska M, Norman G, Parker D, Segala R (2000) Symbolic model checking of probabilistic processes using MTBDDs and the kronecker representation. In: 6th International conference on tools and algorithms for the construction and analysis of systems, TACAS 2000, volume 1785 LNCS. Springer, pp 395---410
[22]
Delgado C, Benevides M (2009) Verification of epistemic properties in probabilistic multi-agent systems. In: Proceeding of MATES 2009, volume 5774 LNAI, Hamburg, Germany, Sept. 9---11. Springer, pp 16---28
[23]
Dijkstra EW (1971) Hierarchical ordering of sequential processes. Acta Informatica 1(2):115---138
[24]
Durrett R (2010) Probability: theory and examples, 4th edn. Cambridge University Press, Cambridge
[25]
El Menshawy M, Bentahar J, El Kholy W, Dssouli R (2013) Reducing model checking commitments for agent communication to model checking ARCTL and GCTL*. Auton Agent Multi-Agent Syst 27(3):375---418
[26]
Elnaffar S, Maamar Z, Yahyaoui H, Bentahar J, Thiran P (2008) Reputation of communities of web services--preliminary investigation. In: 22nd International conference on advanced information networking and applications, AINA 2008, Workshops Proceedings, GinoWan, Okinawa, Japan, March 25---28, 2008. IEEE Computer Society, pp 1603---1608
[27]
Emerson EA, Clarke EM (1982) Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2(3):241---266
[28]
Fagin R, Halpern JY, Moses Y, Vardi MY (1995) Reasoning about knowledge. MIT Press, Cambridge
[29]
Finger M, Gabbay DM (1992) Adding a temporal dimension to a logic system. J Log Lang Inf 1(3):203---233
[30]
Fujita M, McGeer PC, Yang JC-Y (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst Des 10(2---3):149---169
[31]
Gammie P, Van der Meyden R (2004) Mck: model checking the logic of knowledge. In: Proceedings of the 16th international conference on computer aided verification, 13---17 July. Springer, Berlin, pp 479---483
[32]
Geffner H, Wainer J (1998) Modeling action, knowledge and control. In: Proceedings of European Conference on AI (ECAI-98), 23---28 Aug. Wiley, Chichester, pp 532---536
[33]
Gonsalves T, Itoh K (2011) GA optimization of Petri net-modeled concurrent service systems. Appl Soft Comput 11(5):3929---3937
[34]
Halpern JY (2003) Reasoning about uncertainty. MIT Press, Cambridge
[35]
Hansen H, Kwiatkowska MZ, Qu H (2011) Partial order reduction for model checking Markov decision processes under unconditional fairness. In: Eighth international conference on quantitative evaluation of systems, QEST 2011, 5---8 September, 2011. Aachen, Germany, pp 203---212
[36]
Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6 (5):512---535
[37]
Hartonas-Garmhausen V, Campos S, Clarke EM (1999) Probverus: probabilistic symbolic model checking. In: Formal methods for real-time and probabilistic systems. Springer, pp 96---110
[38]
Hérault T, Lassaigne R, Magniette F, Peyronnet S (2004) Approximate probabilistic model checking. In: Verification, model checking, and abstract interpretation. Springer, pp 73---84
[39]
Herd B, Miles S, McBurney P, Luck M (2013) Verification and validation of agent-based simulations using approximate model checking. In: Multi-agent-based simulation XIV, volume 8235 of Lecture Notes in Computer Science, pp 53---70
[40]
Huang X, Luo C, der Meyden RV (2011) Symbolic model checking of probabilistic knowledge. In: 13th conference on theoretical aspects of rationality and knowledge, TARK 2011, July 12---14, Groningen, pp 177---186
[41]
Huang X, Su K, Zhang C (2012) Probabilistic alternating-time temporal logic of incomplete information and synchronous perfect recall. In: Proceedings of the twenty-sixth AAAI conference on artificial intelligence, July 22---26, 2012, Toronto, pp 765---771
[42]
Jamroga W (2008) A temporal logic for Markov chains. In: Proceeding of 7th international conference on AAMAS, May 12---16. Padgham, Parkes, pp 697---704
[43]
Jebbaoui H, Mourad A, Otrok H, Haraty RA (2015) Semantics-based approach for detecting flaws, conflicts and redundancies in XACML policies. Comput Electr Eng 44:91---103
[44]
Kaelbling LP, Littman ML, Cassandra AR (1996) Partially observable Markov decision processes for artificial intelligence. In: Reasoning with uncertainty in robotics, 4---6 Dec. 1995. Springer, Berlin, pp 146---62
[45]
Kaplow R, Atrash A, Pineau J (2010) Variable resolution decomposition for robotic navigation under a POMDP framework. In: Proceedings - IEEE international conference on robotics and automation, pp 369---376
[46]
Konur S, Fisher M, Schewe S (2013) Combined model checking for temporal, probabilistic, and real-time logics. Theor Comput Sci 503:61---88
[47]
Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM (JACM) 47(2):312---360
[48]
Kwiatkowska M, Norman G, Pacheco A (2006) Model checking expected time and expected reward formulae with random time bounds. Comput Math Appl 51(2):305---316
[49]
Kwiatkowska M, Norman G, Parker D (2004) Probabilistic symbolic model checking with PRISM a hybrid approach. Int J Softw Tools Technol Transfer 6(2):128---142
[50]
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Proceedings of the 23rd international conference on computer aided verification (CAV'11), volume 6806 of LNCS. Springer, pp 585---591
[51]
Kwiatkowska M, Norman G, Parker D, Segala R (1999) Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex, Technical Report CSR-99-1, School of Computer Science, University of Birmingham
[52]
Lee C (1959) Representation of switching circuits by binary-decision programs. Bell Syst Tech J 38(4):985---999
[53]
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
[54]
Liu H, Zhang P, Hu B, Moore P (2015) A novel approach to task assignment in a cooperative multi-agent design system. Appl Intell 43(1):162---175
[55]
Lomuscio A, Qu H, Solanki M (2008) Towards verifying contract regulated service composition. In: IEEE international conference on web services ICWS, pp 254---261
[56]
Lomuscio A, Raimondi F (2006) The complexity of model checking concurrent programs against CTLK specifications. In: Declarative agent languages and technologies IV. Springer, pp 29---42
[57]
Lomuscio A, Raimondi F (2006) Mcmas: a model checker for multi-agent systems. In: Proceedings of the 12th international conference on tools and algorithms for the construction and analysis of systems. Berlin, Germany, 25 March-2 April 2006. Springer, pp 450---454
[58]
Meyer J-JC, van der Hoek W (1995) Epistemic logic for AI and computer science, vol 41. Cambridge University Press, Cambridge
[59]
Paquet S, Tobin L, Chaib-draa B (2005) Real-time decision making for large POMDPs. In: Lecture notes in computer science (including subseries lecture notes in artificial intelligence and lecture notes in bioinformatics), LNAI, vol 3501, pp 450--- 455
[60]
Parker D (2002) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham
[61]
Penczek W, Lomuscio A (2003) Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2):167---185, 05
[62]
Schnoebelen P (2002) The complexity of temporal logic model checking. Advances in Modal Logic 4:393---436
[63]
Shani G, Brafman R, Shimony S (2005) Model-based online learning of POMDPs. In: Machine learning ECML 2005, vol 3720. LNAI, Berlin, Germany, pp 353---364
[64]
Sheng QZ, Maamar Z, Yahyaoui H, Bentahar J, Boukadi K (2010) Separating operational and control behaviors: a new approach to web services modeling. IEEE Internet Comput 14(3):68--- 76
[65]
Sultan K, Bentahar J, El-Menshawy M (2014) Model checking probabilistic social commitments for intelligent agent communication. Appl Soft Comput 22:397---409
[66]
Taha T, Miro J, Dissanayake G (2011) A POMDP framework for modelling human interaction with assistive robots. In: IEEE international conference on robotics and automation, Piscataway, NJ, USA, pp 544---549
[67]
Tanenbaum AS (1992) Modern operating systems. Pearson Education
[68]
Tout H, Mourad A, Talhi C, Otrok H (2015) AOMD approach for context-adaptable and conflict-free web services composition. Comput Electr Eng 44:200---217
[69]
van der Meyden R, Shilov N (1999) Model checking knowledge and time in systems with perfect recall. In: Proceedings 19th conference on the foundations of software technology and theoretical computer science. Springer, pp 432---445
[70]
Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: IEEE Symposium on Foundations of Computer Science, pp 327---338
[71]
Wan W, Bentahar J, Ben Hamza A (2011) Model checking epistemic and probabilistic properties of multi-agent systems. In: Modern approaches in applied intelligence, vol 6704. LNAI, Syracuse, NY, United States, pp 68---78
[72]
Wan W, Bentahar J, Ben Hamza A (2013) Model checking epistemic-probabilistic logic using probabilistic interpreted systems. Knowl-Based Syst:279---295
[73]
Wang F, Kwiatkowska M (2005) An MTBDD-based implementation of forward reachability for probabilistic timed automata. In: Automated technology for verification and analysis. Springer, pp 385---399
[74]
Wooldridge MJ (2009) An introduction to multiagent systems, 2nd edn. Wiley, Chichester
[75]
Yousefian R, Rafe V, Rahmani M (2014) A heuristic solution for model checking graph transformation systems. Appl Soft Comput 24:169---180
[76]
Zhou C, Sun B, Liu Z (2010) Abstraction for model checking the probabilistic temporal logic of knowledge. In: Artificial intelligence and computational intelligence. Springer, pp 209---221
- Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications
Recommendations
Model checking epistemic-probabilistic logic using probabilistic interpreted systems
Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. ...
Temporalised Epistemic Logic for Reasoning about Agent-Based Systems
WI-IAT '09: Proceedings of the 2009 IEEE/WIC/ACM International Joint Conference on Web Intelligence and Intelligent Agent Technology - Volume 03For modelling and verifying agent systems, many researchers have proposed different logical systems. Since agent-based systems are designed to operate in dynamic environments such as the Internet, it is also important to model the temporal aspects of ...
Model checking probabilistic social commitments for intelligent agent communication
Interaction among autonomous agents in Multi-Agent Systems (MASs) is a key aspect for agents to coordinate with one another. Social approaches, as opposed to the mental approaches, have recently received a considerable attention in the area of agent ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2016 Springer Science+Business Media New York.
Publisher
Kluwer Academic Publishers
United States
Publication History
Published: 01 October 2016
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 26 Nov 2024
Other Metrics
Citations
Cited By
View all- Mccabe-Dansted JReynolds M(2017)To be fair, use bundlesAnnals of Mathematics and Artificial Intelligence10.1007/s10472-017-9546-x80:3-4(317-364)Online publication date: 1-Aug-2017
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in