A Three-valued Approach to Strategic Abilities under Imperfect Information

Francesco Belardinelli (1) , Vadim Malvone (2)

1 Imperial College London
2 IBISC - Informatique, BioInformatique, Systèmes Complexes

A major challenge for logics for strategies is represented by their verification in contexts of imperfect information. In this contribution we advance the state of the art by approximating the verification of Alternating-time Temporal Logic (AT L) under imperfect information by using perfect information and a three-valued semantics. In particular, we develop novel automata-theoretic techniques for the linear-time logic LT L, then apply these to finding “failure” states, where the AT L specification to be model checked is undefined. Such failure states can then be fed into a refinement procedure, thus providing a sound, albeit partial, verification procedure.

Keywords: Geometric; spatial; and temporal reasoning

Domains: Logic in Computer Science [cs.LO]

Francesco Belardinelli, Vadim Malvone. A Three-valued Approach to Strategic Abilities under Imperfect Information. 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), Sep 2020, Rhodes, Greece. ⟨hal-03170197⟩