Pareto-Rational Verification

TL;DR

This paper investigates the computational complexity of verifying systems interacting with rational environments modeled by Pareto-optimal behaviors, providing complexity results for various objectives and algorithms.

Contribution

It introduces the Pareto-rational verification problem, analyzes its complexity across different objectives, and proposes fixed-parameter tractable algorithms with empirical evaluation.

Findings

Pareto-rational verification is co-NP-complete for parity objectives.

Universal verification is in PSPACE and both NP-hard and co-NP-hard.

Verification problems are PSPACE-complete or 2EXPTIME-complete depending on objectives.

Abstract

We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regard to its set of objectives, given the behavior of the system (which is committed in advance of any interaction). We examine two ways of specifying this behavior, first by means of a deterministic Moore machine, and then by lifting its determinism. In the latter case the machine may embed several different behaviors for the system, and the universal rational verification problem aims at verifying that all of them are correct when the environment is rational. For parity objectives, we prove that the Pareto-rational verification problem is co-NP-complete and that its universal version is in PSPACE and both NP-hard and co-NP-hard. For Boolean B\"uchi objectives, the former problem is $\Pi_2\mathsf{P}$-complete and the latter is PSPACE-complete. We also study the case where the objectives are expressed using LTL formulas and show that the first problem is PSPACE-complete, and that the second is 2EXPTIME-complete. Both problems are also shown to be fixed-parameter tractable (FPT) for parity and Boolean B\"uchi objectives. Finally, we evaluate two variations of the FPT algorithm proposed to solve the Pareto-rational verification problem on a parametric toy example as well as on randomly generated instances.