A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. - Tom van Dijk; Ernst Moritz Hahn; David N. Jansen; Yong Li 031; Thomas Neele; Mariëlle Stoelinga; Andrea Turrini; Lijun Zhang 001 (SETTA, 2015)

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. - Yong Li 031; Wanwei Liu; Andrea Turrini; Ernst Moritz Hahn; Lijun Zhang 001 (SETTA, 2016)

Verify LTL with Fairness Assumptions Efficiently. - Yong Li 031; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (TIME, 2016)

Advanced automata-based algorithms for program termination checking. - Yu-Fang Chen 001; Matthias Heizmann; Ondrej Lengál; Yong Li 031; Ming-Hsien Tsai 001; Andrea Turrini; Lijun Zhang 001 (PLDI, 2018)

Learning Büchi Automata and Its Applications. - Yong Li 031; Andrea Turrini; Yu-Fang Chen 001; Lijun Zhang 001 (SETSS, 2018)

Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). - Matthias Heizmann; Yu-Fang Chen 001; Daniel Dietsch; Marius Greitschus; Jochen Hoenicke; Yong Li 031; Alexander Nutz; Betim Musa; Christian Schilling 001; Tanja Schindler; Andreas Podelski (TACAS (2), 2018)

Learning to Complement Büchi Automata. - Yong Li 031; Andrea Turrini; Lijun Zhang 001; Sven Schewe (VMCAI, 2018)

Synthesizing Nested Ranking Functions for Loop Programs via SVM. - Yi Li; Xuechao Sun; Yong Li 031; Andrea Turrini; Lijun Zhang 001 (ICFEM, 2019)

ROLL 1.0: omega -Regular Language Learning Library. - Yong Li 031; Xuechao Sun; Andrea Turrini; Yu-Fang Chen 001; Junnan Xu (TACAS (1), 2019)

A Noise-Sensitivity-Analysis-Based Test Prioritization Technique for Deep Neural Networks. - Long Zhang; Xuechao Sun; Yong Li 031; Zhenyu Zhang 004 (CoRR, 2019)

Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. - Suguman Bansal; Yong Li 031; Lucas M. Tabajara; Moshe Y. Vardi (AAAI, 2020)

Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling. - Yong Li 031; Andrea Turrini; Xuechao Sun; Lijun Zhang 001 (ATVA, 2020)

Modelling and Implementation of Unmanned Aircraft Collision Avoidance. - Weizhi Feng; Cheng-Chao Huang; Andrea Turrini; Yong Li 031 (SETTA, 2020)

SVMRanker: a general termination analysis framework of loop programs via SVM. - Xie Li; Yi Li; Yong Li 031; Xuechao Sun; Andrea Turrini; Lijun Zhang 001 (ESEC/SIGSOFT FSE, 2020)

On the Power of Unambiguity in Büchi Complementation. - Yong Li 031; Moshe Y. Vardi; Lijun Zhang 001 (GandALF, 2020)

Congruence Relations for Büchi Automata. - Yong Li 031; Yih-Kuen Tsay; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (FM, 2021)

Synthesizing Good-Enough Strategies for LTLf Specifications. - Yong Li 031; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (IJCAI, 2021)

Congruence Relations for Büchi Automata. - Yong Li 031; Yih-Kuen Tsay; Moshe Y. Vardi (CoRR, 2021)

A novel learning algorithm for Büchi automata based on family of DFAs and classification trees. - Yong Li 031; Yu-Fang Chen 001; Lijun Zhang 001; Depeng Liu (Inf. Comput., 2021)

Towards a Grand Unification of Büchi Complementation Constructions. - Moshe Y. Vardi; Seth Fogarty; Yong Li 031; Yih-Kuen Tsay (Principles of Systems Design, 2022)

Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (CAV (2), 2022)

CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper). - Shizhen Yu; Yifan Dong; Jiuyang Liu; Yong Li 031; Zhilin Wu; David N. Jansen; Lijun Zhang 001 (SEFM, 2022)

EPMC Gets Knowledge in Multi-agent Systems. - Chen Fu; Ernst Moritz Hahn; Yong Li 031; Sven Schewe; Meng Sun 002; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2022)

Compositional Safety LTL Synthesis. - Suguman Bansal; Giuseppe De Giacomo; Antonio Di Stasio 001; Yong Li 031; Moshe Y. Vardi; Shufang Zhu 001 (VSTTE, 2022)

Synthesizing ranking functions for loop programs via SVM. - Yi Li; Xie Li; Yong Li 031; Xuechao Sun; Andrea Turrini; Lijun Zhang 001 (Theor. Comput. Sci., 2022)

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition". - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (Zenodo, 2022)

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition". - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (Zenodo, 2022)

Model Checking Strategies from Synthesis over Finite Traces. - Suguman Bansal; Yong Li 031; Lucas M. Tabajara; Moshe Y. Vardi; Andrew M. Wells (ATVA (1), 2023)

A Novel Family of Finite Automata for Recognizing and Learning ømega-Regular Languages. - Yong Li 031; Sven Schewe; Qiyi Tang 001 (ATVA (1), 2023)

Modular Mix-and-Match Complementation of Büchi Automata. - Vojtech Havlena; Ondrej Lengál; Yong Li 031; Barbora Smahlíková; Andrea Turrini (TACAS (1), 2023)

Modular Mix-and-Match Complementation of Büchi Automata (Technical Report). - Vojtech Havlena; Ondrej Lengál; Yong Li 031; Barbora Smahlíková; Andrea Turrini (CoRR, 2023)

On Strategies in Synthesis Over Finite Traces. - Suguman Bansal; Yong Li 031; Lucas Martinelli Tabajara; Moshe Y. Vardi; Andrew M. Wells (CoRR, 2023)

A novel family of finite automata for recognizing and learning ω-regular languages. - Yong Li 031; Sven Schewe; Qiyi Tang 001 (CoRR, 2023)

Quantitative controller synthesis for consumption Markov decision processes. - Jianling Fu; Cheng-Chao Huang; Yong Li 031; Jingyi Mei; Ming Xu 010; Lijun Zhang 001 (Inf. Process. Lett., 2023)

On the power of finite ambiguity in Büchi complementation. - Weizhi Feng; Yong Li 031; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (Inf. Comput., 2023)

DFAMiner: Mining Minimal Separating DFAs from Labelled Samples. - Daniele Dell'Erba; Yong Li 031; Sven Schewe (FM (2), 2024)

DAG-Based Compositional Approaches for LTLf to DFA Conversions. - Suguman Bansal; Yash Kankariya; Yong Li 031 (FMCAD, 2024)

Angluin-Style Learning of Deterministic Büchi and Co-Büchi Automata. - Yong Li 031; Sven Schewe; Qiyi Tang 001 (IJCAI, 2024)

Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata. - Yong Li 031; Sven Schewe; Moshe Y. Vardi (Theor. Comput. Sci., 2024)

Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata. - Yong Li 031; Soumyajit Paul; Sven Schewe; Qiyi Tang 001 (CAV (2), 2025)

Saturation Problems for Families of Automata. - León Bohn; Yong Li 031; Christof Löding; Sven Schewe (ICALP, 2025)

Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty. - Pian Yu; Yong Li 031; David Parker 001; Marta Kwiatkowska (CoRR, 2025)

Solving MDPs with LTLf+ and PPLTL+ Temporal Objectives. - Giuseppe De Giacomo; Yong Li 031; Sven Schewe; Christoph Weinhuber; Pian Yu (CoRR, 2025)

Efficient Learning of Weak Deterministic Büchi Automata. - Mona Alluwayma; Yong Li 031; Sven Schewe; Qiyi Tang 001 (CoRR, 2025)