Alfred V. Aho, John E. Hopcroft & Jeffrey D. Ullman (1974):
The Design and Analysis of Computer Algorithms.
Addison-Wesley.
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.
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.
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.
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.
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.
Meghyn Bienvenu, Christian Fritz & Sheila A. McIlraith:
Planning with Qualitative Temporal Preferences.
In: Patrick Doherty, John Mylopoulos & Christopher A. Welty: KR.
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.
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.
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.
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.
Janusz A. Brzozowski (1962):
Canonical Regular Expressions and Minimal State Graphs for Definite Events.
Marco Cadoli & Francesco M. Donini (1997):
A Survey on Knowledge Compilation.
AI Commun. 10(3-4),
pp. 137–150.
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.
Alberto Camacho, Jorge A. Baier, Christian J. Muise & Sheila A. McIlraith (2018):
Finite LTL Synthesis as Planning.
In: ICAPS,
pp. 29–38.
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.
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.
A.K. Chandra, D.C. Kozen & L.J. Stockmeyer (1981):
Alternation.
J. ACM 28(1),
pp. 114–133,
doi:10.1145/322234.322243.
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.
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.
Adnan Darwiche & Pierre Marquis (2002):
A Knowledge Compilation Map.
J. Artif. Intell. Res. 17,
pp. 229–264,
doi:10.1613/jair.989.
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.
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.
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.
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.
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.
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.
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.
Sonali Dutta, Moshe Y. Vardi & Deian Tabakov (2013):
CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models.
In: DIFTS@FMCAD.
Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Y. Vardi (1995):
Reasoning About Knowledge.
MIT Press,
doi:10.7551/mitpress/5803.001.0001.
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.
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.
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.
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.
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.
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.
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.
John E. Hopcroft (1971):
An n Log n Algorithm for Minimizing States in a Finite Automaton.
Technical Report,
Stanford, CA, USA.
Orna Kupferman (2012):
Recent Challenges and Ideas in Temporal Synthesis.
In: SOFSEM,
pp. 88–98,
doi:10.1007/978-3-642-27660-6_8.
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.
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.
Orna Kupferman & Moshe Y. Vardi (2005):
Safraless Decision Procedures.
In: FOCS,
pp. 531–542,
doi:10.1109/SFCS.2005.66.
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.
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.
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.
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.
Amir Pnueli (1977):
The temporal logic of programs,
pp. 46–57,
doi:10.1109/SFCS.1977.32.
Amir Pnueli & Roni Rosner (1989):
On the Synthesis of a Reactive Module.
In: POPL,
pp. 179–190,
doi:10.1145/75277.75293.
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.
Fabio Somenzi (2016):
CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder.
Lucas Martinelli Tabajara & Moshe Y. Vardi (2019):
Partitioning Techniques in LTL_f Synthesis.
In: IJCAI,
pp. 5599–5606,
doi:10.24963/ijcai.2019/777.
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.
Deian Tabakov & Moshe Y. Vardi (2005):
Experimental Evaluation of Classical Automata Constructions.
In: LPAR,
pp. 396–411,
doi:10.1007/11591191_28.
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.
Yaqi Xie, Fan Zhou & Harold Soh (2021):
Embedding Symbolic Temporal Knowledge into Deep Sequential Models.
CoRR abs/2101.11981.
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.
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.
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.
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.