Search Results

Documents authored by Madnani, Khushraj

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.142
An Efficient Quantifier Elimination Procedure for Presburger Arithmetic

Authors: Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existentially quantified variables in singly exponential time. As corollaries, we can establish the precise complexity of numerous problems. Examples include deciding (i) monadic decomposability for existential formulas, (ii) whether an existential formula defines a well-quasi ordering or, more generally, (iii) certain formulas of Presburger arithmetic with Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure shows that under mild assumptions, even NP upper bounds for decision problems about quantifier-free formulas can be transferred to existential formulas. The technical basis of our results is a kind of small model property for parametric integer programming that generalizes the seminal results by von zur Gathen and Sieveking on small integer points in convex polytopes.
Cite as

Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 142:1-142:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.ICALP.2024.142,
  author =	{Haase, Christoph and Krishna, Shankara Narayanan and Madnani, Khushraj and Mishra, Om Swostik and Zetzsche, Georg},
  title =	{{An Efficient Quantifier Elimination Procedure for Presburger Arithmetic}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{142:1--142:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.142},
  URN =		{urn:nbn:de:0030-drops-202856},
  doi =		{10.4230/LIPIcs.ICALP.2024.142},
  annote =	{Keywords: Presburger arithmetic, quantifier elimination, parametric integer programming, convex geometry}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.42
Counter Machines with Infrequent Reversals

Authors: Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
Bounding the number of reversals in a counter machine is one of the most prominent restrictions to achieve decidability of the reachability problem. Given this success, we explore whether this notion can be relaxed while retaining decidability. To this end, we introduce the notion of an f-reversal-bounded counter machine for a monotone function f: ℕ → ℕ. In such a machine, every run of length n makes at most f(n) reversals. Our first main result is a dichotomy theorem: We show that for every monotone function f, one of the following holds: Either (i) f grows so slowly that every f-reversal bounded counter machine is already k-reversal bounded for some constant k or (ii) f belongs to Ω(log(n)) and reachability in f-reversal bounded counter machines is undecidable. This shows that classical reversal bounding already captures the decidable cases of f-reversal bounding for any monotone function f. The key technical ingredient is an analysis of the growth of small solutions of iterated compositions of Presburger-definable constraints. In our second contribution, we investigate whether imposing f-reversal boundedness improves the complexity of the reachability problem in vector addition systems with states (VASS). Here, we obtain an analogous dichotomy: We show that either (i) f grows so slowly that every f-reversal-bounded VASS is already k-reversal-bounded for some constant k or (ii) f belongs to Ω(n) and the reachability problem for f-reversal-bounded VASS remains Ackermann-complete. This result is proven using run amalgamation in VASS. Overall, our results imply that classical restriction of reversal boundedness is a robust one.
Cite as

Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche. Counter Machines with Infrequent Reversals. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2023.42,
  author =	{Finkel, Alain and Krishna, Shankara Narayanan and Madnani, Khushraj and Majumdar, Rupak and Zetzsche, Georg},
  title =	{{Counter Machines with Infrequent Reversals}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.42},
  URN =		{urn:nbn:de:0030-drops-194152},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.42},
  annote =	{Keywords: Counter machines, reversal-bounded, reachability, decidability, complexity}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.7
More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words

Authors: Hsi-Ming Ho and Khushraj Madnani

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

Abstract
We study the expressiveness of the pointwise interpretations (i.e. over timed words) of some predicate and temporal logics with metric and counting features. We show that counting in the unit interval (0, 1) is strictly weaker than counting in (0, b) with arbitrary b ≥ 0; moreover, allowing the latter indeed leads to expressive completeness for the metric predicate logic Q2MLO, recovering the corresponding result for the continuous interpretations (i.e. over signals). Exploiting this connection, we show that in contrast to the continuous case, adding "punctual" predicates into Q2MLO is still insufficient for the full expressive power of the Monadic First-Order Logic of Order and Metric (FO[<,+1]). Finally, we propose a generalisation of the recently proposed Pnueli automata modalities and show that the resulting metric temporal logic is expressively complete for FO[<,+1].
Cite as

Hsi-Ming Ho and Khushraj Madnani. More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ho_et_al:LIPIcs.TIME.2023.7,
  author =	{Ho, Hsi-Ming and Madnani, Khushraj},
  title =	{{More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{7:1--7:15},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.7},
  URN =		{urn:nbn:de:0030-drops-190979},
  doi =		{10.4230/LIPIcs.TIME.2023.7},
  annote =	{Keywords: Temporal Logic, Expressiveness, Automata}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.10
Monus Semantics in Vector Addition Systems with States

Authors: Pascal Baumann, Khushraj Madnani, Filip Mazowiecki, and Georg Zetzsche

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which these problems can be decided more efficiently. We study an overapproximation, called monus semantics, that slightly relaxes the semantics of decrements: A key property of a vector addition systems is that in order to decrement a counter, this counter must have a positive value. In contrast, our semantics allows decrements of zero-valued counters: If such a transition is executed, the counter just remains zero. It turns out that if only a subset of transitions is used with monus semantics (and the others with classical semantics), then reachability is undecidable. However, we show that if monus semantics is used throughout, reachability remains decidable. In particular, we show that reachability for VASS with monus semantics is as hard as that of classical VASS (i.e. Ackermann-hard), while the zero-reachability and coverability are easier (i.e. EXPSPACE-complete and NP-complete, respectively). We provide a comprehensive account of the complexity of the general reachability problem, reachability of zero configurations, and coverability under monus semantics. We study these problems in general VASS, two-dimensional VASS, and one-dimensional VASS, with unary and binary counter updates.
Cite as

Pascal Baumann, Khushraj Madnani, Filip Mazowiecki, and Georg Zetzsche. Monus Semantics in Vector Addition Systems with States. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baumann_et_al:LIPIcs.CONCUR.2023.10,
  author =	{Baumann, Pascal and Madnani, Khushraj and Mazowiecki, Filip and Zetzsche, Georg},
  title =	{{Monus Semantics in Vector Addition Systems with States}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.10},
  URN =		{urn:nbn:de:0030-drops-190047},
  doi =		{10.4230/LIPIcs.CONCUR.2023.10},
  annote =	{Keywords: Vector addition systems, Overapproximation, Reachability, Coverability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.39
Logics Meet 1-Clock Alternating Timed Automata

Authors: Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
This paper investigates a decidable and highly expressive real time logic QkMSO which is obtained by extending MSO[<] with guarded quantification using block of less than k metric quantifiers. The resulting logic is shown to be expressively equivalent to 1-clock ATA where loops are without clock resets, as well as, RatMTL, a powerful extension of MTL[U_I] with regular expressions. We also establish 4-variable property for QkMSO and characterize the expressive power of its 2-variable fragment. Thus, the paper presents progress towards expressively complete logics for 1-clock ATA.
Cite as

Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Logics Meet 1-Clock Alternating Timed Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krishna_et_al:LIPIcs.CONCUR.2018.39,
  author =	{Krishna, Shankara Narayanan and Madnani, Khushraj and Pandya, Paritosh K.},
  title =	{{Logics Meet 1-Clock Alternating Timed Automata}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{39:1--39:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.39},
  URN =		{urn:nbn:de:0030-drops-95779},
  doi =		{10.4230/LIPIcs.CONCUR.2018.39},
  annote =	{Keywords: Metric Temporal Logic, Alternating Timed Automata, MSO, Regular Expressions, Expressive Completeness}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.77
Making Metric Temporal Logic Rational

Authors: Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We study an extension of MTL in pointwise time with regular expression guarded modality Reg_I(re) where re is a rational expression over subformulae. We study the decidability and expressiveness of this extension (MTL+Ureg+Reg), called RegMTL, as well as its fragment SfrMTL where only star-free rational expressions are allowed. Using the technique of temporal projections, we show that RegMTL has decidable satisfiability by giving an equisatisfiable reduction to MTL. We also identify a subclass MITL+UReg of RegMTL for which our equisatisfiable reduction gives rise to formulae of MITL, yielding elementary decidability. As our second main result, we show a tight automaton-logic connection between SfrMTL and partially ordered (or very weak) 1-clock alternating timed automata.
Cite as

Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Making Metric Temporal Logic Rational. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 77:1-77:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{krishna_et_al:LIPIcs.MFCS.2017.77,
  author =	{Krishna, Shankara Narayanan and Madnani, Khushraj and Pandya, Paritosh K.},
  title =	{{Making Metric Temporal Logic Rational}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{77:1--77:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.77},
  URN =		{urn:nbn:de:0030-drops-81112},
  doi =		{10.4230/LIPIcs.MFCS.2017.77},
  annote =	{Keywords: Metric Temporal Logic, Timed Automata, Regular Expression, Equisatisfiability, Expressiveness}
}
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 About DROPS Imprint Privacy Contact