Concurrent Games in Dynamic Epistemic Logic
Authors: Bastien Maubert, Sophie Pinchinat, Francois Schwarzentruber, Silvia Stranieri
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | Our first contribution is to define a DEL concurrent update product that provides the dynamics of concurrent epistemic actions. This new product yields a non-deterministic dynamics controlled by a scheduler, whose role is to resolve conflicts. On the basis of this product we show how finite DEL presentations can generate infinite concurrent game arenas. Our second contribution is a proof that distributed synthesis can be solved for such games for two cases: the case where all actions are public (perfectly observed by everyone), and the case where all actions have propositional pre- and post-conditions and information among the agents is hierarchical (Theorems 4 and 7). To prove this we extend to the concurrent setting some results from [Maubert et al., 2019; Maubert et al., 2020], namely, that the infinite concurrent game arenas arising from DEL game presentations can be finitely represented when actions are all public or all propositional. We then transfer existing results on the model-checking problem for the epistemic strategic logic ATL K [Van der Hoek and Wooldridge, 2003] to obtain, in particular, decidability of distributed synthesis for rich temporal epistemic objectives. |
| Researcher Affiliation | Academia | Bastien Maubert1 , Sophie Pinchinat2 , Franc ois Schwarzentruber2 and Silvia Stranieri1 1Universit à degli Studi di Napoli Federico II , Italy 2Universit e de Rennes, IRISA, CNRS, France |
| Pseudocode | No | The paper does not contain any pseudocode or clearly labeled algorithm blocks. |
| Open Source Code | No | The paper does not provide any statement or link indicating that open-source code for the methodology is available. |
| Open Datasets | No | This paper is theoretical and does not involve experimental evaluation on datasets, thus no training data is mentioned. |
| Dataset Splits | No | This paper is theoretical and does not involve experimental evaluation on datasets, thus no validation split information is provided. |
| Hardware Specification | No | This paper is theoretical and does not describe experimental procedures that would require specific hardware for execution. |
| Software Dependencies | No | This paper is theoretical and focuses on logical frameworks; therefore, it does not specify software dependencies with version numbers for experimental reproducibility. |
| Experiment Setup | No | This paper is theoretical and does not describe experiments with specific setup details or hyperparameters. |