Probabilistic Strategy Logic with Degrees of Observability
Authors: Chunyan Mu, Nima Motamed, Natasha Alechina, Brian Logan
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we present a formal framework for reasoning about information transparency properties in stochastic multi-agent systems. We extend Probabilistic Strategy Logic with new observability operators that capture the degree of observability of temporal properties by agents. We show that the model checking problem for the resulting logic is decidable. ... Showing that the model-checking problem for o PSL with memoryless strategies is decidable in 3EXPSPACE. |
| Researcher Affiliation | Academia | 1Department of Computing Science, University of Aberdeen 2Department of Information and Computing Sciences, Utrecht University 3Department of Computer Science, Open University Netherlands EMAIL, EMAIL, EMAIL, EMAIL |
| Pseudocode | No | The detailed definitions of a kΦ,s are omitted here due to lack of space and can be found in (Mu et al. 2024). ... Again, due to space constraints, the detailed construction of EqnobsiΦ,s can be found in (Mu et al. 2024). The paper describes algorithmic approaches but does not present them in a structured pseudocode or algorithm block within this document. |
| Open Source Code | No | The paper does not contain any explicit statements about releasing source code, nor does it provide links to repositories or mention code in supplementary materials. |
| Open Datasets | No | The paper describes a formal framework and theoretical model checking. It uses "Example 1. Consider the simple message interception scenario illustrated in Figure 1." as an illustrative example, but no actual datasets are used or made available. |
| Dataset Splits | No | The paper is theoretical and does not use any datasets, thus there is no information on dataset splits. |
| Hardware Specification | No | The paper describes a theoretical framework and model checking problem; it does not conduct experiments and therefore does not specify hardware. |
| Software Dependencies | No | The paper focuses on theoretical logic and model checking; it does not mention specific software dependencies or version numbers used for implementation or experiments. |
| Experiment Setup | No | The paper is theoretical and focuses on a formal framework and decidability of model checking, thus it does not include experimental setup details or hyperparameters. |