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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
