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.
DBLP Google Scholar
2025
-
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).
To appear -
Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan, Miaomiao Zhang (2025)
Efficient Decomposition Identification of Deterministic Finite Automata from Examples
International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2025).
To appear -
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).
To apper -
Chengzi Huang, Behnam Khodabandeloo, Duc Anh Nguyen, Wang Yi, Jie An and Zhenya Zhang (2025)
Causality Monitoring for MIMOS
Principles of Formal Quantitative Analysis -- Essays dedicated to Christel Baier on the occasion of her 60th birthday (PFQA-Baier60).
To apper -
Yu Teng, Hanyue Chen, Junri Mi, Miaomiao Zhang and Jie An (2025)
Active Learning of Deterministic Timed Automata via Timed Classification Tree
SCIENCE CHINA Information Sciences (SCIS).
To apper
2024
-
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), pages 286-304.
paper code bibtex (🎖️ Artifact Evaluated)
@inproceedings{ZhangAAH24, author = {Zhenya Zhang and Jie An and Paolo Arcaini and Ichiro Hasuo}, editor = {Andre Platzer and Kristin Yvonne Rozier and Matteo Pradella and Matteo Rossi}, title = {CauMon: An Informative Online Monitor for Signal Temporal Logic}, booktitle = {Formal Methods - 26th International Symposium, {FM} 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part {II}}, series = {Lecture Notes in Computer Science}, volume = {14934}, pages = {286--304}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-71177-0\_18}, doi = {10.1007/978-3-031-71177-0\_18} } -
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 bibtex
@inproceedings{AnGWZH24, author = {Jie An and Qiang Gao and Lingtai Wang and Naijun Zhan and Ichiro Hasuo}, editor = {Andr{\'{e}} Platzer and Kristin Yvonne Rozier and Matteo Pradella and Matteo Rossi}, title = {The Opacity of Timed Automata}, booktitle = {Formal Methods - 26th International Symposium, {FM} 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {14933}, pages = {620--637}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-71162-6\_32}, doi = {10.1007/978-3-031-71162-6\_32} } -
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 bibtex (🎖️ Artifact Evaluated)
@inproceedings{SatoAZH24, author = {Sota Sato and Jie An and Zhenya Zhang and Ichiro Hasuo}, editor = {Arie Gurfinkel and Vijay Ganesh}, title = {Optimization-Based Model Checking and Trace Synthesis for Complex {STL} Specifications}, booktitle = {Computer Aided Verification - 36th International Conference, {CAV} 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part {III}}, series = {Lecture Notes in Computer Science}, volume = {14683}, pages = {282--306}, publisher = {Springer}, year = {2024}, url = {https://doi.org/10.1007/978-3-031-65633-0\_13}, doi = {10.1007/978-3-031-65633-0\_13}, timestamp = {Fri, 02 Aug 2024 12:00:01 +0200}, biburl = {https://dblp.org/rec/conf/cav/SatoAZH24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } -
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 bibtex
@inproceedings{TengZ024, author = {Yu Teng and Miaomiao Zhang and Jie An}, editor = {Erika {\'{A}}brah{\'{a}}m and Manuel Mazo Jr.}, title = {Learning Deterministic Multi-Clock Timed Automata}, booktitle = {Proceedings of the 27th {ACM} International Conference on Hybrid Systems: Computation and Control, {HSCC} 2024, Hong Kong SAR, China, May 14-16, 2024}, pages = {6:1--6:11}, publisher = {{ACM}}, year = {2024}, url = {https://doi.org/10.1145/3641513.3650124}, doi = {10.1145/3641513.3650124} }
2023
- Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo
Online Causation Monitoring of Signal Temporal Logic
International Conference on Computer Aided Verification (CAV 2023), Part I, pages 62-84.
paper arXiv slides code bibtex (🎖️ Artifact Evaluated)
@inproceedings{ZhangAAH23, author = {Zhenya Zhang and Jie An and Paolo Arcaini and Ichiro Hasuo}, editor = {Constantin Enea and Akash Lal}, title = {Online Causation Monitoring of Signal Temporal Logic}, booktitle = {Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {13964}, pages = {62--84}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-37706-8\_4}, doi = {10.1007/978-3-031-37706-8\_4} }
2022
-
Runqing Xu, Jie An, Bohua Zhan
Active learning of One-Clock Timed Automata using Constraint Solving
International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pages 249-265.
paper arXiv slides code bibtex
@inproceedings{XuAZ22, author = {Runqing Xu and Jie An and Bohua Zhan}, editor = {Ahmed Bouajjani and Luk{\'{a}}s Hol{\'{\i}}k and Zhilin Wu}, title = {Active Learning of One-Clock Timed Automata Using Constraint Solving}, booktitle = {Automated Technology for Verification and Analysis - 20th International Symposium, {ATVA} 2022, Virtual Event, October 25-28, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13505}, pages = {249--265}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-19992-9\_16}, doi = {10.1007/978-3-031-19992-9\_16} } -
Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, Naijun Zhan
Learning Deterministic One-Clock Timed Automata via Mutation Testing
International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pages 233-248.
paper bibtex
@inproceedings{TangSZAZZ22, author = {Xiaochen Tang and Wei Shen and Miaomiao Zhang and Jie An and Bohua Zhan and Naijun Zhan}, editor = {Ahmed Bouajjani and Luk{\'{a}}s Hol{\'{\i}}k and Zhilin Wu}, title = {Learning Deterministic One-Clock Timed Automata via Mutation Testing}, booktitle = {Automated Technology for Verification and Analysis - 20th International Symposium, {ATVA} 2022, Virtual Event, October 25-28, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13505}, pages = {233--248}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-19992-9\_15}, doi = {10.1007/978-3-031-19992-9\_15} } -
Junri Mi, Miaomiao Zhang, Jie An, Bowen Du
Learning Deterministic One-clock Timed Automata Based on Timed Classification Tree
Journal of Software, 33(8): 2797-2814.
bibtex
@article{20222797, author = {Junri Mi and Miaomiao Zhang and Jie An and Bowen Du}, title = {Learning Deterministic One-clock Timed Automata Based on Timed Classification Tree}, journal = {Journal of Software}, volume = {33}, number = {8}, pages = {2797--2814}, year = {2022}, doi = {10.13328/j.cnki.jos.006599} }
2021
-
Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning Nondeterministic Real-Time Automata
ACM Transactions on Embedded Computing Systems (ACM TECS), 20(5s): 99:1-99:26. (A special issue of EMSOFT 2021).
paper slides bibtex
@article{AnZZZ21, author = {Jie An and Bohua Zhan and Naijun Zhan and Miaomiao Zhang}, title = {Learning Nondeterministic Real-Time Automata}, journal = {{ACM} Trans. Embed. Comput. Syst.}, volume = {20}, number = {5s}, pages = {99:1--99:26}, year = {2021}, url = {https://doi.org/10.1145/3477030}, doi = {10.1145/3477030} } -
Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Inferring Switched Nonlinear Dynamical Systems
Formal Aspects of Computing (FAC). 33(3):385-406.
paper bibtex
@article{JinAZZZ21, author = {Xiangyu Jin and Jie An and Bohua Zhan and Naijun Zhan and Miaomiao Zhang}, title = {Inferring Switched Nonlinear Dynamical Systems}, journal = {Formal Aspects Comput.}, volume = {33}, number = {3}, pages = {385--406}, year = {2021}, url = {https://doi.org/10.1007/s00165-021-00542-7}, doi = {10.1007/s00165-021-00542-7} } -
Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning Real-Time Automata
SCIENCE CHINA Information Sciences (SCIS), 64(9): 192103:1-192103:17.
paper bibtex
@article{AnWZZZ21, author = {Jie An and Lingtai Wang and Bohua Zhan and Naijun Zhan and Miaomiao Zhang}, title = {Learning real-time automata}, journal = {SCIENCE CHINA Information Sciences}, volume = {64}, number = {9}, year = {2021}, url = {https://doi.org/10.1007/s11432-019-2767-4}, doi = {10.1007/s11432-019-2767-4} }
2020
-
Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, Naijun Zhan
PAC Learning of Deterministic One-Clock Timed Automata
International Conference on Formal Engineering Methods (ICFEM 2020), pages 129-146.
paper bibtex
@inproceedings{ShenAZZ0Z20, author = {Wei Shen and Jie An and Bohua Zhan and Miaomiao Zhang and Bai Xue and Naijun Zhan}, editor = {Shang{-}Wei Lin and Zhe Hou and Brendan P. Mahony}, title = {{PAC} Learning of Deterministic One-Clock Timed Automata}, booktitle = {Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, {ICFEM} 2020, Singapore, Singapore, March 1-3, 2021, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {12531}, pages = {129--146}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-63406-3\_8}, doi = {10.1007/978-3-030-63406-3\_8} } -
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
Learning One-Clock Timed Automata
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), pages 444-462.
paper arXiv slides code bibtex (🎖️ Artifact Evaluated) (🥇 FMAC 2019 Best Paper Award) (🏵 Springer High-Impact Paper)
@inproceedings{AnCZZZ20, author = {Jie An and Mingshuai Chen and Bohua Zhan and Naijun Zhan and Miaomiao Zhang}, editor = {Armin Biere and David Parker}, title = {Learning One-Clock Timed Automata}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, {TACAS} 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {12078}, pages = {444--462}, publisher = {Springer}, year = {2020}, url = {https://doi.org/10.1007/978-3-030-45190-5\_25}, doi = {10.1007/978-3-030-45190-5\_25} } -
Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, and Ting Gan
From model to implementation: A network-algorithm programming language
SCIENCE CHINA Information Sciences (SCIS), 63(7): 172102:1-172102:17.
paper bibtex
@article{WangACZWZG20, author = {Jian Wang and Jie An and Mingshuai Chen and Naijun Zhan and Lulin Wang and Miaomiao Zhang and Ting Gan}, title = {From model to implementation: a network algorithm programming language}, journal = {SCIENCE CHINA Information Sciences}, volume = {63}, number = {7}, year = {2020}, url = {https://doi.org/10.1007/s11432-019-2644-8}, doi = {10.1007/s11432-019-2644-8} }
2019
-
Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, Naijun Zhan
NIL: Learning Nonlinear Interpolants
International Conference on Automated Deduction (CADE-27), pages 178-196.
paper arXiv slides code bibtex
@inproceedings{ChenWAZKZ19, author = {Mingshuai Chen and Jian Wang and Jie An and Bohua Zhan and Deepak Kapur and Naijun Zhan}, editor = {Pascal Fontaine}, title = {{NIL:} Learning Nonlinear Interpolants}, booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11716}, pages = {178--196}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-29436-6\_11}, doi = {10.1007/978-3-030-29436-6\_11} } -
Xiaoxue Hou, Jie An, Miaomiao Zhang, Bowen Du, Jing Liu
High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training
International Conference on Tools with Artificial Intelligence (ICTAI 2019), pages 840-847.
paper bibtex
@inproceedings{HouAZDL19, author = {Xiaoxue Hou and Jie An and Miaomiao Zhang and Bowen Du and Jing Liu}, title = {High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training}, booktitle = {31st {IEEE} International Conference on Tools with Artificial Intelligence, {ICTAI} 2019, Portland, OR, USA, November 4-6, 2019}, pages = {840--847}, publisher = {{IEEE}}, year = {2019}, url = {https://doi.org/10.1109/ICTAI.2019.00120}, doi = {10.1109/ICTAI.2019.00120} } -
Jie An, Miaomiao Zhang
Verifying Continuous-time Duration Calculus against Real-time Automaton
Journal of Software, 30(7): 1953-1965.
bibtex
@article{20191953, author = {Jie An and Miaomiao Zhang}, title = {Verifying Continuous-time Duration Calculus against Real-time Automaton}, journal = {Journal of Software}, volume = {30}, number = {7}, pages = {1953--1965}, year = {2019}, doi = {10.13328/j.cnki.jos.005752} }
2018
-
Lingtai Wang, Naijun Zhan, Jie An
The Opacity of Real-Time Automata
IEEE Transactions on CAD of Integrated Circuits and Systems (IEEE TCAD), 37(11):2845-2856. (A special issue of EMSOFT 2018)
paper slides bibtex
@article{WangZA18, author = {Lingtai Wang and Naijun Zhan and Jie An}, title = {The Opacity of Real-Time Automata}, journal = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.}, volume = {37}, number = {11}, pages = {2845--2856}, year = {2018}, url = {https://doi.org/10.1109/TCAD.2018.2857363}, doi = {10.1109/TCAD.2018.2857363} } -
Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, Wang Yi
Model Checking Bounded Continuous-time Extended Linear Duration Invariants
International Conference on Hybrid Systems: Computation and Control (HSCC 2018), pages 81-90.
paper slides bibtex
@inproceedings{AnZLZY18, author = {Jie An and Naijun Zhan and Xiaoshan Li and Miaomiao Zhang and Wang Yi}, editor = {Maria Prandini and Jyotirmoy V. Deshmukh}, title = {Model Checking Bounded Continuous-time Extended Linear Duration Invariants}, booktitle = {Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of {CPS} Week), {HSCC} 2018, Porto, Portugal, April 11-13, 2018}, pages = {81--90}, publisher = {{ACM}}, year = {2018}, url = {https://doi.org/10.1145/3178126.3178147}, doi = {10.1145/3178126.3178147} }