Skip to content

profile_picture
Jie An · 安杰

       

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

Hiring

We are constantly looking for self-motivated Postdocs, Ph.D./Master Students, and Research Assistants/Interns to join our group at ISCAS. The excellent postdocs can be appointed as the Special Research Associates of the Chinese Academy of Sciences. If you are interested in our work and would like to join us, please do not hesitate to send me an email with or without your CV to start a conversation!

Also refer to my webpage at the University of Chinese Academy of Sciences: https://people.ucas.edu.cn/~anjie.

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