SAT-Based Explicit LTL Reasoning. - Jianwen Li; Shufang Zhu 001; Geguang Pu; Moshe Y. Vardi (Haifa Verification Conference, 2015)

Approximate Reachability. - Jianwen Li; Shufang Zhu 001; Yueling Zhang; Geguang Pu; Moshe Y. Vardi (CoRR, 2016)

A Symbolic Approach to Safety ltl Synthesis. - Shufang Zhu 001; Lucas M. Tabajara; Jianwen Li; Geguang Pu; Moshe Y. Vardi (Haifa Verification Conference, 2017)

Safety model checking with complementary approximations. - Jianwen Li; Shufang Zhu 001; Yueling Zhang; Geguang Pu; Moshe Y. Vardi (ICCAD, 2017)

Symbolic LTLf Synthesis. - Shufang Zhu 001; Lucas M. Tabajara; Jianwen Li; Geguang Pu; Moshe Y. Vardi (IJCAI, 2017)

An explicit transition system construction approach to LTL satisfiability checking. - Jianwen Li; Lijun Zhang 001; Shufang Zhu 001; Geguang Pu; Moshe Y. Vardi; Jifeng He 001 (Formal Aspects Comput., 2018)

First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation. - Shufang Zhu 001; Geguang Pu; Moshe Y. Vardi (TAMC, 2019)

First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation. - Shufang Zhu 001; Geguang Pu; Moshe Y. Vardi (CoRR, 2019)

SAT-based explicit LTL reasoning and its application to satisfiability checking. - Jianwen Li; Shufang Zhu 001; Geguang Pu; Lijun Zhang 001; Moshe Y. Vardi (Formal Methods Syst. Des., 2019)

LTLƒ Synthesis with Fairness and Stability Assumptions. - Shufang Zhu 001; Giuseppe De Giacomo; Geguang Pu; Moshe Y. Vardi (AAAI, 2020)

Two-Stage Technique for LTLf Synthesis Under LTL Assumptions. - Giuseppe De Giacomo; Antonio Di Stasio 001; Moshe Y. Vardi; Shufang Zhu 001 (KR, 2020)

On-the-fly Synthesis for LTL over Finite Traces. - Shengping Xiao; Jianwen Li; Shufang Zhu 001; Yingying Shi; Geguang Pu; Moshe Y. Vardi (AAAI, 2021)

Synthesis with Mandatory Stop Actions. - Giuseppe De Giacomo; Antonio Di Stasio 001; Giuseppe Perelli; Shufang Zhu 001 (KR, 2021)

On the Power of Automata Minimization in Temporal Synthesis. - Shufang Zhu 001; Lucas M. Tabajara; Geguang Pu; Moshe Y. Vardi (GandALF, 2021)

Synthesis of Maximally Permissive Strategies for LTLf Specifications. - Shufang Zhu 001; Giuseppe De Giacomo (IJCAI, 2022)

LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. - Giuseppe De Giacomo; Marco Favorito; Jianwen Li; Moshe Y. Vardi; Shengping Xiao; Shufang Zhu 001 (IJCAI, 2022)

Act for Your Duties but Maintain Your Rights. - Shufang Zhu 001; Giuseppe De Giacomo (KR, 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)

Finite-trace and generalized-reactivity specifications in temporal synthesis. - Giuseppe De Giacomo; Antonio Di Stasio 001; Lucas M. Tabajara; Moshe Y. Vardi; Shufang Zhu 001 (Formal Methods Syst. Des., 2022)

LTLf Best-Effort Synthesis in Nondeterministic Planning Domains. - Giuseppe De Giacomo; Gianmarco Parretti; Shufang Zhu 001 (ECAI, 2023)

sc ltlf Synthesis Under Environment Specifications for Reachability and Safety Properties. - Benjamin Aminof; Giuseppe De Giacomo; Antonio Di Stasio 001; Hugo Francon; Sasha Rubin; Shufang Zhu 001 (EUMAS, 2023)

Symbolic sc ltlf Best-Effort Synthesis. - Giuseppe De Giacomo; Gianmarco Parretti; Shufang Zhu 001 (EUMAS, 2023)

Symbolic LTLf Best-Effort Synthesis. - Giuseppe De Giacomo; Gianmarco Parretti; Shufang Zhu 001 (CoRR, 2023)

LTLf Best-Effort Synthesis in Nondeterministic Planning Domains. - Giuseppe De Giacomo; Gianmarco Parretti; Shufang Zhu 001 (CoRR, 2023)

Mimicking Behaviors in Separated Domains. - Giuseppe De Giacomo; Dror Fried; Fabio Patrizi; Shufang Zhu 001 (J. Artif. Intell. Res., 2023)

Mimicking Behaviors in Separated Domains (Abstract Reprint). - Giuseppe De Giacomo; Dror Fried; Fabio Patrizi; Shufang Zhu 001 (AAAI, 2024)

Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic. - Ben Greenman; Siddhartha Prasad; Antonio Di Stasio 001; Shufang Zhu 001; Giuseppe De Giacomo; Shriram Krishnamurthi; Marco Montali; Tim Nelson; Milda Zizyte (FM (1), 2024)

The Trembling-Hand Problem for LTLf Planning. - Pian Yu; Shufang Zhu 001; Giuseppe De Giacomo; Marta Kwiatkowska; Moshe Y. Vardi (IJCAI, 2024)

On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts. - Shengping Xiao; Yongkang Li; Shufang Zhu 001; Jun Sun 001; Jianwen Li; Geguang Pu; Moshe Y. Vardi (CoRR, 2024)

Learning to Coordinate without Communication under Incomplete Information. - Shenghui Chen; Shufang Zhu 001; Giuseppe De Giacomo; Ufuk Topcu (CoRR, 2024)

LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specifications. - Shufang Zhu 001; Marco Favorito (TACAS (1), 2025)

Engineering an LTLf Synthesis Tool. - Alexandre Duret-Lutz; Shufang Zhu 001; Nir Piterman; Giuseppe De Giacomo; Moshe Y. Vardi (CIAA, 2025)

LTLf synthesis under environment specifications for reachability and safety properties. - Benjamin Aminof; Giuseppe De Giacomo; Antonio Di Stasio 001; Hugo Francon; Sasha Rubin; Shufang Zhu 001 (Inf. Comput., 2025)

Symbolic ltlf Synthesis: A Unified Approach for Synthesizing Winning, Dominant, and Best-Effort Strategies. - Giuseppe De Giacomo; Gianmarco Parretti; Shufang Zhu 001 (SN Comput. Sci., 2025)

LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains. - Giuseppe De Giacomo; Gianmarco Parretti; Shufang Zhu 001 (CoRR, 2025)

Engineering an LTLf Synthesis Tool. - Alexandre Duret-Lutz; Shufang Zhu 001; Nir Piterman; Giuseppe De Giacomo; Moshe Y. Vardi (CoRR, 2025)

A Compositional Framework for On-the-Fly LTLf Synthesis. - Yongkang Li; Shengping Xiao; Shufang Zhu 001; Jianwen Li; Geguang Pu (CoRR, 2025)