13 citations · 32 across the 18 of their papers we have counts for
21 papers
MightyPPL: Verification of MITL with Past and Pnueli Modalities
Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani +2
Metric Interval Temporal Logic (MITL) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using MITL in verificatio…
Openness And Partial Adjacency In One Variable TPTL
Shankara Narayanan Krishna, Khushraj Madnani, Agnipratim Nag +1
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) extend Linear Temporal Logic (LTL) for real-time constraints, with MTL using time-bounded modalities and T…
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar +1
We investigate the decidability of the fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL is PSPACE-c…
Logics Meet 2-Way 1-Clock Alternating Timed Automata
Shankara Narayanan Krishna, Khushraj Nanik Madnani, Manuel Mazo +1
In this paper, we study the extension of 1-clock Alternating Timed Automata (1-ATA) with the ability to read in both forward and backward direction, the 2-Way 1-clock Alternating T…
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
Shankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo +1
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking…
Specification and Optimal Reactive Synthesis of Run-time Enforcement Shields
Paritosh K. Pandya, Amol Wakankar
A system with sporadic errors (SSE) is a controller which produces high quality output but it may occasionally violate a critical requirement REQ(I,O). A run-time enforcement shiel…
Specification and Reactive Synthesis of Robust Controllers
Paritosh K. Pandya, Amol Wakankar
This paper investigates the synthesis of robust controllers from logical specification of regular properties given in an interval temporal logic QDDC. Our specification encompasses…
DCSYNTH: Guided Reactive Synthesis with Soft Requirements
Amol Wakankar, Paritosh K. Pandya, Rajmohan Matteplackel
In reactive controller synthesis, a number of implementations (controllers) are possible for a given specification because of the incomplete nature of specification. To choose the…
Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership
Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya +1
We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variabl…
Büchi-Kamp Theorems for 1-clock ATA
Shankara Narayanan Krishna, Khushraj Madnani, Paritosh Pandya
This paper investigates Kamp-like and Büchi-like theorems for 1-clock Alternating Timed Automata (1-ATA) and its natural subclasses. A notion of 1-ATA with loop-free-resets is defi…
DCSYNTH: Guided Reactive Synthesis with Soft Requirements for Robust Controller and Shield Synthesis
Amol Wakankar, Paritosh K. Pandya, Raj Mohan Matteplackel
DCSYNTH is a tool for the synthesis of controllers from safety and bounded liveness requirements given in interval temporal logic QDDC. It investigates the role of soft requirement…
Formalizing Timing Diagram Requirements in Discrete Duration Calulus
Raj Mohan Matteplackel, Paritosh K. Pandya, Amol Wakankar
Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. These include LTL, discrete time MTL and the recent indu…
Making Metric Temporal Logic Rational
Shankara Narayanan Krishna, Khushraj Madnani, P. K. Pandya
We study an extension of $\mtl$ in pointwise time with rational expression guarded modality $\reg_I(\re)$ where $\re$ is a rational expression over subformulae. We study the decida…
Deterministic Temporal Logics and Interval Constraints
Kamal Lodaya, Paritosh K. Pandya
In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiab…
Two-variable Logic with a Between Predicate
Andreas Krebs, Kamal Lodaya, Paritosh Pandya +1
We study an extension of FO^2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable…
Metric Temporal Logic with Counting
Khushraj Madnani, Shankara Narayanan Krishna, Paritosh Pandya
Ability to count number of occurrences of events within a specified time interval is very useful in specification of resource bounded real time computation. In this paper, we study…
Partially Punctual Metric Temporal Logic is Decidable
Khushraj Madnani, Shankara Narayanan Krishna, Paritosh Pandya
Metric Temporal Logic $\mathsf{MTL}[\until_I,\since_I]$ is one of the most studied real time logics. It exhibits considerable diversity in expressiveness and decidability propertie…
Deterministic Logics for UL
Paritosh K. Pandya, Simoni S. Shah
The class of Unambiguous Star-Free Regular Languages (UL) was defined by Schutzenberger as the class of languages defined by Unambiguous Polynomials. UL has been variously characte…
The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)
Paritosh K. Pandya, Simoni S. Shah
We study two unary fragments of the well-known metric interval temporal logic MITL[U_I,S_I] that was originally proposed by Alur and Henzinger, and we pin down their expressiveness…
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
Khushraj Madnani, Shankara Narayanan Krishna, Paritosh K. Pandya
Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permit…
On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing
Paritosh K. Pandya, Simoni S. Shah
Timed temporal logics exhibit a bewildering diversity of operators and the resulting decidability and expressiveness properties also vary considerably. We study the expressive powe…