Synthesizing Strategies for Epistemic Goals by Epistemic Model Checking: An Application to Pursuit Evasion Games

The paper identifies a special case in which the complex problem of synthesis from specifications in temporal-epistemic logic can be reduced to the simpler problem of model checking such specifications. An application is given of strategy synthesis in pursuit-evasion games, where one or more pursuers with incomplete information aim to discover theexistence of an evader. Experimental results are provided to evaluate the feasibility of the approach.

• Publication year

  2012

• Venue

  AAAI Conference on Artificial Intelligence

• Publication date

  2012-07-22

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1609/aaai.v26i1.8228
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model Checking

  2018cited by this paper
• Model Checking Knowledge in Pursuit Evasion Games

  2011cited by this paper
• GSST: anytime guaranteed search

  2010cited by this paper
• A graph search algorithm for indoor pursuit/evasion

  2009cited by this paper
• MCMAS: A Model Checker for the Verification of Multi-Agent Systems

  2009cited by this paper
• VerICS 2007 - a Model Checker for Knowledge and Real-Time

  2008cited by this paper
• Synthesis from Knowledge-Based Speci(cid:12)cations ?

  2007cited by this paper
• Model Checking Temporal Logics of Knowledge Via OBDDs

  2007cited by this paper
• Strong planning under partial observability

  2006influential reference
• A complete algorithm for visibility-based pursuit-evasion with limited field of view

  2004cited by this paper
• Strategic Planning through Model Checking of ATL Formulae

  2004cited by this paper
• Dynamic epistemic modelling

  2004cited by this paper
• Symbolic model checking the knowledge of the dining cryptographers

  2004cited by this paper
• MCK: Model Checking the Logic of Knowledge

  2004cited by this paper
• Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications

  2003cited by this paper
• Probabilistic pursuit-evasion games: theory, implementation, and experimental evaluation

  2002cited by this paper
• Tractable multiagent planning for epistemic goals

  2002cited by this paper
• Planning as Model Checking for Extended Goals in Non-deterministic Domains

  2001cited by this paper
• Real-Time Collision Avoidance: Differential Game, Numerical Solution, and Synthesis of Strategies

  2000cited by this paper
• Planning as Model Checking

  1999cited by this paper
• Synthesis from Knowledge-Based Specifications (Extended Abstract)

  1998cited by this paper
• Alternating-time temporal logic

  1997cited by this paper
• Reasoning about knowledge

  1995influential reference
• Graph-based Algorithm for Boolean Function Manipulation

  1989cited by this paper
• Differential Games. A Mathematical Theory with Applications to Warfare and Pursuit, Control and Optimization

  1966cited by this paper

• Dependable learning-enabled multiagent systems

  2022cites this paper
• An Overview of Verification and Validation Challenges for Inspection Robots

  2021cites this paper
• Knowledge-Based Strategies for Multi-Agent Teams Playing Against Nature

  2020cites this paper
• Multiagent Pursuit-Evasion Problem with the Pursuers Moving at Uncertain Speeds

  2018influential citation
• Pursuing a Faster Evader Based on an Agent Team with Unstable Speeds

  2017cites this paper
• Bounded model checking of strategy ability with perfect recall

  2015cites this paper
• A logic of probabilistic knowledge and strategy

  2013cites this paper
• Bounded planning for strategic goals with incomplete information and perfect recall

  2013cites this paper