3 Search Results for "Mahajan, Ashutosh"

Document
DOI: 10.4230/LIPIcs.STACS.2026.64
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
DOI: 10.4230/LIPIcs.CSL.2026.33
Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

Authors: Isa Vialard

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this paper, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.
Cite as

Isa Vialard. Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{vialard:LIPIcs.CSL.2026.33,
  author =	{Vialard, Isa},
  title =	{{Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.33},
  URN =		{urn:nbn:de:0030-drops-254580},
  doi =		{10.4230/LIPIcs.CSL.2026.33},
  annote =	{Keywords: Weighted timed games, decidability, real-time systems}
}
Document
DOI: 10.4230/LIPIcs.SEA.2022.23
Automatic Reformulations for Convex Mixed-Integer Nonlinear Optimization: Perspective and Separability

Authors: Meenarli Sharma and Ashutosh Mahajan

Published in: LIPIcs, Volume 233, 20th International Symposium on Experimental Algorithms (SEA 2022)

Abstract
Tight reformulations of combinatorial optimization problems like Convex Mixed-Integer Nonlinear Programs (MINLPs) enable one to solve these problems faster by obtaining tight bounds on optimal value. We consider two techniques for reformulation: perspective reformulation and separability detection. We develop routines for automatic detection of problem structures suitable for these reformulations, and implement new extensions. Since detecting all "on-off" sets for perspective reformulation in a problem can be as hard as solving the original problem, we develop heuristic methods to automatically identify them. The LP/NLP branch-and-bound method is strengthened via "perspective cuts" derived from these automatic routines. We also provide methods to generate tight perspective cuts at different nodes in the branch-and-bound tree. The second structure, i.e., separability of nonlinear functions, is detected by means of the computational graph of the function. Our routines have been implemented in the open-source Minotaur solver for general convex MINLPs. Computational results show an improvement of up to 45% in the solution time and the size of the branch-and-bound tree for convex instances from benchmark library MINLPLib. On instances where reformulation using function separability induces structures that are amenable to perspective reformulation, we observe an improvement of up to 88% in the solution time.
Cite as

Meenarli Sharma and Ashutosh Mahajan. Automatic Reformulations for Convex Mixed-Integer Nonlinear Optimization: Perspective and Separability. In 20th International Symposium on Experimental Algorithms (SEA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 233, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{sharma_et_al:LIPIcs.SEA.2022.23,
  author =	{Sharma, Meenarli and Mahajan, Ashutosh},
  title =	{{Automatic Reformulations for Convex Mixed-Integer Nonlinear Optimization: Perspective and Separability}},
  booktitle =	{20th International Symposium on Experimental Algorithms (SEA 2022)},
  pages =	{23:1--23:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-251-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{233},
  editor =	{Schulz, Christian and U\c{c}ar, Bora},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2022.23},
  URN =		{urn:nbn:de:0030-drops-165579},
  doi =		{10.4230/LIPIcs.SEA.2022.23},
  annote =	{Keywords: Convex MINLP, perspective reformulation, branch-and-bound, outer approximation, function separability}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 1 2022

  • Refine by Author
  • 1 Lasota, Sławomir
  • 1 Lehaut, Mathieu
  • 1 Mahajan, Ashutosh
  • 1 Parreaux, Julie
  • 1 Piórkowski, Radosław
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Timed and hybrid models
  • 1 Applied computing → Operations research
  • 1 Mathematics of computing → Combinatorial optimization
  • 1 Mathematics of computing → Solvers
  • 1 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 1 Büchi-Landweber games
  • 1 Church synthesis problem
  • 1 Convex MINLP
  • 1 Weighted timed games
  • 1 branch-and-bound
  • 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
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact