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. .

