Exploring the KD45 n property of a kripke model after the execution of an action sequence
Tran Cao Son, Enrico Pontelli, Chitta R. Baral, Gregory Gelfond · 2015
The paper proposes a condition for preserving the KD45n property of a Kripke model when a sequence of update mod-els is applied to it. The paper defines the notions of a primitive update model and a semi-reflexive KD45n (or sr-KD45n) Kripke model. It proves that updating a sr-KD45n Kripke model using a primitive update model results in a sr-KD45n Kripke model, i.e., a primitive update model preserves the properties of a sr-KD45n Kripke model. It shows that sev-eral update models for modeling well-known actions found in the literature are primitive. This result provides guaran-tees that can be useful in presence of multiple applications of actions in multi-agent system (e.g., multi-agent planning). Introduction and Motivations In a multi-agent action setting, agents need to not just