Hsi-Ming Ho

TACAS Conference 2026 Conference Paper

MightyPPL: Model Checking MITL with Past and Pnueli Modalities

• Hsi-Ming Ho
• Shankara Narayanan Krishna
• Khushraj Madnani
• Rupak Majumdar
• Paritosh Pandya

I&C Journal 2025 Journal Article

Metric quantifiers and counting in timed logics and automata

• Hsi-Ming Ho
• Khushraj Madnani

We study the expressiveness of the pointwise interpretations (i. e. over timed words) of some predicate and temporal logics with metric and counting features. We show that counting in the unit interval ( 0, 1 ) is strictly weaker than counting in ( 0, b ) with arbitrary b ≥ 0; moreover, allowing the latter to be included in temporal logics leads to expressive completeness for the metric predicate logic Q2MLO, recovering the corresponding result for the continuous interpretations (i. e. over signals). Exploiting this connection, we show that in contrast to the continuous case, adding ‘punctual’ predicates into Q2MLO is still insufficient for the full expressive power of the Monadic First-Order Logic of Order and Metric (FO[ <, + 1 ]); as a remedy, we propose a generalisation of the recently proposed Pnueli automata modalities and show that the resulting metric temporal logic is expressively complete for FO[ <, + 1 ]. On the practical side, we propose a compositional construction from metric interval temporal logic with counting or similar extensions to timed automata, which is more amenable to implementation based on existing tools that support on-the-fly model checking.

TIME Conference 2023 Conference Paper

More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words

• Hsi-Ming Ho
• Khushraj Madnani

We study the expressiveness of the pointwise interpretations (i. e. over timed words) of some predicate and temporal logics with metric and counting features. We show that counting in the unit interval (0, 1) is strictly weaker than counting in (0, b) with arbitrary b ≥ 0; moreover, allowing the latter indeed leads to expressive completeness for the metric predicate logic Q2MLO, recovering the corresponding result for the continuous interpretations (i. e. over signals). Exploiting this connection, we show that in contrast to the continuous case, adding "punctual" predicates into Q2MLO is still insufficient for the full expressive power of the Monadic First-Order Logic of Order and Metric (FO[<, +1]). Finally, we propose a generalisation of the recently proposed Pnueli automata modalities and show that the resulting metric temporal logic is expressively complete for FO[<, +1].

I&C Journal 2021 Journal Article

Timed hyperproperties

• Hsi-Ming Ho
• Ruoyu Zhou
• Timothy M. Jones

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMITL, a timed extension of HyperLTL. While the satisfiability problem can be solved similarly as for HyperLTL, we show that the model-checking problem for HyperMITL, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMITL with quantifier alternations is possible under certain semantic restrictions. As an intermediate tool, we give an ‘asynchronous’ interpretation of Wilke's monadic logic of relative distance ( L d ↔ ) and show that it characterises timed languages recognised by timed automata with silent transitions.

TIME Conference 2019 Conference Paper

On Verifying Timed Hyperproperties

• Hsi-Ming Ho
• Ruoyu Zhou
• Timothy M. Jones 0001

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: synchronous and asynchronous. While the satisfiability problem can be decided similarly as for HyperLTL regardless of the choice of semantics, we show that the model-checking problem for HyperMTL, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.

Highlights Conference 2017 Conference Abstract

MightyL: A Compositional Translation from MITL to Timed Automata

• Hsi-Ming Ho

Abstract available in PDF.

TIME Conference 2017 Conference Paper

Timed-Automata-Based Verification of MITL over Signals

• Thomas Brihaye
• Gilles Geeraerts
• Hsi-Ming Ho
• Benjamin Monmege

It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i. e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i. e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.

Highlights Conference 2016 Conference Abstract

Real-Time Synthesis is Hard!

• Thomas Brihaye
• Morgane Estiévenart
• Gilles Geeraerts
• Hsi-Ming Ho
• Benjamin Monmege
• Nathalie Sznajder

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 infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D’Souza et al. and Bouyer et al.). During this talk, we precise the decidability border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it. This is joint work (submitted at FORMATS 2016) with Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho, and Nathalie Sznajder.