A Computationally Grounded Logic of 'Seeing-to-it-that'

A Computationally Grounded Logic of 'Seeing-to-it-that'

Andreas Herzig, Emiliano Lorini, Elise Perrotin

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 2648-2654. https://doi.org/10.24963/ijcai.2022/367

We introduce a simple model of agency that is based on the concepts of control and attempt. Both relate agents and propositional variables. Moreover, they can be nested: an agent i may control whether another agent j controls a propositional variable p; i may control whether j attempts to change p; i may attempt to change whether j controls p; i may attempt to change whether j attempts to change p; and so on. In this framework we define several modal operators of time and agency: the LTL operators on the one hand, and the Chellas and the deliberative stit operator on the other. While in the standard stit framework the model checking problem is unfeasible because its models are infinite, in our framework models are represented in a finite and compact way: they are grounded on the primitive concepts of control and attempt. This makes model checking practically feasible. We prove its PSPACE-completeness and we show how the concept of social influence can be captured.
Keywords:
Knowledge Representation and Reasoning: Knowledge Representation Languages
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
Knowledge Representation and Reasoning: Reasoning about actions