7 Search Results for "Ho, Hsi-Ming"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.19
Time for Timed Monitorability

Authors: Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
  author =	{Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
  title =	{{Time for Timed Monitorability}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.19},
  URN =		{urn:nbn:de:0030-drops-239690},
  doi =		{10.4230/LIPIcs.CONCUR.2025.19},
  annote =	{Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.24
Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.

Authors: Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Paritosh Pandya

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
We demonstrate a surprising and first-of-its-kind expressive equivalence between decidable metric and freeze logics over timed words in pointwise semantics. Our main result states that Metric Interval Temporal Logic with future, past and Pnueli modalities, MITPPL, and full unilateral timed propositional temporal logic with both future and past temporal modalities, UPTL, have identical expressiveness. One of the highlights of this paper, which allows for this equivalence, is to prove that UPTL formulas admit monadic decomposition. Our result also implies that several decidable logics for real-time specifications, such as one-variable UPTL, unilateral MITPPL, and Q2MLO, are all expressively equivalent, and the reductions between them are effective. Hence, our result unifies the fragmented expressiveness boundary of timed temporal logics. As corollaries, we resolve the open question of the decidability for full UPTL, and the variable or clock hierarchy problem for the future fragment of UPTL.
Cite as

Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Paritosh Pandya. Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ho_et_al:LIPIcs.CONCUR.2025.24,
  author =	{Ho, Hsi-Ming and Krishna, Shankara Narayanan and Madnani, Khushraj and Majumdar, Rupak and Pandya, Paritosh},
  title =	{{Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.24},
  URN =		{urn:nbn:de:0030-drops-239744},
  doi =		{10.4230/LIPIcs.CONCUR.2025.24},
  annote =	{Keywords: Timed Propositional Temporal Logic, Expressiveness, Metric Interval Temporal Logic, Satisfiability, Decidability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.7
More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words

Authors: Hsi-Ming Ho and Khushraj Madnani

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
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].
Cite as

Hsi-Ming Ho and Khushraj Madnani. More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ho_et_al:LIPIcs.TIME.2023.7,
  author =	{Ho, Hsi-Ming and Madnani, Khushraj},
  title =	{{More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.7},
  URN =		{urn:nbn:de:0030-drops-190979},
  doi =		{10.4230/LIPIcs.TIME.2023.7},
  annote =	{Keywords: Temporal Logic, Expressiveness, Automata}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.23
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

Authors: Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We investigate the decidability of the {0,∞} fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL^{0,∞} is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL^{0,∞}) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL^{0,∞} is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual’’ subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞}) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA^{0,∞}.
Cite as

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya. Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krishna_et_al:LIPIcs.CONCUR.2023.23,
  author =	{Krishna, Shankara Narayanan and Madnani, Khushraj Nanik and Majumdar, Rupak and Pandya, Paritosh},
  title =	{{Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.23},
  URN =		{urn:nbn:de:0030-drops-190171},
  doi =		{10.4230/LIPIcs.CONCUR.2023.23},
  annote =	{Keywords: TPTL, Satisfiability, Non-Punctuality, Decidability, Expressiveness, ATA}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.20
On Verifying Timed Hyperproperties

Authors: Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
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.
Cite as

Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones. On Verifying Timed Hyperproperties. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ho_et_al:LIPIcs.TIME.2019.20,
  author =	{Ho, Hsi-Ming and Zhou, Ruoyu and Jones, Timothy M.},
  title =	{{On Verifying Timed Hyperproperties}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.20},
  URN =		{urn:nbn:de:0030-drops-113782},
  doi =		{10.4230/LIPIcs.TIME.2019.20},
  annote =	{Keywords: Timed Automata, Temporal Logics, Cybersecurity}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.7
Timed-Automata-Based Verification of MITL over Signals

Authors: Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
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.
Cite as

Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. Timed-Automata-Based Verification of MITL over Signals. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.TIME.2017.7,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Ho, Hsi-Ming and Monmege, Benjamin},
  title =	{{Timed-Automata-Based Verification of MITL over Signals}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.7},
  URN =		{urn:nbn:de:0030-drops-79126},
  doi =		{10.4230/LIPIcs.TIME.2017.7},
  annote =	{Keywords: real-time temporal logic, timed automata, real-time systems}
}
  • Refine by Type
  • 7 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 2 2023
  • 1 2019
  • 1 2017

  • Refine by Author
  • 4 Ho, Hsi-Ming
  • 2 Krishna, Shankara Narayanan
  • 2 Madnani, Khushraj
  • 2 Majumdar, Rupak
  • 2 Pandya, Paritosh
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 2 Theory of computation → Logic
  • 2 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Automata over infinite objects

  • Refine by Keyword
  • 3 Expressiveness
  • 2 Decidability
  • 2 Satisfiability
  • 2 Timed Automata
  • 1 ATA
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact