Partial Order Reductions for model checking temporal epistemic logic over interleaved mulit-agent systems

Abstract : We investigate partial order reduction for model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model chechking step and show preservation properties. We evaluate the technique by discussing the experimental results obtained against well-known examples in the MAS literature
Type de document :
Communication dans un congrès
AAMAS 2010 : International Conference on Autonomous Agents and Multiagent Systems, May 2010, Toronto, Canada. 2010
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00458132
Contributeur : Brigitte Briot <>
Soumis le : vendredi 19 février 2010 - 13:51:01
Dernière modification le : vendredi 26 février 2010 - 13:52:21
Document(s) archivé(s) le : vendredi 18 juin 2010 - 18:33:46

Fichier

aamas.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00458132, version 1

Collections

Citation

Alessio Lomuscio, Wojciech Penczek, Hongyang Qu. Partial Order Reductions for model checking temporal epistemic logic over interleaved mulit-agent systems. AAMAS 2010 : International Conference on Autonomous Agents and Multiagent Systems, May 2010, Toronto, Canada. 2010. 〈inria-00458132〉

Partager

Métriques

Consultations de la notice

63

Téléchargements de fichiers

77