On Verifying Expectations and Observations of Intelligent Agents

Authors: Sourav Chakraborty, Avijeet Ghosh, Sujata Ghosh, François Schwarzentruber

IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical In this work, we investigate the computational complexity of the model checking problem for POL and prove its PSPACE-completeness. We also study various syntactic fragments of POL. We exemplify the applicability of POL model checking in verifying different characteristics and features of an interactive system with respect to the distinct expectations and (matching) observations of the system. Finally, we provide a discussion on the implementation of the model checking algorithms.
Researcher Affiliation Academia 1Indian Statistical Institute, Kolkata 2Indian Statistical Institute, Chennai 3Univ Rennes, IRISA, France
Pseudocode Yes Algorithm 1 mc POL Input: M = S, , V, Exp , s S, φ Output: True iff M, s φ
Open Source Code Yes (for details, see [Chakraborty et al., 2022]and https://github.com/francoisschwarzentruber/polmc).
Open Datasets No The paper uses illustrative examples (e.g., traffic light, message passing, farming drone) but does not use or refer to any publicly available datasets for empirical training.
Dataset Splits No No empirical experiments are conducted on datasets; therefore, there is no discussion of training, validation, or test splits.
Hardware Specification No The paper discusses algorithms and complexity but does not provide any specific details about the hardware used for computation or experiments.
Software Dependencies No The paper discusses implementation strategies but does not list any specific software dependencies with version numbers.
Experiment Setup No As a theoretical paper focusing on complexity and algorithms, there are no experimental setup details like hyperparameters or training configurations provided.