4 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…
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…