Foundations of Software Systems (FoSS)

Hsi-Ming Ho

Selected Publications

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

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

2021

  • Arif, M., Zhou, R., Ho, H. -M., & Jones, T. M. (2021, February 27). 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.

2020

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

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. 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. (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.
  • 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:1-13:52. doi:10.23638/LMCS-15(2:13)2019
    Article. View online.

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

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

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

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

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