François Schwarzentruber

Tutorial on 22/6/15, 13h30: Decision problems in Dynamic epistemic logic

We first present Dynamic epistemic logic which is a framework for reasoning about epistemic actions in a multi-agent systems [van Ditmarsch, 2007]. For instance, such actions could be "agent A shows its card to agent B, agent C notices that agent A has shown his own card while agent D does not notice it". In a first part, we show how to model epistemic situations (with Kripke epistemic models) and how to model actions with action models. In a second part, we discuss the model checking problem and the epistemic planning problem. In particular, we give complexity results/decidability results depending on restrictions on the specification and also how the specification is encoded.

Bibliography

Charrier et al. Arbitrary public announcement logic with mental programs. AAMAS 2015.

Bolander, Jensen, et al. Complexity results in Epistemic Planning. IJCAI 2015

Ma, Katsuhiko Sano et al. Tableaux for Non-normal Public Announcement Logic. ICLA 2015.

van Ditmarsch, H., Herzig, Lorini et al. Listen to Me! Public Announcements to Agents That Pay Attention - or Not. LORI 2013.

Aucher et al. On the Complexity of Dynamic Epistemic Logic, TARK 2013.

Aucher, Bolander. Undecidability in Epistemic Planning IJCAI 2013.

Balbiani, Gasquet et al. Agents that look at one another. Journal of IGPL. 2013

van Ditmarsch, H., van der Hoek, W., & Kooi, B. P. (Eds.). (2007). Dynamic epistemic logic (Vol. 337). Springer.

Talk on 23/6/15, 13h30:  Arbitrary Public Announcement Logic with Mental Programs

We propose a variant of arbitrary public announcement logic which is
decidable. In this variant, knowledge accessibility relations are
defined by programs. Technically, programs are written in dynamic
logic with propositional assignments. We prove that both the model
checking problem and the satisfiability problem are decidable and
AEXPpol-complete where AEXPpol is the class of decision problems
decided by alternating Turing machines running in exponential time
where the number of alternations is polynomial. Whereas arbitrary
public announcement logic is undecidable, our framework is decidable
and we provide a proof-of-concept to show its expressiveness: we use
our framework to reason about epistemic properties and arbitrary
announcements when agents are cameras located in the plane.

cimi_toulouse222june_tutorial_del_complexity_francois_schwarzentruber.pdf

cimi_toulouse_23june_arbitrarypal_mental_programs_francois_schwarzentruber.pdf