Bounded model checking of strategy ability with perfect recall
作者： Xiaowei Huang
DOI: 10.1016/J.ARTINT.2015.01.005
关键词:
摘要: The paper works with a logic which has the expressiveness to quantify over strategies of bounded length. semantics is based on systems multiple agents. Agents have incomplete information about underlying system state and their are perfect recall memory observations local actions. computational complexity model checking shown be PSPACE-complete. We give two BDD-based algorithms. algorithms implemented in checker experimental results reported show applications.
bcu.ac.uk
elsevier.com
core.ac.uk 
sci-hub.se 参考文章(43)
Ron van der Meyden, Xiaowei Huang, An Epistemic Strategy Logic arXiv: Logic in Computer Science. ,(2014)
Chenyi Zhang, Xiaowei Huang, Kaile Su, Probabilistic alternating-time temporal logic of incomplete information and synchronous perfect recall national conference on artificial intelligence. ,vol. 1, pp. 765- 771 ,(2012)
W.J. Jamroga, Some Remarks on Alternating Temporal Epistemic Logic Formal Approaches to Multi-Agent Systems (FAMAS 2003). pp. 133- 139 ,(2003)
Xiaowei Huang, Ron van der Meyden, Symbolic Synthesis for Epistemic Specifications with Observational Semantics Tools and Algorithms for the Construction and Analysis of Systems. pp. 455- 469 ,(2014) , 10.1007/978-3-642-54862-8_39
Ron Van Der Meyden, Xiaowei Huang, Synthesizing strategies for epistemic goals by epistemic model checking: an application to pursuit evasion games national conference on artificial intelligence. pp. 772- 778 ,(2012)
Peter Gammie, Ron van der Meyden, MCK: Model Checking the Logic of Knowledge Computer Aided Verification. ,vol. 3114, pp. 479- 483 ,(2004) , 10.1007/978-3-540-27813-9_41
Fausto Giunchiglia, Paolo Traverso, Planning as Model Checking Lecture Notes in Computer Science. pp. 1- 20 ,(1999) , 10.1007/10720246_1
Ron Van Der Meyden, Xiaowei Huang, Patrick Maupin, Model checking knowledge in pursuit evasion games international joint conference on artificial intelligence. pp. 240- 245 ,(2011) , 10.5591/978-1-57735-516-8/IJCAI11-051
Wojciech Jamroga, Strategic Planning through Model Checking of ATL Formulae international conference on artificial intelligence and soft computing. pp. 879- 884 ,(2004) , 10.1007/978-3-540-24844-6_136
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu, Bounded Model Checking Advances in Computers. ,vol. 58, pp. 117- 148 ,(2003) , 10.1016/S0065-2458(03)58003-2