7 Search Results for "Horn, Florian"


Document
Embarrassingly Greedy Inconsistency Resolution of Qualitative Constraint Networks

Authors: Michael Sioutis

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)


Abstract
In this paper, we deal with inconsistency resolution in qualitative constraint networks (QCN). This type of networks allows one to represent and reason about spatial or temporal information in a natural, human-like manner, e.g., by expressing relations of the form x {is north of ∨ is east of} y. On the other hand, inconsistency resolution involves maximizing the amount of information that is consistent in a knowledge base; in the context of QCNs, this translates to maximizing the number of constraints that can be satisfied, via obtaining a qualitative solution (scenario) of the QCN that ignores/violates as few of the original constraints as possible. To this end, we present two novel approaches: a greedy constraint-based and an optimal Partial MaxSAT-based one, with a focus on the former due to its simplicity. Specifically, the greedy technique consists in adding the constraints of a QCN to a new, initially empty network, one by one, all the while filtering out the ones that fail the satisfiability check. What makes or breaks this technique is the ordering in which the constraints will be processed to saturate the empty QCN, and for that purpose we use many different strategies to form a portfolio-style implementation. The Partial MaxSAT-based approach is powered by Horn theory-based maximal tractable subsets of relations. Finally, we compare the greedy approach with the optimal one, commenting on the trade-off between obtaining repairs that are optimal and obtaining repairs in a manner that is fast, and make our source code available for anyone to use.

Cite as

Michael Sioutis. Embarrassingly Greedy Inconsistency Resolution of Qualitative Constraint Networks. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 12:1-12:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{sioutis:LIPIcs.TIME.2023.12,
  author =	{Sioutis, Michael},
  title =	{{Embarrassingly Greedy Inconsistency Resolution of Qualitative Constraint Networks}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{12:1--12:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.12},
  URN =		{urn:nbn:de:0030-drops-191020},
  doi =		{10.4230/LIPIcs.TIME.2023.12},
  annote =	{Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Inconsistency Resolution, Maximizing Satisfiability, Greedy Algorithm, Partial MaxSAT Solver}
}
Document
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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}
}
  • Refine by Author
  • 6 Horn, Florian
  • 1 Asarin, Eugene
  • 1 Cervelle, Julien
  • 1 Colcombet, Thomas
  • 1 Cristau, Julien
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Temporal reasoning
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Constraint and logic programming

  • Refine by Keyword
  • 2 Games
  • 1 Controller synthesis
  • 1 Cut-offs
  • 1 Game Theory
  • 1 Greedy Algorithm
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 2 2008
  • 1 2009
  • 1 2014
  • 1 2016
  • 1 2020
  • Show More...

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