7 Search Results for "Witteveen, Cees"


Document
One-Clock Synthesis Problems

Authors: Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)


Abstract
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton, and one of the players can elapse time. We perform a systematic study of synthesis problems in all variants of timed games, depending on which player’s winning condition is specified, and which player’s strategy (or controller, a finite-memory strategy) is sought. As our main result we prove ubiquitous undecidability in all the variants, both for strategy and controller synthesis, already for winning conditions specified by one-clock automata. This strengthens and generalises previously known undecidability results. We also fully characterise those cases where finite memory is sufficient to win, namely existence of a strategy implies existence of a controller. All our results are stated in the timed setting, while analogous results hold in the data setting where one-clock automata are replaced by one-register ones.

Cite as

Sławomir Lasota, Mathieu Lehaut, Julie Parreaux, and Radosław Piórkowski. One-Clock Synthesis Problems. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 64:1-64:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{lasota_et_al:LIPIcs.STACS.2026.64,
  author =	{Lasota, S{\l}awomir and Lehaut, Mathieu and Parreaux, Julie and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{One-Clock Synthesis Problems}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{64:1--64:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.64},
  URN =		{urn:nbn:de:0030-drops-255533},
  doi =		{10.4230/LIPIcs.STACS.2026.64},
  annote =	{Keywords: timed automata, register automata, B\"{u}chi-Landweber games, Church synthesis problem, reactive synthesis problem}
}
Document
An Application of SAT Solvers in Integer Programming Games

Authors: Pravesh Koirala, Aditya Shrey, and Forrest Laine

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)


Abstract
Integer programming games (IPGs) are a popular game-theoretic tool to model an array of games where each player has a discrete strategy set. These games arise in important domains such as economics, transportation, cybersecurity, etc., but solving them is non-trivial as it is known that checking for the existence of pure Nash equilibria in an IPG is Σ₂^p-complete. Recent works have proposed a class of relaxed solution concepts for IPGs called locally optimal integer solutions (LOIS) and shown it to be an efficient alternative for pure Nash equilibria. While LOIS are significantly simpler to compute, they still do not scale when solved using traditional mathematical solvers, especially when high-quality solutions are desired. In this paper, we apply commercially available SAT solvers to find LOIS in IPGs. We investigate efficient encodings for a cybersecurity game and compare solution times when using SAT solvers vs mathematical program solvers. We also investigate the application of SAT solvers in graph games using a graph interdiction example and compare against the obtained LOI solutions against existing heuristics-based solutions. Our results indicate that with appropriate encodings, large-scale IPGs can be solved much more efficiently using SAT solvers. We also show that SAT solvers can be applied to graph games in conjunction with LOIS for obtaining high-quality solutions. Our results emphasize the potential of SAT solvers combined with LOIS to solve significant game theory problems.

Cite as

Pravesh Koirala, Aditya Shrey, and Forrest Laine. An Application of SAT Solvers in Integer Programming Games. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 19:1-19:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{koirala_et_al:LIPIcs.SAT.2025.19,
  author =	{Koirala, Pravesh and Shrey, Aditya and Laine, Forrest},
  title =	{{An Application of SAT Solvers in Integer Programming Games}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{19:1--19:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.19},
  URN =		{urn:nbn:de:0030-drops-237534},
  doi =		{10.4230/LIPIcs.SAT.2025.19},
  annote =	{Keywords: Game Theory, Integer Programming Games, SAT Solvers, Local Solutions, Graph Games}
}
Document
08461 Abstracts Collection – Planning in Multiagent Systems

Authors: Jürgen Dix, Edmund H. Durfee, and Cees Witteveen

Published in: Dagstuhl Seminar Proceedings, Volume 8461, Planning in Multiagent Systems (2009)


Abstract
From the 9th of November to the 14th of November 2008 the Dagstuhl Seminar 08461 '`Planning in Multiagent Systems'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Jürgen Dix, Edmund H. Durfee, and Cees Witteveen. 08461 Abstracts Collection – Planning in Multiagent Systems. In Planning in Multiagent Systems. Dagstuhl Seminar Proceedings, Volume 8461, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{dix_et_al:DagSemProc.08461.1,
  author =	{Dix, J\"{u}rgen and Durfee, Edmund H. and Witteveen, Cees},
  title =	{{08461 Abstracts Collection – Planning in Multiagent Systems}},
  booktitle =	{Planning in Multiagent Systems},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{8461},
  editor =	{J\"{u}rgen Dix and Edmund H. Durfee and Cees Witteveen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08461.1},
  URN =		{urn:nbn:de:0030-drops-18740},
  doi =		{10.4230/DagSemProc.08461.1},
  annote =	{Keywords: Multi-agent systems, AI-planning, coordination, robustness, temporal planning}
}
Document
08461 Executive Summary – Planning in Multi-Agent Systems

Authors: Jürgen Dix, Edmund H. Durfee, and Cees Witteveen

Published in: Dagstuhl Seminar Proceedings, Volume 8461, Planning in Multiagent Systems (2009)


Abstract
Planning in Multiagent Systems, or Multiagent Planning (MAP for short), considers the planning problem in the context of multiagent systems. It extends traditional AI planning to domains where multiple agents are involved in a plan and need to act together. Research in multiagent planning is promising for real-world problems: on one hand, AI planning techniques provide powerful tools for solving problems in single agent settings; on the other hand, multiagent systems, which have made significant progress over the past few years, are recognized as a key technology for tackling complex problems in realistic application domains. The motivation for this seminar is thus to bring together researchers working on these different fields in AI planning and multiagent systems to discuss the central topics mentioned above, to identify potential opportunities for coordination, and to develop benchmarks for future research in multiagent planning.

Cite as

Jürgen Dix, Edmund H. Durfee, and Cees Witteveen. 08461 Executive Summary – Planning in Multi-Agent Systems. In Planning in Multiagent Systems. Dagstuhl Seminar Proceedings, Volume 8461, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{dix_et_al:DagSemProc.08461.2,
  author =	{Dix, J\"{u}rgen and Durfee, Edmund H. and Witteveen, Cees},
  title =	{{08461 Executive Summary – Planning in Multi-Agent Systems }},
  booktitle =	{Planning in Multiagent Systems},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{8461},
  editor =	{J\"{u}rgen Dix and Edmund H. Durfee and Cees Witteveen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08461.2},
  URN =		{urn:nbn:de:0030-drops-18739},
  doi =		{10.4230/DagSemProc.08461.2},
  annote =	{Keywords: Multi-agent systems, AI-planning, coordination, robustness, temporal planning}
}
Document
ASODPOP: Making Open DPOP Asynchronous

Authors: Brammert Ottens

Published in: Dagstuhl Seminar Proceedings, Volume 8461, Planning in Multiagent Systems (2009)


Abstract
In this paper we show how ODPOP can be adapted to an asynchronous environment where agents might have to decide their values before the algorithm has ended, giving us Asynchronous ODPOP (ASODPOP). We have compared the algorithm with both ADOPT and distributed local search (DSA). Compared to ADOPT we show that our approach sends fewer messages, converges to a reasonable solution faster, and uses an equal amount of NCCCs. We also show that this convergence is much faster than local search, whilst the solution that local search converges to is far from optimal.

Cite as

Brammert Ottens. ASODPOP: Making Open DPOP Asynchronous. In Planning in Multiagent Systems. Dagstuhl Seminar Proceedings, Volume 8461, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{ottens:DagSemProc.08461.3,
  author =	{Ottens, Brammert},
  title =	{{ASODPOP: Making Open DPOP Asynchronous}},
  booktitle =	{Planning in Multiagent Systems},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{8461},
  editor =	{J\"{u}rgen Dix and Edmund H. Durfee and Cees Witteveen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08461.3},
  URN =		{urn:nbn:de:0030-drops-18714},
  doi =		{10.4230/DagSemProc.08461.3},
  annote =	{Keywords: DCOP, Logistics, Planning, Coordination}
}
Document
Creating incentives to prevent execution failures: an extension of VCG mechanism

Authors: Yingqian Zhang and Mathijs de Weerdt

Published in: Dagstuhl Seminar Proceedings, Volume 8461, Planning in Multiagent Systems (2009)


Abstract
When information or control in a multiagent planning system is private to the agents, they may misreport this information or refuse to execute an agreed outcome, in order to change the resulting end state of such a system to their benefit. In some domains this may result in an execution failure. We show that in such settings VCG mechanisms lose truthfulness, and that the utility of truthful agents can become negative when using VCG payments (i.e., VCG is not strongly individually rational). To deal with this problem, we introduce an extended payment structure which takes into account the actual execution of the promised outcome. We show that this extended mechanism can guarantee a nonnegative utility and is (i) incentive compatible in a Nash equilibrium, and (ii) incentive compatible in dominant strategies if and only if all agents can be verified during execution.

Cite as

Yingqian Zhang and Mathijs de Weerdt. Creating incentives to prevent execution failures: an extension of VCG mechanism. In Planning in Multiagent Systems. Dagstuhl Seminar Proceedings, Volume 8461, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{zhang_et_al:DagSemProc.08461.4,
  author =	{Zhang, Yingqian and de Weerdt, Mathijs},
  title =	{{Creating incentives to prevent execution failures: an extension of VCG mechanism}},
  booktitle =	{Planning in Multiagent Systems},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{8461},
  editor =	{J\"{u}rgen Dix and Edmund H. Durfee and Cees Witteveen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08461.4},
  URN =		{urn:nbn:de:0030-drops-18705},
  doi =		{10.4230/DagSemProc.08461.4},
  annote =	{Keywords: Mechanism design, multiagent planning}
}
Document
Using Options with Set Exercise Prices to Reduce Bidder Exposure in Sequential Auctions

Authors: Lonneke Mous, Valentin Robu, and Han La Poutre

Published in: Dagstuhl Seminar Proceedings, Volume 8461, Planning in Multiagent Systems (2009)


Abstract
The exposure problem appears whenever an agent with complementary valuations bids to acquire a bundle of items sold sequentially, in separate auctions. In this talk, we review a possible solution that can help solve this problem, which involves selling options for the items, instead of the items themselves. We provide a brief overview of the state of the art in this field and discuss, based on our recent results, under which conditions using option mechanisms would be desirable for both buyers and sellers, by comparison to direct auctioning of items. We conclude with a brief discussion of further research directions in this field, as well as the relation to other techniques proposed to address the problem, such as leveled commitment mechanisms.

Cite as

Lonneke Mous, Valentin Robu, and Han La Poutre. Using Options with Set Exercise Prices to Reduce Bidder Exposure in Sequential Auctions. In Planning in Multiagent Systems. Dagstuhl Seminar Proceedings, Volume 8461, pp. 1-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{mous_et_al:DagSemProc.08461.5,
  author =	{Mous, Lonneke and Robu, Valentin and La Poutre, Han},
  title =	{{Using Options with Set Exercise Prices to Reduce Bidder Exposure in Sequential Auctions}},
  booktitle =	{Planning in Multiagent Systems},
  pages =	{1--35},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{8461},
  editor =	{J\"{u}rgen Dix and Edmund H. Durfee and Cees Witteveen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08461.5},
  URN =		{urn:nbn:de:0030-drops-18724},
  doi =		{10.4230/DagSemProc.08461.5},
  annote =	{Keywords: Options, sequential auctions, multi-agent systems, exposure problem, bidding strategies, mechanism design, leveled commitment}
}
  • Refine by Type
  • 7 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 5 2009

  • Refine by Author
  • 2 Dix, Jürgen
  • 2 Durfee, Edmund H.
  • 2 Witteveen, Cees
  • 1 Koirala, Pravesh
  • 1 La Poutre, Han
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 5 DagSemProc

  • Refine by Classification
  • 1 Security and privacy → Network security
  • 1 Theory of computation → Algorithmic game theory and mechanism design
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Quantitative automata
  • Show More...

  • Refine by Keyword
  • 2 AI-planning
  • 2 Multi-agent systems
  • 2 coordination
  • 2 robustness
  • 2 temporal planning
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail