References

  1. Alfred V. Aho, John E. Hopcroft & Jeffrey D. Ullman (1974): The Design and Analysis of Computer Algorithms. Addison-Wesley.
  2. Roy Armoni, Sergey Egorov, Ranan Fraer, Dmitry Korchemny & Moshe Y. Vardi (2005): Efficient LTL compilation for SAT-based model checking. In: ICCAD 2005, pp. 877–884, doi:10.1109/ICCAD.2005.1560185.
  3. Fahiem Bacchus & Froduald Kabanza (1998): Planning for Temporally Extended Goals. Ann. Math. Artif. Intell. 22(1-2), pp. 5–27, doi:10.1023/A:1018985923441.
  4. Fahiem Bacchus & Froduald Kabanza (2000): Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1-2), pp. 123–191, doi:10.1016/S0004-3702(99)00071-5.
  5. Suguman Bansal, Yong Li, Lucas M. Tabajara & Moshe Y. Vardi (2020): Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. In: AAAI, pp. 9766–9774, doi:10.1609/aaai.v34i06.6528.
  6. Nicola Bertoglio, Gianfranco Lamperti & Marina Zanella (2019): Temporal Diagnosis of Discrete-Event Systems with Dual Knowledge Compilation. In: Andreas Holzinger, Peter Kieseberg, A Min Tjoa & Edgar R. Weippl: Machine Learning and Knowledge Extraction, Lecture Notes in Computer Science 11713. Springer, pp. 333–352, doi:10.1007/978-3-030-29726-8_21.
  7. Meghyn Bienvenu, Christian Fritz & Sheila A. McIlraith: Planning with Qualitative Temporal Preferences. In: Patrick Doherty, John Mylopoulos & Christopher A. Welty: KR.
  8. Roderick Bloem (2015): Reactive Synthesis. In: FMCAD. IEEE, pp. 3, doi:10.1109/FMCAD.2015.7542241.
  9. Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Specify, Compile, Run: Hardware from PSL. Electron. Notes Theor. Comput. Sci. 190(4), pp. 3–16, doi:10.1016/j.entcs.2007.09.004.
  10. Ronen I. Brafman & Giuseppe De Giacomo (2019): Planning for LTL_f /LDL_f Goals in Non-Markovian Fully Observable Nondeterministic Domains. In: Sarit Kraus: IJCAI, pp. 1602–1608, doi:10.24963/ijcai.2019/222.
  11. Ronen I. Brafman, Giuseppe De Giacomo & Fabio Patrizi (2018): LTL_f/LDL_f Non-Markovian Rewards. In: Sheila A. McIlraith & Kilian Q. Weinberger: AAAI, pp. 1771–1778.
  12. Randal E. Bryant (1992): Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv. 24(3), pp. 293–318, doi:10.1145/136035.136043.
  13. Janusz A. Brzozowski (1962): Canonical Regular Expressions and Minimal State Graphs for Definite Events.
  14. Marco Cadoli & Francesco M. Donini (1997): A Survey on Knowledge Compilation. AI Commun. 10(3-4), pp. 137–150.
  15. Diego Calvanese, Giuseppe De Giacomo & Moshe Y. Vardi: Reasoning about Actions and Planning in LTL Action Theories. In: Dieter Fensel, Fausto Giunchiglia, Deborah L. McGuinness & Mary-Anne Williams: KR.
  16. Alberto Camacho, Jorge A. Baier, Christian J. Muise & Sheila A. McIlraith (2018): Finite LTL Synthesis as Planning. In: ICAPS, pp. 29–38.
  17. Alberto Camacho, Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano & Sheila A. McIlraith (2019): LTL and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning. In: Sarit Kraus: IJCAI, pp. 6065–6073, doi:10.24963/ijcai.2019/840.
  18. Alberto Camacho, Eleni Triantafillou, Christian Muise, Jorge A. Baier & Sheila McIlraith (2017): Non-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Infinite Traces. In: AAAI, pp. 3716–3724.
  19. A.K. Chandra, D.C. Kozen & L.J. Stockmeyer (1981): Alternation. J. ACM 28(1), pp. 114–133, doi:10.1145/322234.322243.
  20. Claudio Di Ciccio, Fabrizio Maria Maggi, Marco Montali & Jan Mendling (2017): Resolving inconsistencies and redundancies in declarative process models. Inf. Syst. 64, pp. 425–446, doi:10.1016/j.is.2016.09.005.
  21. Luca Console, Paolo Terenziani & Daniele Theseider Dupré (2002): Local Reasoning and Knowledge Compilation for Efficient Temporal Abduction. IEEE Trans. Knowl. Data Eng. 14(6), pp. 1230–1248, doi:10.1109/TKDE.2002.1047764.
  22. Adnan Darwiche & Pierre Marquis (2002): A Knowledge Compilation Map. J. Artif. Intell. Res. 17, pp. 229–264, doi:10.1613/jair.989.
  23. Christian Dax, Jochen Eisinger & Felix Klaedtke (2007): Mechanizing the Powerset Construction for Restricted Classes of omega -Automata. In: Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino & Yoshio Okamura: ATVA, pp. 223–236, doi:10.1007/978-3-540-75596-8_17.
  24. Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti & Sasha Rubin (2020): Pure-Past Linear Temporal and Dynamic Logic on Finite Traces. In: Christian Bessiere: IJCAI, pp. 4959–4965, doi:10.24963/ijcai.2020/690.
  25. Giuseppe De Giacomo, Luca Iocchi, Marco Favorito & Fabio Patrizi (2019): Foundations for Restraining Bolts: Reinforcement Learning with LTL_f/LDL_f Restraining Specifications. In: ICAPS, pp. 128–136.
  26. Giuseppe De Giacomo & Sasha Rubin (2018): Automata-Theoretic Foundations of FOND Planning for LTL_f/LDL_f Goals. In: IJCAI, pp. 4729–4735, doi:10.24963/ijcai.2018/657.
  27. Giuseppe De Giacomo & Moshe Y. Vardi (2013): Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In: IJCAI, pp. 854–860, doi:10.5555/2540128.2540252.
  28. Giuseppe De Giacomo & Moshe Y. Vardi (2015): Synthesis for LTL and LDL on Finite Traces. In: IJCAI, pp. 1558–1564, doi:10.5555/2832415.2832466.
  29. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault & Laurent Xu (2016): Spot 2.0 — A Framework for LTL and ω-automata Manipulation. In: ATVA, pp. 122–129, doi:10.1007/978-3-319-46520-3_8.
  30. Sonali Dutta, Moshe Y. Vardi & Deian Tabakov (2013): CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models. In: DIFTS@FMCAD.
  31. Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Y. Vardi (1995): Reasoning About Knowledge. MIT Press, doi:10.7551/mitpress/5803.001.0001.
  32. Michael Fisher & Michael J. Wooldridge (2005): Temporal Reasoning in Agent-Based Systems. In: Michael Fisher, Dov M. Gabbay & Lluís Vila: Handbook of Temporal Reasoning in Artificial Intelligence, Foundations of Artificial Intelligence 1. Elsevier, pp. 469–495, doi:10.1016/S1574-6526(05)80017-3.
  33. Seth Fogarty, Orna Kupferman, Moshe Y. Vardi & Thomas Wilke (2013): Profile Trees for Büchi Word Automata, with Application to Determinization. In: GandALF, pp. 107–121, doi:10.4204/EPTCS.119.11.
  34. Dror Fried, Lucas M. Tabajara & Moshe Y. Vardi (2016): BDD-Based Boolean Functional Synthesis. In: CAV, pp. 402–421, doi:10.1007/978-3-319-41540-6_22.
  35. Giuseppe De Giacomo, Riccardo De Masellis, Marco Grasso, Fabrizio Maria Maggi & Marco Montali (2014): Monitoring Business Metaconstraints Based on LTL and LDL for Finite Traces. In: Shazia Wasim Sadiq, Pnina Soffer & Hagen Völzer: BPM, Lecture Notes in Computer Science 8659, pp. 1–17, doi:10.1007/978-3-319-10172-9_1.
  36. Giuseppe De Giacomo & Moshe Y. Vardi (1999): Automata-Theoretic Approach to Planning for Temporally Extended Goals. In: Susanne Biundo & Maria Fox: ECP, Lecture Notes in Computer Science 1809. Springer, pp. 226–238, doi:10.1007/10720246_18.
  37. Keliang He, Andrew M. Wells, Lydia E. Kavraki & Moshe Y. Vardi (2019): Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks. In: ICRA, pp. 8993–8999, doi:10.1109/ICRA.2019.8794170.
  38. Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe & Anders Sandholm (1995): Mona: Monadic Second-order Logic in Practice. In: TACAS, pp. 89–110, doi:10.1007/3-540-60630-0_5.
  39. John E. Hopcroft (1971): An n Log n Algorithm for Minimizing States in a Finite Automaton. Technical Report, Stanford, CA, USA.
  40. Orna Kupferman (2012): Recent Challenges and Ideas in Temporal Synthesis. In: SOFSEM, pp. 88–98, doi:10.1007/978-3-642-27660-6_8.
  41. Orna Kupferman & Moshe Y. Vardi (1998): Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time. In: LICS, pp. 81–92, doi:10.1109/LICS.1998.705645.
  42. Orna Kupferman & Moshe Y. Vardi (2001): Model Checking of Safety Properties. Formal Methods in System Design 19(3), pp. 291–314, doi:10.1023/A:1011254632723.
  43. Orna Kupferman & Moshe Y. Vardi (2005): Safraless Decision Procedures. In: FOCS, pp. 531–542, doi:10.1109/SFCS.2005.66.
  44. Orna Lichtenstein, Amir Pnueli & Lenore D. Zuck (1985): The Glory of the Past. In: Logics of Programs, pp. 196–218, doi:10.1007/3-540-15648-8_16.
  45. Andreas Morgenstern & Klaus Schneider (2008): From LTL to Symbolically Represented Deterministic Automata. In: Francesco Logozzo, Doron A. Peled & Lenore D. Zuck: VMCAI, pp. 279–293, doi:10.1007/978-3-540-78163-9_24.
  46. Maja Pesic, Helen Schonenberg & Wil M. P. van der Aalst (2007): DECLARE: Full Support for Loosely-Structured Processes. In: (EDOC, pp. 287–300, doi:10.1109/EDOC.2007.14.
  47. Jean-Eric Pin (1987): On the Language Accepted by Finite Reversible Automata. In: Thomas Ottmann: ICALP, pp. 237–249, doi:10.1007/3-540-18088-5_19.
  48. Amir Pnueli (1977): The temporal logic of programs, pp. 46–57, doi:10.1109/SFCS.1977.32.
  49. Amir Pnueli & Roni Rosner (1989): On the Synthesis of a Reactive Module. In: POPL, pp. 179–190, doi:10.1145/75277.75293.
  50. M.O. Rabin & D. Scott (1959): Finite automata and their decision problems. IBM Journal of Research and Development 3, pp. 115–125, doi:10.1147/rd.32.0114.
  51. Fabio Somenzi (2016): CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder.
  52. Lucas Martinelli Tabajara & Moshe Y. Vardi (2019): Partitioning Techniques in LTL_f Synthesis. In: IJCAI, pp. 5599–5606, doi:10.24963/ijcai.2019/777.
  53. Deian Tabakov, Kristin Y. Rozier & Moshe Y. Vardi (2012): Optimized temporal monitors for SystemC. Formal Methods in System Design 41(3), pp. 236–268, doi:10.1007/s10703-011-0139-8.
  54. Deian Tabakov & Moshe Y. Vardi (2005): Experimental Evaluation of Classical Automata Constructions. In: LPAR, pp. 396–411, doi:10.1007/11591191_28.
  55. Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki & Moshe Y. Vardi (2020): LTL_f Synthesis on Probabilistic Systems. In: Jean-François Raskin & Davide Bresolin: GandALF, EPTCS 326, pp. 166–181, doi:10.4204/EPTCS.326.11.
  56. Yaqi Xie, Fan Zhou & Harold Soh (2021): Embedding Symbolic Temporal Knowledge into Deep Sequential Models. CoRR abs/2101.11981.
  57. Shufang Zhu, Giuseppe De Giacomo, Geguang Pu & Moshe Y. Vardi (2020): LTL_f Synthesis with Fairness and Stability Assumptions. In: AAAI, pp. 3088–3095, doi:10.1609/aaai.v34i03.5704.
  58. Shufang Zhu, Geguang Pu & Moshe Y. Vardi (2019): First-Order vs. Second-Order Encodings for LTL_f-to-Automata Translation. In: TAMC, pp. 684–705, doi:10.1007/978-3-030-14812-6_43.
  59. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu & Moshe Y. Vardi (2017): A Symbolic Approach to Safety LTL Synthesis. In: HVC, pp. 147–162, doi:10.1007/978-3-319-70389-3_10.
  60. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu & Moshe Y. Vardi (2017): Symbolic LTL_f Synthesis. In: IJCAI, pp. 1362–1369, doi:10.24963/ijcai.2017/189.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org