Search Results

Documents authored by Pinchinat, Sophie


Document
Plan Logic

Authors: Dylan Bellier, Massimo Benerecetti, Fabio Mogavero, and Sophie Pinchinat

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)


Abstract
When reasoning about games, one is often interested in verifying more intricate strategic properties than the mere existence of a winning strategy for a given coalition. Several languages, among which the very expressive Strategy Logic (SL), have been proposed that explicitly quantify over strategies in order to express and verify such properties. However, quantifying over strategies poses serious issues: not only does this lead to a non-elementary model-checking problem, but the classic Tarskian semantics is not fully adequate, both from a conceptual and practical viewpoint, since it does not guarantee the realisability of the strategies involved. In this paper, we follow a different approach and introduce Plan Logic (PL), a logic that takes plans, i.e., sequences of actions, as first-class citizens instead of strategies. Since plans are much simpler objects than strategies, it becomes easier to enforce realisability. In this setting, we can recover strategic reasoning by means of a compositional hyperteams semantics, inspired by the well-known team semantics. We show that the Conjunctive-Goal and Disjunctive-Goal fragments of SL are captured by PL, with an effective polynomial translation. This result relies on the definition of a suitable game-theoretic semantics for the two fragments. We also investigate the model-checking problem for PL. For the full prenex fragment, the problem is shown to be fixed-parameter-tractable: it is polynomial in the size of the model, when the formula is fixed, and 2-ExpTimeC in the size of the formula. For the Conjunctive-Goal and Disjunctive-Goal fragments of PL this result can be improved to match the optimal polynomial complexity in the size of the model, regardless of the size of the formula.

Cite as

Dylan Bellier, Massimo Benerecetti, Fabio Mogavero, and Sophie Pinchinat. Plan Logic. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{bellier_et_al:LIPIcs.FSTTCS.2024.9,
  author =	{Bellier, Dylan and Benerecetti, Massimo and Mogavero, Fabio and Pinchinat, Sophie},
  title =	{{Plan Logic}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.9},
  URN =		{urn:nbn:de:0030-drops-221988},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.9},
  annote =	{Keywords: Logic for strategic reasoning, Strategy Logic, Realisable strategies, Strategies vs. plans, Hyperteam semantics}
}
Document
Invited Talk
Strategic Reasoning Under Imperfect Information with Synchronous Semantics (Invited Talk)

Authors: Sophie Pinchinat

Published in: LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024)


Abstract
Dynamic Epistemic Logic is a modal logic dedicated to specifying epistemic property changes along the dynamic behavior of a multi-agent system. The models that underlie this logic are (epistemic) states together with transitions caused by events, the occurrence of which may modify the current state. We first develop a setting where the entire dynamics of the system starting from an initial state is captured by a single infinite tree, in a way similar to what has been considered for Epistemic Temporal Logic, and second go through the current state-of-the-art regarding strategic reasoning, with a focus on planning problems in this infinite structure.

Cite as

Sophie Pinchinat. Strategic Reasoning Under Imperfect Information with Synchronous Semantics (Invited Talk). In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{pinchinat:LIPIcs.TIME.2024.2,
  author =	{Pinchinat, Sophie},
  title =	{{Strategic Reasoning Under Imperfect Information with Synchronous Semantics}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-349-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{318},
  editor =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.2},
  URN =		{urn:nbn:de:0030-drops-212093},
  doi =		{10.4230/LIPIcs.TIME.2024.2},
  annote =	{Keywords: Strategic reasoning, Imperfect information, chain-MSO, Automatic structures}
}
Document
Dependency Matrices for Multiplayer Strategic Dependencies

Authors: Dylan Bellier, Sophie Pinchinat, and François Schwarzentruber

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)


Abstract
In multi-player games, players take their decisions on the basis of their knowledge about what other players have done, or currently do, or even, in some cases, will do. An ability to reason in games with temporal dependencies between players' decisions is a challenging topic, in particular because it involves imperfect information. In this work, we propose a theoretical framework based on dependency matrices that includes many instances of strategic dependencies in multi-player imperfect information games. For our framework to be well-defined, we get inspiration from quantified linear-time logic where each player has to label the timeline with truth values of the propositional variable she owns. We study the problem of the existence of a winning strategy for a coalition of players, show it is undecidable in general, and exhibit an interesting subclass of dependency matrices that makes the problem decidable: the class of perfect-information dependency matrices.

Cite as

Dylan Bellier, Sophie Pinchinat, and François Schwarzentruber. Dependency Matrices for Multiplayer Strategic Dependencies. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bellier_et_al:LIPIcs.FSTTCS.2022.31,
  author =	{Bellier, Dylan and Pinchinat, Sophie and Schwarzentruber, Fran\c{c}ois},
  title =	{{Dependency Matrices for Multiplayer Strategic Dependencies}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{31:1--31:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.31},
  URN =		{urn:nbn:de:0030-drops-174230},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.31},
  annote =	{Keywords: Temporal dependency, Delay games, Strategic reasoning, Temporal logic}
}
Document
Complete Volume
LIPIcs, Volume 147, TIME'19, Complete Volume

Authors: Johann Gamper, Sophie Pinchinat, and Guido Sciavicco

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)


Abstract
LIPIcs, Volume 147, TIME'19, Complete Volume

Cite as

26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Proceedings{gamper_et_al:LIPIcs.TIME.2019,
  title =	{{LIPIcs, Volume 147, TIME'19, Complete Volume}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019},
  URN =		{urn:nbn:de:0030-drops-113887},
  doi =		{10.4230/LIPIcs.TIME.2019},
  annote =	{Keywords: Theory of computation, Logic; Information systems, Temporal data; Computing methodologies, Knowledge representation and reasoning}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Johann Gamper, Sophie Pinchinat, and Guido Sciavicco

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gamper_et_al:LIPIcs.TIME.2019.0,
  author =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.0},
  URN =		{urn:nbn:de:0030-drops-113582},
  doi =		{10.4230/LIPIcs.TIME.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Jumping Automata for Uniform Strategies

Authors: Bastien Maubert and Sophie Pinchinat

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)


Abstract
The concept of uniform strategies has recently been proposed as a relevant notion in game theory for computer science. It relies on properties involving sets of plays in two-player turn-based arenas equipped with a binary relation between plays. Among the two notions of fully-uniform and strictly-uniform strategies, we focus on the latter, less explored. We present a language that extends CTL^* with a quantifier over all related plays, which enables to express a rich class of uniformity constraints on strategies. We show that the existence of a uniform strategy is equivalent to the language non-emptiness of a jumping tree automaton. While the existence of a uniform strategy is undecidable for rational binary relations, restricting to ecognizable relations yields a 2EXPTIME-complete complexity, and still captures a class of two-player imperfect-information games with epistemic temporal objectives. This result relies on a translation from jumping tree automata with recognizable relations to two-way tree automata.

Cite as

Bastien Maubert and Sophie Pinchinat. Jumping Automata for Uniform Strategies. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 287-298, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@InProceedings{maubert_et_al:LIPIcs.FSTTCS.2013.287,
  author =	{Maubert, Bastien and Pinchinat, Sophie},
  title =	{{Jumping Automata for Uniform Strategies}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{287--298},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.287},
  URN =		{urn:nbn:de:0030-drops-43801},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.287},
  annote =	{Keywords: Games, Imperfect information, Uniform strategies, Jumping automata}
}
Document
Emptiness Of Alternating Tree Automata Using Games With Imperfect Information

Authors: Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)


Abstract
We consider the emptiness problem for alternating tree automata, with two acceptance semantics: classical (all branches are accepted) and qualitative (almost all branches are accepted). For the classical semantics, the usual technique to tackle this problem relies on a Simulation Theorem which constructs an equivalent non-deterministic automaton from the original alternating one, and then checks emptiness by a reduction to a two-player perfect information game. However, for the qualitative semantics, no simulation of alternation by means of non-determinism is known. We give an alternative technique to decide the emptiness problem of alternating tree automata, that does not rely on a Simulation Theorem. Indeed, we directly reduce the emptiness problem to solving an imperfect information two-player parity game. Our new approach can successfully be applied to both semantics, and yields decidability results with optimal complexity; for the qualitative semantics, the key ingredient in the proof is a positionality result for stochastic games played over infinite graphs.

Cite as

Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre. Emptiness Of Alternating Tree Automata Using Games With Imperfect Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 299-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.FSTTCS.2013.299,
  author =	{Fijalkow, Nathana\"{e}l and Pinchinat, Sophie and Serre, Olivier},
  title =	{{Emptiness Of Alternating Tree Automata Using Games With Imperfect Information}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{299--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.299},
  URN =		{urn:nbn:de:0030-drops-43812},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.299},
  annote =	{Keywords: Alternating Automata, Emptiness checking, Two-player games, Imperfect Information Games}
}
Document
VaToMAS - Verification and Testing of Multi-Agent Systems (Dagstuhl Seminar 13181)

Authors: Alessio R. Lomuscio, Sophie Pinchinat, and Holger Schlingloff

Published in: Dagstuhl Reports, Volume 3, Issue 4 (2013)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13181 ``VaToMAS - Verification and Testing of Multi-Agent Systems''.

Cite as

Alessio R. Lomuscio, Sophie Pinchinat, and Holger Schlingloff. VaToMAS - Verification and Testing of Multi-Agent Systems (Dagstuhl Seminar 13181). In Dagstuhl Reports, Volume 3, Issue 4, pp. 151-187, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@Article{lomuscio_et_al:DagRep.3.4.151,
  author =	{Lomuscio, Alessio R. and Pinchinat, Sophie and Schlingloff, Holger},
  title =	{{VaToMAS - Verification and Testing of Multi-Agent Systems (Dagstuhl Seminar 13181)}},
  pages =	{151--187},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{4},
  editor =	{Lomuscio, Alessio R. and Pinchinat, Sophie and Schlingloff, Holger},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.4.151},
  URN =		{urn:nbn:de:0030-drops-41746},
  doi =		{10.4230/DagRep.3.4.151},
  annote =	{Keywords: Model checking, Specification-based testing, Multi-agent systems, Controller synthesis, Temporal logic}
}
Document
On Timed Alternating Simulation for Concurrent Timed Games

Authors: Laura Bozzelli, Axel Legay, and Sophie Pinchinat

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)


Abstract
We address the problem of alternating simulation refinement for concurrent timed games (\TG). We show that checking timed alternating simulation between\TG is \EXPTIME-complete, and provide a logical characterization of thispreorder in terms of a meaningful fragment of a new logic, \TAMTLSTAR.\TAMTLSTAR is an action-based timed extension of standard alternating-timetemporal logic \ATLSTAR, which allows to quantify on strategies where thedesignated player is not responsible for blocking time. While for full \TAMTLSTAR, model-checking \TG is undecidable, we show that for its fragment \TAMTL, corresponding to the timed version of \ATL, in \EXPTIME.

Cite as

Laura Bozzelli, Axel Legay, and Sophie Pinchinat. On Timed Alternating Simulation for Concurrent Timed Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 85-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.FSTTCS.2009.2309,
  author =	{Bozzelli, Laura and Legay, Axel and Pinchinat, Sophie},
  title =	{{On Timed Alternating Simulation for Concurrent Timed Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{85--96},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2309},
  URN =		{urn:nbn:de:0030-drops-23092},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2309},
  annote =	{Keywords: Concurrent Timed Games, Timed Alternating Simulation, Timed Alternating Temporal Logics}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail