Model Checking Against Arbitrary Public Announcement Logic: A First-Order-Logic Prover Approach for the Existential Fragment
作者： Tristan Charrier , Sophie Pinchinat , François Schwarzentruber
DOI: 10.1007/978-3-319-73579-5_9
关键词: Epistemic modal logic 、 Satisfiability 、 Reduction (recursion theory) 、 First-order logic 、 Group (mathematics) 、 Fragment (logic) 、 Model checking 、 Calculus 、 Gas meter prover 、 Computer science
摘要: In this paper, we investigate the model checking problem of symbolic models against epistemic logic with arbitrary public announcements and group announcements. We reduce to satisfiability Monadic Second Order Logic (MMSO), fragment monadic-second order restricted monadic predicates. particular, for case formulas in which all are existential, proposed reduction lands first-order logic. take advantage situation report on few experiments made provers.
springer.com
sci-hub.st 参考文章(42)
Konstantin Korovin, iProver --- An Instantiation-Based Theorem Prover for First-Order Logic (System Description) international joint conference on automated reasoning. pp. 292- 298 ,(2008) , 10.1007/978-3-540-71070-7_24
Hans P. van Ditmarsch, Tim French, Undecidability for arbitrary public announcement logic advances in modal logic. pp. 23- 42 ,(2008)
Hans van Ditmarsch, The Russian Cards Problem Studia Logica. ,vol. 75, pp. 31- 62 ,(2003) , 10.1023/A:1026168632319
Leopold L�wenheim, Über Möglichkeiten im Relativkalkül Mathematische Annalen. ,vol. 76, pp. 447- 470 ,(1915) , 10.1007/BF01458217
Rachid Alami, Mathieu Warnier, Séverin Lemaignan, Akin E. Sisbot, Human-Robot Interaction: Tackling the AI Challenges Artificial Intelligence. ,(2014)
Olivier Gasquet, Valentin Goranko, François Schwarzentruber, Big Brother Logic: visual-epistemic reasoning in stationary multi-agent systems Autonomous Agents and Multi-Agent Systems. ,vol. 30, pp. 793- 825 ,(2016) , 10.1007/S10458-015-9306-4
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
David S. JOHNSON, A catalog of complexity classes Handbook of theoretical computer science (vol. A). pp. 67- 161 ,(1991) , 10.1016/B978-0-444-88071-0.50007-2
Alexandru Baltag, Lawrence S. Moss, Sławomir Solecki, The logic of public announcements, common knowledge, and private suspicions theoretical aspects of rationality and knowledge. pp. 43- 56 ,(1998) , 10.1007/978-3-319-20451-2_38
Laura Bozzelli, Hans van Ditmarsch, Sophie Pinchinat, The Complexity of One-Agent Refinement Modal Logic Logics in Artificial Intelligence. ,vol. 7519, pp. 120- 133 ,(2012) , 10.1007/978-3-642-33353-8_10