Publications
2025
ltl synthesis under environment specifications for reachability and safety properties
Aminof, B., De Giacomo, G., Di Stasio, A., Francon, H., Rubin, S., & Zhu, S. (2025). ltl synthesis under environment specifications for reachability and safety properties. Information and Computation, 303, 105255. doi:10.1016/j.ic.2024.105255
Symbolic ltl$$_f$$ Synthesis: A Unified Approach for Synthesizing Winning, Dominant, and Best-Effort Strategies
De Giacomo, G., Parretti, G., & Zhu, S. (n.d.). Symbolic ltl$$_f$$ Synthesis: A Unified Approach for Synthesizing Winning, Dominant, and Best-Effort Strategies. SN Computer Science, 6(2). doi:10.1007/s42979-024-03337-8
Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Greenman, B., Prasad, S., Di Stasio, A., Zhu, S., De Giacomo, G., Krishnamurthi, S., . . . Zizyte, M. (2025). Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic. In Lecture Notes in Computer Science (pp. 579-599). Springer Nature Switzerland. doi:10.1007/978-3-031-71162-6_30
2024
Mimicking Behaviors in Separated Domains (Abstract Reprint)
De Giacomo, G., Fried, D., Patrizi, F., & Zhu, S. (n.d.). Mimicking Behaviors in Separated Domains (Abstract Reprint). Proceedings of the AAAI Conference on Artificial Intelligence, 38(20), 22695. doi:10.1609/aaai.v38i20.30595
The Trembling-Hand Problem for LTLf Planning
Yu, P., Zhu, S., De Giacomo, G., Kwiatkowska, M., & Vardi, M. (2024). The Trembling-Hand Problem for LTLf Planning. In Proceedings of the Thirty-ThirdInternational Joint Conference on Artificial Intelligence (pp. 3631-3641). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2024/402
2023
LTLf Best-Effort Synthesis in Nondeterministic Planning Domains
De Giacomo, G., Parretti, G., & Zhu, S. (2023). LTLf Best-Effort Synthesis in Nondeterministic Planning Domains. IOS Press. doi:10.3233/faia230313
$${\textsc {ltl}}_f$$ Synthesis Under Environment Specifications for Reachability and Safety Properties
Aminof, B., De Giacomo, G., Di Stasio, A., Francon, H., Rubin, S., & Zhu, S. (2023). $${\textsc {ltl}}_f$$ Synthesis Under Environment Specifications for Reachability and Safety Properties. In Unknown Conference (pp. 263-279). Springer Nature Switzerland. doi:10.1007/978-3-031-43264-4_17
Compositional Safety LTL Synthesis
Bansal, S., De Giacomo, G., Di Stasio, A., Li, Y., Vardi, M. Y., & Zhu, S. (2023). Compositional Safety LTL Synthesis. In Unknown Conference (pp. 1-19). Springer International Publishing. doi:10.1007/978-3-031-25803-9_1
Mimicking Behaviors in Separated Domains
De Giacomo, G., Fried, D., Patrizi, F., & Zhu, S. (n.d.). Mimicking Behaviors in Separated Domains. Journal of Artificial Intelligence Research, 77, 1087-1112. doi:10.1613/jair.1.14591
Symbolic $$\textsc {ltl}_f$$ Best-Effort Synthesis
De Giacomo, G., Parretti, G., & Zhu, S. (2023). Symbolic $$\textsc {ltl}_f$$ Best-Effort Synthesis. In Unknown Conference (pp. 228-243). Springer Nature Switzerland. doi:10.1007/978-3-031-43264-4_15
2022
Finite-trace and generalized-reactivity specifications in temporal synthesis
De Giacomo, G., Di Stasio, A., Tabajara, L. M., Vardi, M. Y., & Zhu, S. (2022). Finite-trace and generalized-reactivity specifications in temporal synthesis. Formal Methods in System Design, 61(2-3), 139-163. doi:10.1007/s10703-023-00413-2
LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
De Giacomo, G., Favorito, M., Li, J., Vardi, M. Y., Xiao, S., & Zhu, S. (2022). LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (pp. 2591-2598). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2022/359
Synthesis of Maximally Permissive Strategies for LTLf Specifications
Zhu, S., & De Giacomo, G. (2022). Synthesis of Maximally Permissive Strategies for LTLf Specifications. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (pp. 2783-2789). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2022/386
Act for Your Duties but Maintain Your Rights
Zhu, S., & De Giacomo, G. (2022). Act for Your Duties but Maintain Your Rights. In Proceedings of the Nineteenth International Conference on Principles of Knowledge Representation and Reasoning (pp. 384-393). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/kr.2022/38
LTL<inf>f</inf> Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
De Giacomo, G., Favorito, M., Li, J., Vardi, M. Y., Xiao, S., & Zhu, S. (2022). LTL<inf>f</inf> Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. In IJCAI International Joint Conference on Artificial Intelligence (pp. 2591-2598). doi:10.24963/ijcai.2022/359
Synthesis of Maximally Permissive Strategies for LTL<inf>f</inf> Specifications
Zhu, S., & De Giacomo, G. (2022). Synthesis of Maximally Permissive Strategies for LTL<inf>f</inf> Specifications. In IJCAI International Joint Conference on Artificial Intelligence (pp. 2783-2789). doi:10.24963/ijcai.2022/386
2021
On the Power of Automata Minimization in Reactive Synthesis
Zhu, S., M. Tabajara, L., Pu, G., & Y. Vardi, M. (n.d.). On the Power of Automata Minimization in Reactive Synthesis. In Electronic Proceedings in Theoretical Computer Science Vol. 346 (pp. 117-134). Open Publishing Association. doi:10.4204/eptcs.346.8
Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
De Giacomo, G., Di Stasio, A., M. Tabajara, L., Vardi, M., & Zhu, S. (2021). Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence (pp. 1852-1858). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2021/255
On-the-fly Synthesis for LTL over Finite Traces
Xiao, S., Li, J., Zhu, S., Shi, Y., Pu, G., & Vardi, M. (n.d.). On-the-fly Synthesis for LTL over Finite Traces. In Proceedings of the AAAI Conference on Artificial Intelligence Vol. 35 (pp. 6530-6537). Association for the Advancement of Artificial Intelligence (AAAI). doi:10.1609/aaai.v35i7.16809
Synthesis with Mandatory Stop Actions
De Giacomo, G., Di Stasio, A., Perelli, G., & Zhu, S. (2021). Synthesis with Mandatory Stop Actions. In Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning (pp. 237-246). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/kr.2021/23
2020
Two-Stage Technique for LTLf Synthesis Under LTL Assumptions
De Giacomo, G., Di Stasio, A., Vardi, M. Y., & Zhu, S. (2020). Two-Stage Technique for LTLf Synthesis Under LTL Assumptions. In Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning (pp. 304-314). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/kr.2020/31
LTLƒ Synthesis with Fairness and Stability Assumptions
Zhu, S., De Giacomo, G., Pu, G., & Vardi, M. Y. (n.d.). LTLƒ Synthesis with Fairness and Stability Assumptions. Proceedings of the AAAI Conference on Artificial Intelligence, 34(03), 3088-3095. doi:10.1609/aaai.v34i03.5704
LTL<inf>f</inf> synthesis with fairness and stability assumptions
Zhu, S., de Giacomo, G., Pu, G., & Vardi, M. Y. (2020). LTL<inf>f</inf> synthesis with fairness and stability assumptions. In AAAI 2020 - 34th AAAI Conference on Artificial Intelligence (pp. 3088-3095).
Two-stage technique for ltlf synthesis under ltl assumptions
De Giacomo, G., Di Stasio, A., Vardi, M. Y., & Zhu, S. (2020). Two-stage technique for ltlf synthesis under ltl assumptions. In 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 Vol. 1 (pp. 303-313).
2019
SAT-based explicit LTL reasoning and its application to satisfiability checking
Li, J., Zhu, S., Pu, G., Zhang, L., & Vardi, M. Y. (2019). SAT-based explicit LTL reasoning and its application to satisfiability checking. Formal Methods in System Design, 54(2), 164-190. doi:10.1007/s10703-018-00326-5
First-Order vs. Second-Order Encodings for $$\textsc {ltl}_f$$-to-Automata Translation
Zhu, S., Pu, G., & Vardi, M. Y. (2019). First-Order vs. Second-Order Encodings for $$\textsc {ltl}_f$$-to-Automata Translation. In Unknown Conference (pp. 684-705). Springer International Publishing. doi:10.1007/978-3-030-14812-6_43
2018
An explicit transition system construction approach to LTL satisfiability checking
Li, J., Zhang, L., Zhu, S., Pu, G., Vardi, M. Y., & He, J. (2018). An explicit transition system construction approach to LTL satisfiability checking. Formal Aspects of Computing, 30(2), 193-217. doi:10.1007/s00165-017-0442-2
2017
Safety model checking with complementary approximations
Li, J., Zhu, S., Zhang, Y., Pu, G., & Vardi, M. Y. (2017). Safety model checking with complementary approximations. In 2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD) (pp. 95-100). IEEE. doi:10.1109/iccad.2017.8203765
A Symbolic Approach to Safety ltl Synthesis
Zhu, S., Tabajara, L. M., Li, J., Pu, G., & Vardi, M. Y. (2017). A Symbolic Approach to Safety ltl Synthesis. In Unknown Conference (pp. 147-162). Springer International Publishing. doi:10.1007/978-3-319-70389-3_10
Symbolic LTLf Synthesis
Zhu, S., M. Tabajara, L., Li, J., Pu, G., & Y. Vardi, M. (2017). Symbolic LTLf Synthesis. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (pp. 1362-1369). International Joint Conferences on Artificial Intelligence Organization. doi:10.24963/ijcai.2017/189
2015
SAT-Based Explicit LTL Reasoning
Li, J., Zhu, S., Pu, G., & Vardi, M. Y. (2015). SAT-Based Explicit LTL Reasoning. In Unknown Conference (pp. 209-224). Springer International Publishing. doi:10.1007/978-3-319-26287-1_13