Search Results

Documents authored by Horn, Florian

Document
DOI: 10.4230/LIPIcs.CONCUR.2020.46
Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks

Authors: Florian Horn and Arnaud Sangnier

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

Abstract
We study networks of processes which all execute the same finite-state protocol and communicate thanks to a rendez-vous mechanism. Given a protocol, we are interested in checking whether there exists a number, called a cut-off, such that in any networks with a bigger number of participants, there is an execution where all the entities end in some final states. We provide decidability and complexity results of this problem under various assumptions, such as absence/presence of a leader or symmetric/asymmetric rendez-vous.
Cite as

Florian Horn and Arnaud Sangnier. Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{horn_et_al:LIPIcs.CONCUR.2020.46,
  author =	{Horn, Florian and Sangnier, Arnaud},
  title =	{{Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{46:1--46:16},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.46},
  URN =		{urn:nbn:de:0030-drops-128581},
  doi =		{10.4230/LIPIcs.CONCUR.2020.46},
  annote =	{Keywords: Parameterized networks, Verification, Cut-offs}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.11
Entropy Games and Matrix Multiplication Games

Authors: Eugene Asarin, Julien Cervelle, Aldric Degorre, Catalin Dima, Florian Horn, and Victor Kozyakin

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
Two intimately related new classes of games are introduced and studied: entropy games (EGs) and matrix multiplication games (MMGs). An EG is played on a finite arena by two-and-a-half players: Despot, Tribune and the non-deterministic People. Despot wants to make the set of possible People's behaviors as small as possible, while Tribune wants to make it as large as possible. An MMG is played by two players that alternately write matrices from some predefined finite sets. One wants to maximize the growth rate of the product, and the other to minimize it. We show that in general MMGs are undecidable in quite a strong sense. On the positive side, EGs correspond to a subclass of MMGs, and we prove that such MMGs and EGs are determined, and that the optimal strategies are simple. The complexity of solving such games is in NP cap coNP.
Cite as

Eugene Asarin, Julien Cervelle, Aldric Degorre, Catalin Dima, Florian Horn, and Victor Kozyakin. Entropy Games and Matrix Multiplication Games. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{asarin_et_al:LIPIcs.STACS.2016.11,
  author =	{Asarin, Eugene and Cervelle, Julien and Degorre, Aldric and Dima, Catalin and Horn, Florian and Kozyakin, Victor},
  title =	{{Entropy Games and Matrix Multiplication Games}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.11},
  URN =		{urn:nbn:de:0030-drops-57129},
  doi =		{10.4230/LIPIcs.STACS.2016.11},
  annote =	{Keywords: game theory, entropy, joint spectral radius}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.379
Playing Safe

Authors: Thomas Colcombet, Nathanael Fijalkow, and Florian Horn

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.
Cite as

Thomas Colcombet, Nathanael Fijalkow, and Florian Horn. Playing Safe. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 379-390, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.379,
  author =	{Colcombet, Thomas and Fijalkow, Nathanael and Horn, Florian},
  title =	{{Playing Safe}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{379--390},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.379},
  URN =		{urn:nbn:de:0030-drops-48571},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.379},
  annote =	{Keywords: Game Theory, Synthesis, Safety Specifications, Program Verification}
}
Document
DOI: 10.4230/LIPIcs.STACS.2009.1848
Random Fruits on the Zielonka Tree

Authors: Florian Horn

Published in: LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

Abstract
Stochastic games are a natural model for the synthesis of controllers confronted to adversarial and/or random actions. In particular, $\omega$-regular games of infinite length can represent reactive systems which are not expected to reach a correct state, but rather to handle a continuous stream of events. One critical resource in such applications is the memory used by the controller. In this paper, we study the amount of memory that can be saved through the use of randomisation in strategies, and present matching upper and lower bounds for stochastic Muller games.
Cite as

Florian Horn. Random Fruits on the Zielonka Tree. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 541-552, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{horn:LIPIcs.STACS.2009.1848,
  author =	{Horn, Florian},
  title =	{{Random Fruits on the Zielonka Tree}},
  booktitle =	{26th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{541--552},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-09-5},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{3},
  editor =	{Albers, Susanne and Marion, Jean-Yves},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1848},
  URN =		{urn:nbn:de:0030-drops-18489},
  doi =		{10.4230/LIPIcs.STACS.2009.1848},
  annote =	{Keywords: Model checking, Controller synthesis, Stochastic games, Randomisation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1756
Explicit Muller Games are PTIME

Authors: Florian Horn

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

Abstract
Regular games provide a very useful model for the synthesis of controllers in reactive systems. The complexity of these games depends on the representation of the winning condition: if it is represented through a win-set, a coloured condition, a Zielonka-DAG or Emerson-Lei formulae, the winner problem is \pspace-complete; if the winning condition is represented as a Zielonka tree, the winner problem belongs to \np and \conp. In this paper, we show that explicit Muller games can be solved in polynomial time, and provide an effective algorithm to compute the winning regions.
Cite as

Florian Horn. Explicit Muller Games are PTIME. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 235-243, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{horn:LIPIcs.FSTTCS.2008.1756,
  author =	{Horn, Florian},
  title =	{{Explicit Muller Games are PTIME}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{235--243},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1756},
  URN =		{urn:nbn:de:0030-drops-17565},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1756},
  annote =	{Keywords: Games, authomata, model checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1748
Graph Games on Ordinals

Authors: Julien Cristau and Florian Horn

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

Abstract
We consider an extension of Church\'s synthesis problem to ordinals by adding limit transitions to graph games. We consider game arenas where these limit transitions are defined using the sets of cofinal states. In a previous paper, we have shown that such games of ordinal length are determined and that the winner problem is \pspace-complete, for a subclass of arenas where the length of plays is always smaller than $\omega^\omega$. However, the proof uses a rather involved reduction to classical Muller games, and the resulting strategies need infinite memory. We adapt the LAR reduction to prove the determinacy in the general case, and to generate strategies with finite memory, using a reduction to games where the limit transitions are defined by priorities. We provide an algorithm for computing the winning regions of both players in these games, with a complexity similar to parity games. Its analysis yields three results: determinacy without hypothesis on the length of the plays, existence of memoryless strategies, and membership of the winner problem in \npconp.
Cite as

Julien Cristau and Florian Horn. Graph Games on Ordinals. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 143-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{cristau_et_al:LIPIcs.FSTTCS.2008.1748,
  author =	{Cristau, Julien and Horn, Florian},
  title =	{{Graph Games on Ordinals}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{143--154},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1748},
  URN =		{urn:nbn:de:0030-drops-17485},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1748},
  annote =	{Keywords: Games, ordinals, zeno}
}
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