6 Search Results for "Madnani, Khushraj"

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-dev.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-dev.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-dev.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.2023.23
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

Authors: Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya

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

Abstract
We investigate the decidability of the {0,∞} fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL^{0,∞} is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL^{0,∞}) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL^{0,∞} is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual’’ subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞}) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA^{0,∞}.
Cite as

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya. Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krishna_et_al:LIPIcs.CONCUR.2023.23,
  author =	{Krishna, Shankara Narayanan and Madnani, Khushraj Nanik and Majumdar, Rupak and Pandya, Paritosh},
  title =	{{Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{23:1--23: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.23},
  URN =		{urn:nbn:de:0030-drops-190171},
  doi =		{10.4230/LIPIcs.CONCUR.2023.23},
  annote =	{Keywords: TPTL, Satisfiability, Non-Punctuality, Decidability, Expressiveness, ATA}
}
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-dev.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-dev.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}
}
  • Refine by Author
  • 5 Madnani, Khushraj
  • 4 Krishna, Shankara Narayanan
  • 2 Majumdar, Rupak
  • 2 Pandya, Paritosh K.
  • 2 Zetzsche, Georg
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Models of computation

  • Refine by Keyword
  • 3 Expressiveness
  • 2 Metric Temporal Logic
  • 1 ATA
  • 1 Alternating Timed Automata
  • 1 Automata
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 4 2023
  • 1 2017
  • 1 2018

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