Exploring the KD45 Property of a Kripke Model After the Execution of an Action Sequence
Abstract
The paper proposes a condition for preserving the KD45 property of a Kripke model when a sequence of update models is applied to it. The paper defines the notions of a primitive update model and a semi-reflexive KD45 (or sr-KD45) Kripke model. It proves that updating a sr-KD45 Kripke model using a primitive update model results in a sr-KD45 Kripke model, i.e., a primitive update model preserves the properties of a sr-KD45 Kripke model. It shows that several update models for modeling well-known actions found in the literature are primitive. This result provides guarantees that can be useful in presence of multiple applications of actions in multi-agent system (e.g., multi-agent planning).
Cite
Text
Son et al. "Exploring the KD45 Property of a Kripke Model After the Execution of an Action Sequence." AAAI Conference on Artificial Intelligence, 2015. doi:10.1609/AAAI.V29I1.9401Markdown
[Son et al. "Exploring the KD45 Property of a Kripke Model After the Execution of an Action Sequence." AAAI Conference on Artificial Intelligence, 2015.](https://mlanthology.org/aaai/2015/son2015aaai-exploring/) doi:10.1609/AAAI.V29I1.9401BibTeX
@inproceedings{son2015aaai-exploring,
title = {{Exploring the KD45 Property of a Kripke Model After the Execution of an Action Sequence}},
author = {Son, Tran Cao and Pontelli, Enrico and Baral, Chitta and Gelfond, Gregory},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2015},
pages = {1604-1610},
doi = {10.1609/AAAI.V29I1.9401},
url = {https://mlanthology.org/aaai/2015/son2015aaai-exploring/}
}