4 citations · 8 across the 7 of their papers we have counts for
8 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…
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…
Revisiting Timed Logics with Automata Modalities
Hsi-Ming Ho
It is well known that (timed) -regular properties such as `p holds at every even position' and `p occurs at least three times within the next 10 time units' cannot be expressed…
On Verifying Timed Hyperproperties
Hsi-Ming Ho, Ruoyu Zhou, Timothy M. Jones
We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of event…
On the Expressiveness and Monitoring of Metric Temporal Logic
Hsi-Ming Ho, Joël Ouaknine, James Worrell
It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this…
Real-Time Synthesis is Hard!
Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts +3
We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infi…
The Cyclic-Routing UAV Problem is PSPACE-Complete
Hsi-Ming Ho, Joel Ouaknine
Consider a finite set of targets, with each target assigned a relative deadline, and each pair of targets assigned a fixed transit flight time. Given a flock of identical UAVs, can…