6 Search Results for "St�phan, Igor"

Document
DOI: 10.4230/LIPIcs.CONCUR.2020.24
Games Where You Can Play Optimally with Arena-Independent Finite Memory

Authors: Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka [Hugo Gimbert and Wieslaw Zielonka, 2005] provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory - finite or infinite - is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).
Cite as

Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games Where You Can Play Optimally with Arena-Independent Finite Memory. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2020.24,
  author =	{Bouyer, Patricia and Le Roux, St\'{e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Games Where You Can Play Optimally with Arena-Independent Finite Memory}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{24:1--24:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.24},
  URN =		{urn:nbn:de:0030-drops-128360},
  doi =		{10.4230/LIPIcs.CONCUR.2020.24},
  annote =	{Keywords: two-player games on graphs, finite-memory determinacy, optimal strategies}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.19
Resolution with Counting: Dag-Like Lower Bounds and Different Moduli

Authors: Fedor Part and Iddo Tzameret

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin_R), this refutation system operates with disjunctions of linear equations with boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of [Ran Raz and Iddo Tzameret, 2008], through the work of [Dmitry Itsykson and Dmitry Sokolov, 2014] which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. [Jan Krajícek, 2017; Dmitry Itsykson and Dmitry Sokolov, 2014; Jan Krajícek and Igor Carboni Oliveira, 2018; Michal Garlik and Lezsek Kołodziejczyk, 2018]) made it evident that establishing lower bounds against general Res(lin_R) refutations is a challenging and interesting task since the system captures a "minimal" extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds on general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subset-sum principle 1+ x_1 + ̇s +2^n x_n = 0 requires refutations of exponential-size over ℚ. Our proof technique is nontrivial and novel: roughly speaking, we show that under certain conditions every refutation of a subset-sum instance f=0, where f is a linear polynomial over ℚ, must pass through a fat clause containing an equation f=α for each α in the image of f under boolean assignments. We develop a somewhat different approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. We then turn to the finite fields regime, showing that the work of Itsykson and Sokolov [Dmitry Itsykson and Dmitry Sokolov, 2014] who obtained tree-like lower bounds over ?_2 can be carried over and extended to every finite field. We establish new lower bounds and separations as follows: (i) for every pair of distinct primes p,q, there exist CNF formulas with short tree-like refutations in Res(lin_{?_p}) that require exponential-size tree-like Res(lin_{?_q}) refutations; (ii) random k-CNF formulas require exponential-size tree-like Res(lin_{?_p}) refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like Res(lin_?) refutations of the pigeonhole principle, for every field ?.
Cite as

Fedor Part and Iddo Tzameret. Resolution with Counting: Dag-Like Lower Bounds and Different Moduli. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 19:1-19:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{part_et_al:LIPIcs.ITCS.2020.19,
  author =	{Part, Fedor and Tzameret, Iddo},
  title =	{{Resolution with Counting: Dag-Like Lower Bounds and Different Moduli}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{19:1--19:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.19},
  URN =		{urn:nbn:de:0030-drops-117041},
  doi =		{10.4230/LIPIcs.ITCS.2020.19},
  annote =	{Keywords: Proof complexity, concrete lower bounds, resolution, satisfiability, combinatorics}
}
Document
DOI: 10.4230/OASIcs.ICLP.2018.4
A New Proof-Theoretical Linear Semantics for CHR

Authors: Igor Stéphan

Published in: OASIcs, Volume 64, Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)

Abstract
Constraint handling rules are a committed-choice language consisting of multiple-heads guarded rules that rewrite constraints into simpler ones until they are solved. We propose a new proof-theoretical declarative linear semantics for Constraint Handling Rules. We demonstrate completeness and soundness of our semantics w.r.t. operational omega_t. semantics. We propose also a translation from this semantics to linear logic.
Cite as

Igor Stéphan. A New Proof-Theoretical Linear Semantics for CHR. In Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). Open Access Series in Informatics (OASIcs), Volume 64, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{stephan:OASIcs.ICLP.2018.4,
  author =	{St\'{e}phan, Igor},
  title =	{{A New Proof-Theoretical Linear Semantics for CHR}},
  booktitle =	{Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)},
  pages =	{4:1--4:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-090-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{64},
  editor =	{Dal Palu', Alessandro and Tarau, Paul and Saeedloei, Neda and Fodor, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.4},
  URN =		{urn:nbn:de:0030-drops-98707},
  doi =		{10.4230/OASIcs.ICLP.2018.4},
  annote =	{Keywords: Constraint Handling Rules, Linear Logic}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.40
Concurrent Games and Semi-Random Determinacy

Authors: Stéphane Le Roux

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
Consider concurrent, infinite duration, two-player win/lose games played on graphs. If the winning condition satisfies some simple requirement, the existence of Player 1 winning (finite-memory) strategies is equivalent to the existence of winning (finite-memory) strategies in finitely many derived one-player games. Several classical winning conditions satisfy this simple requirement. Under an additional requirement on the winning condition, the non-existence of Player 1 winning strategies from all vertices is equivalent to the existence of Player 2 stochastic strategies almost-sure winning from all vertices. Only few classical winning conditions satisfy this additional requirement, but a fairness variant of omega-regular languages does.
Cite as

Stéphane Le Roux. Concurrent Games and Semi-Random Determinacy. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.MFCS.2018.40,
  author =	{Le Roux, St\'{e}phane},
  title =	{{Concurrent Games and Semi-Random Determinacy}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.40},
  URN =		{urn:nbn:de:0030-drops-96220},
  doi =		{10.4230/LIPIcs.MFCS.2018.40},
  annote =	{Keywords: Two-player win/lose, graph, infinite duration, abstract winning condition}
}
Document
DOI: 10.4230/OASIcs.ICLP.2016.6
Justifications and Blocking Sets in a Rule-Based Answer Set Computation

Authors: Christopher Béatrix, Claire Lefèvre, Laurent Garcia, and Igor Stéphan

Published in: OASIcs, Volume 52, Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)

Abstract
Notions of justifications for logic programs under answer set semantics have been recently studied for atom-based approaches or argumentation approaches. The paper addresses the question in a rule-based answer set computation: the search algorithm does not guess on the truth or falsity of an atom but on the application or non application of a non monotonic rule. In this view, justifications are sets of ground rules with particular properties. Properties of these justifications are established; in particular the notion of blocking set (a reason incompatible with an answer set) is defined, that permits to explain computation failures. Backjumping, learning, debugging and explanations are possible applications.
Cite as

Christopher Béatrix, Claire Lefèvre, Laurent Garcia, and Igor Stéphan. Justifications and Blocking Sets in a Rule-Based Answer Set Computation. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beatrix_et_al:OASIcs.ICLP.2016.6,
  author =	{B\'{e}atrix, Christopher and Lef\`{e}vre, Claire and Garcia, Laurent and St\'{e}phan, Igor},
  title =	{{Justifications and Blocking Sets in a Rule-Based Answer Set Computation}},
  booktitle =	{Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)},
  pages =	{6:1--6:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-007-1},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{52},
  editor =	{Carro, Manuel and King, Andy and Saeedloei, Neda and De Vos, Marina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2016.6},
  URN =		{urn:nbn:de:0030-drops-67310},
  doi =		{10.4230/OASIcs.ICLP.2016.6},
  annote =	{Keywords: Answer Set Programming, Justification, Rule-based Computation}
}
Document
DOI: 10.4230/DagSemProc.05171.6
Possibilistic Stable Models

Authors: Pascal Nicolas, Laurent Garcia, and Igor Stéphan

Published in: Dagstuhl Seminar Proceedings, Volume 5171, Nonmonotonic Reasoning, Answer Set Programming and Constraints (2005)

Abstract
We present the main lines of a new framework that we have defined in order to improve the knowledge representation power of Answer Set Programming paradigm. Our proposal is to use notions from possibility theory to extend the stable model semantics by taking into account a certainty level, expressed in terms of necessity measure, on each rule of a normal logic program. First of all, we introduce possibilistic definite logic programs and show how to compute the conclusions of such programs both in syntactic and semantic ways. The syntactic handling is done by help of a fix-point operator, the semantic part relies on a possibility distribution on all sets of atoms and the two approaches are shown to be equivalent. In a second part, we define what is a possibilistic stable model for a normal logic program, with default negation. Again, we define a possibility distribution allowing to determine the stable models. We end our presentation by showing how we can use our framework to adressing inconsistency in Answer Set Programming.
Cite as

Pascal Nicolas, Laurent Garcia, and Igor Stéphan. Possibilistic Stable Models. In Nonmonotonic Reasoning, Answer Set Programming and Constraints. Dagstuhl Seminar Proceedings, Volume 5171, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{nicolas_et_al:DagSemProc.05171.6,
  author =	{Nicolas, Pascal and Garcia, Laurent and St\'{e}phan, Igor},
  title =	{{Possibilistic Stable Models}},
  booktitle =	{Nonmonotonic Reasoning, Answer Set Programming and Constraints},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5171},
  editor =	{Gerhard Brewka and Ilkka Niemel\"{a} and Torsten Schaub and Miroslaw Truszczynski},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05171.6},
  URN =		{urn:nbn:de:0030-drops-2641},
  doi =		{10.4230/DagSemProc.05171.6},
  annote =	{Keywords: Non monotonic reasoning, uncertainty, possibility theory}
}
  • Refine by Author
  • 3 Stéphan, Igor
  • 2 Garcia, Laurent
  • 2 Le Roux, Stéphane
  • 1 Bouyer, Patricia
  • 1 Béatrix, Christopher
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 1 Software and its engineering → Model checking
  • 1 Software and its engineering → Software verification
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Proof complexity
  • Show More...

  • Refine by Keyword
  • 1 Answer Set Programming
  • 1 Constraint Handling Rules
  • 1 Justification
  • 1 Linear Logic
  • 1 Non monotonic reasoning
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2018
  • 2 2020
  • 1 2005
  • 1 2016

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact