Search Results

Documents authored by Pandya, Paritosh

Found 2 Possible Name Variants:

Pandya, Paritosh K.

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.CSL.2018.28
An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation

Authors: Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.
Cite as

Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krebs_et_al:LIPIcs.CSL.2018.28,
  author =	{Krebs, Andreas and Lodaya, Kamal and Pandya, Paritosh K. and Straubing, Howard},
  title =	{{An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.28},
  URN =		{urn:nbn:de:0030-drops-96953},
  doi =		{10.4230/LIPIcs.CSL.2018.28},
  annote =	{Keywords: two-variable logic, finite model theory, algebraic automata theory}
}
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}
}

Pandya, Paritosh

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.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
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2018
LIPIcs, Volume 122, FSTTCS'18, Complete Volume

Authors: Sumit Ganguly and Paritosh Pandya

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
LIPIcs, Volume 122, FSTTCS'18, Complete Volume
Cite as

38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Proceedings{ganguly_et_al:LIPIcs.FSTTCS.2018,
  title =	{{LIPIcs, Volume 122, FSTTCS'18, Complete Volume}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018},
  URN =		{urn:nbn:de:0030-drops-100240},
  doi =		{10.4230/LIPIcs.FSTTCS.2018},
  annote =	{Keywords: Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSTTCS.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Sumit Ganguly and Paritosh Pandya

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ganguly_et_al:LIPIcs.FSTTCS.2018.0,
  author =	{Ganguly, Sumit and Pandya, Paritosh},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.0},
  URN =		{urn:nbn:de:0030-drops-98992},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
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