论文标题
帕累托理性验证
Pareto-Rational Verification
论文作者
论文摘要
我们研究了合理验证问题，其中包括验证在假定合理行为的环境中执行系统的正确性。我们考虑了合理性的模型，在该模型中，由于系统的行为（在任何互动之前，在其行为之前），环境仅执行对其目标集的行为。我们首先通过确定性的摩尔机器，然后通过举起其确定性来研究两种指定这种行为的方法。在后一种情况下，机器可以为系统嵌入几种不同的行为，并且通用有理验证问题旨在验证当环境是理性时它们都是正确的。对于奇偶校的目标，我们证明了帕累托理性的验证问题是共同完成的，并且其通用版本在pspace中，np-hard和co-np-hard。对于布尔·布尔奇（BuleanBüchi）目标，前一个问题是$π_2\ mathsf {p} $ - 完整，后者是pspace-complete。我们还研究了使用LTL公式表达目标的情况，并表明第一个问题是Pspace complete，而第二个问题是2Exptime-Complete。这两个问题也表明是固定参数可用于奇偶校验的固定参数（FPT）和布尔·布尔奇目标。最后，我们评估了提出的两种FPT算法的变体，以在参数玩具示例以及随机生成的实例上解决帕累托理性验证问题。
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üchi objectives, the former problem is $Π_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üchi 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.
