Publications
2025
DFAMiner: Mining Minimal Separating DFAs from Labelled Samples
Dell’Erba, D., Li, Y., & Schewe, S. (2025). DFAMiner: Mining Minimal Separating DFAs from Labelled Samples. In Lecture Notes in Computer Science (pp. 48-66). Springer Nature Switzerland. doi:10.1007/978-3-031-71177-0_4
2024
Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata
Li, Y., Schewe, S., & Vardi, M. Y. (2024). Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. Theoretical Computer Science, 114650. doi:10.1016/j.tcs.2024.114650
Angluin-Style Learning of Deterministic Büchi and Co-Büchi Automata
Li, Y., Schewe, S., & Tang, Q. (2024). Angluin-Style Learning of Deterministic Büchi and Co-Büchi Automata. In Proceedings of the Thirty-ThirdInternational Joint Conference on Artificial Intelligence (pp. 4506-4514). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2024/498
2023
On the power of finite ambiguity in Büchi complementation
Feng, W., Li, Y., Turrini, A., Vardi, M. Y., & Zhang, L. (2023). On the power of finite ambiguity in Büchi complementation. Information and Computation, 292, 105032. doi:10.1016/j.ic.2023.105032
A Novel Family of Finite Automata for Recognizing and Learning $$\omega $$-Regular Languages
Li, Y., Schewe, S., & Tang, Q. (2023). A Novel Family of Finite Automata for Recognizing and Learning $$\omega $$-Regular Languages. In Lecture Notes in Computer Science (pp. 53-73). Springer Nature Switzerland. doi:10.1007/978-3-031-45329-8_3
Model Checking Strategies from Synthesis over Finite Traces
Bansal, S., Li, Y., Tabajara, L. M., Vardi, M. Y., & Wells, A. (2023). Model Checking Strategies from Synthesis over Finite Traces. In Lecture Notes in Computer Science (pp. 227-247). Springer Nature Switzerland. doi:10.1007/978-3-031-45329-8_11
Modular Mix-and-Match Complementation of Büchi Automata
Havlena, V., Lengál, O., Li, Y., Šmahlíková, B., & Turrini, A. (2023). Modular Mix-and-Match Complementation of Büchi Automata. In Lecture Notes in Computer Science (pp. 249-270). Springer Nature Switzerland. doi:10.1007/978-3-031-30823-9_13
2022
EPMC Gets Knowledge in Multi-Agent Systems
Fu, C., Hahn, E. -M., Li, Y., Schewe, S., Sun, M., Turrini, A., & Zhang, L. (2022). EPMC Gets Knowledge in Multi-Agent Systems. In International Conference on Verification, Model Checking, and Abstract Interpretation.
CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper)
Yu, S., Dong, Y., Liu, J., Li, Y., Wu, Z., Jansen, D. N., & Zhang, L. (2022). CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). In Unknown Book (Vol. 13550, pp. 324-331). doi:10.1007/978-3-031-17108-6_20
Divide-and-Conquer Determinization of Buchi Automata Based on SCC Decomposition
Li, Y., Turrini, A., Feng, W., Vardi, M. Y., & Zhang, L. (2022). Divide-and-Conquer Determinization of Buchi Automata Based on SCC Decomposition. In Unknown Book (Vol. 13372, pp. 152-173). doi:10.1007/978-3-031-13188-2_8
Towards a Grand Unification of Büchi Complementation Constructions
Vardi, M. Y., Fogarty, S., Li, Y., & Tsay, Y. -K. (2022). Towards a Grand Unification of Büchi Complementation Constructions. In Lecture Notes in Computer Science (pp. 185-207). Springer Nature Switzerland. doi:10.1007/978-3-031-22337-2_9
2021
A novel learning algorithm for Buchi automata based on family of DFAs and classification trees
Li, Y., Chen, Y. -F., Zhang, L., & Liu, D. (2021). A novel learning algorithm for Buchi automata based on family of DFAs and classification trees. INFORMATION AND COMPUTATION, 281. doi:10.1016/j.ic.2020.104678
Congruence Relations for Buchi Automata
Li, Y., Tsay, Y. -K., Turrini, A., Vardi, M. Y., & Zhang, L. (2021). Congruence Relations for Buchi Automata. In Unknown Book (Vol. 13047, pp. 465-482). doi:10.1007/978-3-030-90870-6_25
Synthesizing Good-Enough Strategies for LTLf Specifications
Li, Y., Turrini, A., Vardi, M. Y., & Zhang, L. (2021). Synthesizing Good-Enough Strategies for LTLf Specifications. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (pp. 4144-4151). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2021/570
2020
SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM
Li, X., Li, Y., Li, Y., Sun, X., Turrini, A., & Zhang, L. (2020). SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM. In PROCEEDINGS OF THE 28TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (ESEC/FSE '20) (pp. 1635-1639). doi:10.1145/3368089.3417930
On the Power of Unambiguity in Büchi Complementation
Li, Y., Vardi, M. Y., & Zhang, L. (n.d.). On the Power of Unambiguity in Büchi Complementation. Electronic Proceedings in Theoretical Computer Science, 326, 182-198. doi:10.4204/eptcs.326.12
Modelling and Implementation of Unmanned Aircraft Collision Avoidance
Feng, W., Huang, C. -C., Turrini, A., & Li, Y. (2020). Modelling and Implementation of Unmanned Aircraft Collision Avoidance. In Lecture Notes in Computer Science (pp. 52-69). Springer International Publishing. doi:10.1007/978-3-030-62822-2_4
Proving Non-inclusion of Buchi Automata Based on Monte Carlo Sampling
Li, Y., Turrini, A., Sun, X., & Zhang, L. (2020). Proving Non-inclusion of Buchi Automata Based on Monte Carlo Sampling. In Unknown Book (Vol. 12302, pp. 467-483). doi:10.1007/978-3-030-59152-6_26
2019
Learning Büchi Automata and Its Applications
Li, Y., Turrini, A., Chen, Y. -F., & Zhang, L. (2019). Learning Büchi Automata and Its Applications. In Lecture Notes in Computer Science (pp. 38-98). Springer International Publishing. doi:10.1007/978-3-030-17601-3_2
ROLL 1.0: ω-Regular Language Learning Library
Li, Y., Sun, X., Turrini, A., Chen, Y. -F., & Xu, J. (2019). ROLL 1.0: ω-Regular Language Learning Library. In Unknown Book (Vol. 11427, pp. 365-371). doi:10.1007/978-3-030-17462-0_23
Synthesizing Nested Ranking Functions for Loop Programs via SVM
Li, Y., Sun, X., Li, Y., Turrini, A., & Zhang, L. (2019). Synthesizing Nested Ranking Functions for Loop Programs via SVM. In Lecture Notes in Computer Science (pp. 438-454). Springer International Publishing. doi:10.1007/978-3-030-32409-4_27
2018
Advanced Automata-Based Algorithms for Program Termination Checking
Chen, Y. -F., Heizmann, M., Lengal, O., Li, Y., Tsai, M. -H., Turrini, A., & Zhang, L. (2018). Advanced Automata-Based Algorithms for Program Termination Checking. In ACM SIGPLAN NOTICES Vol. 53 (pp. 135-150). doi:10.1145/3192366.3192405
Learning to Complement Buchi Automata
Li, Y., Turrini, A., Zhang, L., & Schewe, S. (2018). Learning to Complement Buchi Automata. In VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2018) Vol. 10747 (pp. 313-335). doi:10.1007/978-3-319-73721-8_15
Ultimate Automizer and the Search for Perfect Interpolants
Heizmann, M., Chen, Y. -F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., . . . Podelski, A. (2018). Ultimate Automizer and the Search for Perfect Interpolants. In Unknown Book (Vol. 10806, pp. 447-451). doi:10.1007/978-3-319-89963-3_30
2017
A Novel Learning Algorithm for Buchi Automata Based on Family of DFAs and Classification Trees
Li, Y., Chen, Y. -F., Zhang, L., & Liu, D. (2017). A Novel Learning Algorithm for Buchi Automata Based on Family of DFAs and Classification Trees. In TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT I Vol. 10205 (pp. 208-226). doi:10.1007/978-3-662-54577-5_12
2016
Verify LTL with Fairness Assumptions Efficiently
Li, Y., Song, L., Feng, Y., & Zhang, L. (2016). Verify LTL with Fairness Assumptions Efficiently. In PROCEEDINGS 23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING - TIME 2016 (pp. 41-50). doi:10.1109/TIME.2016.12
An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties
Li, Y., Liu, W., Turrini, A., Hahn, E. M., & Zhang, L. (2016). An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. In DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS Vol. 9984 (pp. 280-296). doi:10.1007/978-3-319-47677-3_18
2015
A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking
van Dijk, T., Hahn, E. M., Jansen, D. N., Li, Y., Neele, T., Stoelinga, M., . . . Zhang, L. (2015). A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015 Vol. 9409 (pp. 35-51). doi:10.1007/978-3-319-25942-0_3