Hsi-Ming Ho : Publications : Foundations of Software Systems (FoSS) : University of Sussex

Selected Publications

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. View on figshare.
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. View on figshare.

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. View on figshare.
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. View online.

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. View on figshare.

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. View on figshare.

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

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. View online.
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. View online.
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. View on figshare.
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. View online.

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

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

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

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

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

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. View on figshare.