3 citations · 5 across the 13 of their papers we have counts for
16 papers
On Synthesis of Metric Interval Temporal Logics
Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj Madnani
Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications…
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…
When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics
Hsi-Ming Ho, Khushraj Madnani
Pnueli first noticed that certain simple 'counting' properties appear to be inexpressible in popular timed temporal logics such as Metric Interval Temporal Logic (MITL). This inter…
An efficient quantifier elimination procedure for Presburger arithmetic
Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani +2
All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has e…
Monus semantics in vector addition systems with states
Pascal Baumann, Khushraj Madnani, Filip Mazowiecki +1
Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometime…
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…
A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence
Gabriel de Albuquerque Gleizer, Khushraj Nanik Madnani, Manuel Mazo
This paper studies the reduction (abstraction) of finite-state transition systems for control synthesis problems. We revisit the notion of alternating simulation equivalence (ASE),…
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…
Self-Triggered Control for Near-Maximal Average Inter-Sample Time
Gabriel de Albuquerque Gleizer, Khushraj Madnani, Manuel Mazo
Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications within networked-control systems; however, existing STC mechanisms often maximize…
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…
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…
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…
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…
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…