DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2022.33

Pareto-Rational Verification

Authors: Véronique Bruyère, Jean-François Raskin, and Clément Tamines

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

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üchi objectives, the former problem is Π₂𝖯-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 for parity and Boolean Büchi objectives.

Cite as

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-Rational Verification. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2022.33,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
  title =	{{Pareto-Rational Verification}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.33},
  URN =		{urn:nbn:de:0030-drops-170968},
  doi =		{10.4230/LIPIcs.CONCUR.2022.33},
  annote =	{Keywords: Rational verification, Model-checking, Pareto-optimality, \omega-regular objectives}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.27

Stackelberg-Pareto Synthesis

Authors: Véronique Bruyère, Jean-François Raskin, and Clément Tamines

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

In this paper, we study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. For games in which objectives are either all parity or all reachability objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. This problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.

Cite as

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto Synthesis. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2021.27,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
  title =	{{Stackelberg-Pareto Synthesis}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.27},
  URN =		{urn:nbn:de:0030-drops-144040},
  doi =		{10.4230/LIPIcs.CONCUR.2021.27},
  annote =	{Keywords: Stackelberg non-zero sum games played on graphs, synthesis, parity objectives}
}

Search Results

Documents authored by Tamines, Clément

Pareto-Rational Verification

Abstract

Cite as

Stackelberg-Pareto Synthesis

Abstract

Cite as

Thanks for your feedback!

Could not send message