activity
20172026
most citedWhen Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics

1 citations · 1 across the 6 of their papers we have counts for

collaborators
Showing cs.LOShow all

9 papers · 1 filter

cs.LO2026

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…

cs.LO2024

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…

cs.LO2024★ 1 cited

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…

cs.LO2024

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…

cs.LO2023

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…

cs.LO2023

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…