I am an Associate Research Professor at the Institute of Software, Chinese Academy of Sciences (ISCAS), Beijing, China.

Research Interests

My research interests lie in formal methods, with a focus on applying formal methods and AI techniques to intelligent Cyber-Physical Systems (CPS) that underpin our daily lives to ensure their functionality, robustness, reliability, safety, security, etc.

Formal methods offer a mathematically interpretive and rigorous approach to modeling, analyzing, monitoring, and verifying CPS. However, the high complexity and undecidability can pose significant challenges in solving complicated problems effectively and efficiently. On the other hand, AI techniques, such as machine learning, have demonstrated effectiveness in various practical applications, but often lack interpretability and guarantees. Consequently, finding ways to combine lightweight formal methods and interpretable AI to address CPS-related problems presents an exciting research area, but one that requires balancing the trade-off between exactness and effectiveness.

The current research topics of our group include but are not limited to

• Formal Methods + Artificial Intelligence: AI for FM, FM for AI

• Model Learning & System Identification

• Modeling · Monitoring · Falsification · Verification · Synthesis of Real-time Systems, Embedded Systems, and CPS

• Program Verification and Synthesis

Recent Selected Publications

The papers and slides available on this webpage are provided for educational and research purposes only. They are intended solely for academic use and to facilitate the dissemination of knowledge in the respective fields. The copyrights of these papers and slides belong to their respective authors or publishers. More publication information can be found here.

• Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan (2026)
  Quantifier Elimination Meets Treewidth
  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026).
  To appear   arXiv

• Shenghua Feng, Jie An, Fanjiang Xu (2026)
  Runtime Safety and Reach-Avoid Prediction of Stochastic Systems with Observation-Aware Barrier Functions
  Annual AAAI Conference on Artificial Intelligence (AAAI 2026).
  To appear   arXiv

• Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen, Naijun Zhan (2026)
  RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation
  Annual AAAI Conference on Artificial Intelligence (AAAI 2026).
  To appear   arXiv

• Xiaochen Tang, Zhenya Zhang, Miaomiao Zhang, Jie An (2025)
  Control Synthesis of Cyber-Physical Systems for Real-Time Specifications through Causation-Guided Reinforcement Learning
  IEEE Real-Time Systems Symposium (RTSS 2025), pages 324-337.
  paper   arXiv   (🎖️ Artifact Evaluated)

• Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang, Zhenya Zhang (2025)
  On Synthesis of Timed Regular Expressions
  IEEE Real-Time Systems Symposium (RTSS 2025), pages 311-323.
  paper   arXiv

• ​Hiroya Fujinami, Masaki Waga, Jie An, Kohei Suenaga, Nayuta Yanagisawa, Hiroki Iseri, Ichiro Hasuo (2025)
  Componentwise Automata Learning for System Integration
  International Symposium on Automated Technology for Verification and Analysis (ATVA 2025), pages 3-26.
  paper   arXiv   (🎖️ Artifact Evaluated)   (🥇 Distinguished Paper Award)

• Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen, Naijun Zhan (2025)
  Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge
  The Annual Meeting of the Association for Computational Linguistics (ACL 2025), pages 10446-10458.
  paper   arXiv

• Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo (2024)
  CauMon: An Informative Online Monitor for Signal Temporal Logic
  International Symposium on Formal Methods (FM 2024), Part II, pages 286-304.
  paper   code   (🎖️ Artifact Evaluated)

• Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan, Ichiro Hasuo (2024)
  The Opacity of Timed Automata
  International Symposium on Formal Methods (FM 2024), Part I, pages 620-637.
  paper   slides

• Sota Sato, Jie An, Zhenya Zhang, Ichiro Hasuo (2024)
  Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
  International Conference on Computer Aided Verification (CAV 2024), Part III, pages 282-306.
  paper   arXiv   slides   (🎖️ Artifact Evaluated)

• Yu Teng, Miaomiao Zhang, Jie An (2024)
  Learning Deterministic Multi-Clock Timed Automata
  International Conference on Hybrid Systems: Control and Computation (HSCC 2024), pages 6:1-6:11.
  paper   arXiv

• Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo (2023)
  Online Causation Monitoring of Signal Temporal Logic
  International Conference on Computer Aided Verification (CAV 2023), Part I, pages 62-84.
  paper   arXiv   slides   code   (🎖️ Artifact Evaluated)

Projects

• NSFC Excellent Young Scientists Fund Program (Overseas), 2024 - 2028.
• CAS Pioneer Hundred Talents Program, 2024 - 2029.
• "Model Learning for Intelligent Cyber-Physical Systems", a key project of ISCAS Basic Research Program, 2024 - 2026.

Contact

Email
anjie[@]iscas[DOT]ac[DOT]cn

Office
Room B202, Building 5
Institute of Software, Chinese Academy of Sciences
No. 4, South Fourth Street, Zhong Guan Cun, Beijing, 100190, China