Publications

2025

1. HSCC 2025

   

   Runtime Enforcement of CPS against Signal Temporal Logic

   Han Su, Saumya Shankar, Srinivas Pinisetty, Partha S. Roop, and Naijun Zhan

   In Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control, Irvine, CA, USA, 2025

   Best Paper Finalist DOI Bib PDF Artifact Evaluated Slides

   https://hscc.acm.org/2025/hscc-best-paper-award/

   Cyber-Physical Systems (CPSs), especially those involving autonomy, need guarantees of their safety. Runtime Enforcement (RE) is a lightweight method to formally ensure that some specified properties are satisfied over the executions of the system. Hence, there is recent interest in the RE of CPS. However, existing methods are not designed to tackle specifications suitable for the hybrid dynamics of CPS. With this in mind, we develop runtime enforcement of CPS using properties defined in Signal Temporal Logic (STL).In this work, we aim to construct a runtime enforcer for a given STL formula to minimally modify a signal to satisfy the formula. To achieve this, the STL formula to be enforced is first translated into a timed transducer, while the signal to be corrected is encoded as timed words. We provide timed transducers for the temporal operators until and release noting that other temporal operators can be expressed using these two. Our approach enables effective enforcement of STL properties for CPS. A case study is provided to illustrate the approach and generate empirical evidence of its suitability for CPS.

   @inproceedings{10.1145/3716863.3718052,
     author = {Su, Han and Shankar, Saumya and Pinisetty, Srinivas and Roop, Partha S. and Zhan, Naijun},
     title = {Runtime Enforcement of CPS against Signal Temporal Logic},
     year = {2025},
     isbn = {9798400715044},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     url = {https://doi.org/10.1145/3716863.3718052},
     booktitle = {Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control},
     articleno = {18},
     numpages = {11},
     keywords = {Reactive System, Runtime Enforcement, Signal Temporal Logic, Timed Automata, Timed Transducer},
     location = {Irvine, CA, USA},
     series = {HSCC '25},
     doi = {10.1145/3716863.3718052},
     artifact = {https://github.com/Han-SU/stl-enforcement-experiments}
   }

2024

1. FM 2024

   

   Switching Controller Synthesis for Hybrid Systems Against STL Formulas

   Han Su, Shenghua Feng, Sinong Zhan, and Naijun Zhan

   In International Symposium on Formal Methods, Milan, Italy, 2024

   DOI Bib PDF Slides

   Switching controllers play a pivotal role in directing hybrid systems (HSs) towards the desired objective, embodying a “correct-by-construction” approach to HS design. Identifying these objectives is thus crucial for the synthesis of effective switching controllers. While most of existing works focus on safety and liveness, few of them consider timing constraints. In this paper, we delves into the synthesis of switching controllers for HSs that meet system objectives given by a fragment of STL, which essentially corresponds to a reach-avoid problem with timing constraints. Our approach involves iteratively computing the state sets that can be driven to satisfy the reach-avoid specification with timing constraints. This technique supports to create switching controllers for both constant and non-constant HSs. We validate our method’s soundness, and confirm its relative completeness for a certain subclass of HSs. Experiment results affirms the efficacy of our approach.

   @inproceedings{10.1007/978-3-031-71177-0_15,
     author = {Su, Han and Feng, Shenghua and Zhan, Sinong and Zhan, Naijun},
     editor = {Platzer, Andre and Rozier, Kristin Yvonne and Pradella, Matteo and Rossi, Matteo},
     title = {Switching Controller Synthesis for Hybrid Systems Against STL Formulas},
     booktitle = {International Symposium on Formal Methods},
     year = {2024},
     location = {Milan, Italy},
     publisher = {Springer Nature Switzerland},
     address = {Cham},
     pages = {229--247},
     isbn = {978-3-031-71177-0},
     doi = {10.1007/978-3-031-71177-0_15},
   }

2. Reset controller synthesis: a correct-by-construction way to the design of CPS

   Naijun Zhan, Han Su, Mengfei Yang, and Bin Gu

   Research Directions: Cyber-Physical Systems, 2024

   DOI

2023

1. OOPSLA 2023

   

   Lower Bounds for Possibly Divergent Probabilistic Programs

   Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Naijun Zhan

   Proc. ACM Program. Lang., Apr 2023

   DOI PDF Slides

   We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs – as is the case for existing rules – and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.