ÃûæÂÖ±²¥

Foundations of Software Systems (FoSS)

Hsi-Ming Ho

Selected Publications

2025

  • Ho, H. -M., Krishna, S. N., Madnani, K., Majumdar, R., & Pandya, P. (2025). Expressive equivalence between decidable freeze and metric timed temporal logics. In Leibniz International Proceedings in Informatics (pp. pages). Aarhus, Denmark: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2025.24
    Conference publication. .
  • Ho, H. -M., & Madnani, K. (2025). Metric quantifiers and counting in timed logics and automata. Information and Computation, 303, pages. doi:10.1016/j.ic.2025.105268
    Article. .

2024

  • Ho, H. -M., & Madnani, K. (2024). When do you start counting? Revisiting counting and Pnueli modalities in timed logics. Electronic Proceedings in Theoretical Computer Science, 408, 73–89 ( pages). doi:10.4204/EPTCS.408.5
    Article. .
  • Ho, H. -M., & Madnani, K. (2024). When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics. doi:10.48550/arxiv.2410.00539
    Preprint. .

2023

  • Ho, H. -M., & Madnani, K. (2023). More than 0s and 1s: metric quantifiers and counting over timed words. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023) Vol. 278 (pp. pages). Athens, Greece: Leibniz Association. doi:10.4230/LIPIcs.TIME.2023.7
    Conference publication. .

2021

  • Arif, M., Zhou, R., Ho, H. -M., & Jones, T. M. (2021). Cinnamon: a domain-specific language for binary profiling and monitoring. In 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO) (pp. 103-114). Seoul, Korea (South): IEEE. doi:10.1109/CGO51591.2021.9370313
    Conference publication. .

2020

  • Ho, H. -M., Zhou, R., & Jones, T. M. (2020). Timed hyperproperties. Information and Computation, pages. doi:10.1016/j.ic.2020.104639
    Article. .

2019

  • Ho, H. M., Zhou, R., & Jones, T. M. (2019). On verifying timed hyperproperties. In Leibniz International Proceedings in Informatics Lipics Vol. 147 (pp. 201-2018). doi:10.4230/LIPIcs.TIME.2019.20
    Conference publication. .
  • Drucker, N., Ho, H. M., Ouaknine, J., Penn, M., & Strichman, O. (2019). Cyclic-routing of Unmanned Aerial Vehicles. Journal of Computer and System Sciences, 103, 18-45. doi:10.1016/j.jcss.2019.02.002
    Article. .
  • Ho, H. -M., Ouaknine, J., & Worrell, J. (2019). On the expressiveness and monitoring of metric temporal logic. Logical Methods in Computer Science, 15(2), 13-52. doi:10.23638/LMCS-15(2:13)2019
    Article. .
  • Ho, H. M. (2019). Revisiting timed logics with automata modalities. In Hscc 2019 Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems Computation and Control (pp. 67-76). doi:10.1145/3302504.3311818
    Conference publication. .

2018

  • Brihaye, T., Geeraerts, G., Ho, H. M., Milchior, A., & Monmege, B. (2018). Efficient algorithms and tools for MITL model-checking and synthesis. In Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems ICECCS Vol. 2018-December (pp. 180-184). doi:10.1109/ICECCS2018.2018.00027
    Conference publication. .
  • Ho, H. -M. (2018). Revisiting Timed Logics with Automata Modalities. Retrieved from http://arxiv.org/abs/1812.10146v1
    Preprint.
  • Ho, H. -M., Zhou, R., & Jones, T. M. (2018). On Verifying Timed Hyperproperties. Retrieved from http://arxiv.org/abs/1812.10005v1
    Preprint.
  • Ho, H. -M., Ouaknine, J., & Worrell, J. (2018). On the Expressiveness and Monitoring of Metric Temporal Logic. Retrieved from http://dx.doi.org/10.23638/LMCS-15(2:13)2019
    Preprint.

2017

  • Brihaye, T., Geeraerts, G., Ho, H. M., & Monmege, B. (2017). Timed-automata-based verification of MITL over signals. In Leibniz International Proceedings in Informatics Lipics Vol. 90. doi:10.4230/LIPIcs.TIME.2017.7
    Conference publication. .
  • Brihaye, T., Geeraerts, G., Ho, H. M., & Monmege, B. (2017). Mightyl: A compositional translation from mitl to timed automata. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 10426 LNCS (pp. 421-440). doi:10.1007/978-3-319-63387-9_21
    Conference publication. .

2016

  • Brihaye, T., Estiévenart, M., Geeraerts, G., Ho, H. -M., Monmege, B., & Sznajder, N. (2016). Real-Time Synthesis is Hard!. Retrieved from http://arxiv.org/abs/1606.07124v1
    Preprint.
  • Brihaye, T., Estiévenart, M., Geeraerts, G., Ho, H. M., Monmege, B., & Sznajder, N. (2016). Real-time synthesis is hard!. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 9884 LNCS (pp. 105-120). doi:10.1007/978-3-319-44878-7_7
    Conference publication. .

2015

  • Ho, H. M., & Ouaknine, J. (2015). The cyclic-routing UAV problem is PSPACE-complete. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 9034 (pp. 328-342). doi:10.1007/978-3-662-46678-0_21
    Conference publication. .

2014

  • Ho, H. -M., & Ouaknine, J. (2014). The Cyclic-Routing UAV Problem is PSPACE-Complete. Retrieved from http://arxiv.org/abs/1411.2874v2
    Preprint.
  • Ho, H. M., Ouaknine, J., & Worrell, J. (2014). Online monitoring of metric temporal logic. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 8734 LNCS (pp. 178-192). doi:10.1007/2F978-3-319-11164-3_15
    Conference publication. .
  • Ho, H. M. (2014). On the expressiveness of metric temporal logic over bounded timed words. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 8762, 138-150. doi:10.1007/978-3-319-11439-2_11
    Article. .
  • Ho, H. M., Ouaknine, J., & Worrell, J. (2014). Online monitoring of metric temporal logic*. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 8734, 178-192. doi:10.1007/978-3-319-11164-3_15
    Article. .

Unpublished works

  • Ho, H. -M., Krishna, S. N., Madnani, K., Majumdar, R., & Pandya, P. (2026, April 11). MightyPPL: Model Checking MITL with Past and Pnueli Modalities. In 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026) (pp. pages). Turin, Italy.
    Conference publication. .