Publications
This is the list of my current publications. You may also want to look at the DBLP page.
Go to: Conference papers | Editorships | PhD thesis
Journal articles • 8 items
2024
SAT Meets Tableaux for Linear Temporal Logic Satisfiability
Journal of Automated Reasoning
,
volume 68,
6
2023
Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis
Software and Systems Modeling
,
accepted for publication
A first-order logic characterization of safety and co-safety languages
Logical Methods in Computer Science
,
volume 19,
accepted for publication
GR(1) is equivalent to R(1)
Information Processing Letters
,
volume 179,
106319
2022
Decidability and Complexity of Action-Based Temporal Planning over Dense Time
Artificial Intelligence
,
volume 307,
103686
2021
Extended Bounded Response LTL: a New Safety Fragment for Efficient Reactive Synthesis
Formal Methods in System Design
,
to appear on paper
One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past
Information and Computation
,
volume 278,
104599
2020
On timeline-based games and their complexity
Theoretical Computer Science
,
volume 815,
pages 247‑269
Conference papers • 32 items
2023
A Landscape of First-Order Linear Temporal Logics in Infinite-State Verification and Temporal Ontologies
Proceedings of the 5th
Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis, OVERLAY 2023,
accepted for publication
Decidable Fragments of LTLf Modulo Theories
Proceedings of the 26th
European Conference on Artificial Intelligence, ECAI 2023,
accepted for publication
LTL over finite words can be exponentially more succinct than pure-past LTL, and vice versa
Proceedings of the 30th
International Symposium on Temporal Representation and Reasoning, TIME 2023,
accepted for publication
Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract)
Proceedings of the 30th
International Symposium on Temporal Representation and Reasoning, TIME 2023,
accepted for publication
Qualitative Past Timeline-Based Games (Extended Abstract)
Proceedings of the 30th
International Symposium on Temporal Representation and Reasoning, TIME 2023,
accepted for publication
A singly exponential transformation of LTL[X, F] into pure past LTL
Proceedings of the 20th
International Conference on Principles of Knowledge Representation and Reasoning, KR 2023,
pages 65‑74
DOI: 10.24963/kr.2023/7
Standpoint Linear Temporal Logic
Proceedings of the 20th
International Conference on Principles of Knowledge Representation and Reasoning, KR 2023,
pages 311‑321
DOI: 10.24963/kr.2023/31
On the Compilability of Bounded Numeric Planning
Proceedings of the 32nd
International Joint Conference on Artificial Intelligence, IJCAI 2023,
pages 5341‑5349
Complexity of Safety and coSafety Fragments of Linear Temporal Logic
Proceedings of the 37th
AAAI Conference on Artificial Intelligence, AAAI 2023,
pages 6236‑6244
2022
LTL Modulo Theories over Finite Traces: modeling, verification, open questions
Proceedings of the 4th
Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis, OVERLAY 2022,
pages 13‑19
Controller synthesis for Timeline-based games
Proceedings of the 13rd
International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2022,
pages 131‑146
DOI: 10.4204/EPTCS.370.9
Linear Temporal Logic Modulo Theories over Finite Traces
Proceedings of the 31st
International Joint Conference on Artificial Intelligence, IJCAI 2022,
pages 2641‑2647
On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning
Proceedings of the 19th
International Conference on Principles of Knowledge Representation and Reasoning, KR 2022,
published online
A first-order logic characterisation of safety and co-safety languages
Proceedings of the 25th
International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2022,
pages 244‑263
2021
Best Paper Award
Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL synthesis
Proceedings of the 19th
International Conference on Software Engineering and Formal Methods, SEFM 2021,
pages 351‑371
BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker
Proceedings of the 3rd
Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis, OVERLAY 2021,
pages 7‑12
Expressiveness of Extended Bounded Response LTL
Proceedings of the 12nd
International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021,
pages 152‑165
Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker
Proceedings of the 28th
International Symposium on Temporal Representation and Reasoning, TIME 2021,
pages 8:1‑8:17
2020
Reactive Synthesis from Extended Bounded Response LTL Specifications
Proceedings of the 20th
Formal Methods in Computer Aided Design, FMCAD 2020,
pages 83‑92
Complexity of qualitative timeline-based planning
Proceedings of the 27th
International Symposium on Temporal Representation and Reasoning, TIME 2020,
pages 16:1‑16:13
Decidability and Complexity of Action-Based Temporal Planning over Dense Time
Proceedings of the 34th
AAAI Conference on Artificial Intelligence, AAAI 2020,
pages 9859‑9866
2019
A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
Proceedings of the 28th
International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019,
pages 3‑20
2018
A Novel Automata-Theoretic Approach to Timeline-Based Planning
Proceedings of the 16th
International Conference on Principles of Knowledge Representation and Reasoning, KR 2018,
pages 541‑550
One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past
Proceedings of the 9th
International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018,
pages 176‑190
DOI: 10.4204/EPTCS.277.13
A Game-Theoretic Approach to Timeline-based Planning with Uncertainty
Proceedings of the 25th
International Symposium on Temporal Representation and Reasoning, TIME 2018,
pages 13:1‑13:17
2017
Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints
Proceedings of the 26th
International Joint Conference on Artificial Intelligence, IJCAI 2017,
pages 1008‑1014
Complexity of Timeline-based Planning
Proceedings of the 27th
International Conference on Automated Planning and Scheduling, ICAPS 2017,
pages 116‑124
A One-Pass Tree-Shaped Tableau for LTL + Past
Proceedings of the 21st
International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2017,
pages 456‑473
2016
Timelines are Expressive Enough to Capture Action-Based Temporal Planning
Proceedings of the 23rd
International Symposium on Temporal Representation and Reasoning, TIME 2016,
pages 100‑109
DOI: 10.1109/TIME.2016.18
A New Tableau-based Satisfiability Checker for Linear Temporal Logic (Extended Abstract)
Proceedings of the 39th
German Conference on Artificial Intelligence, KI 2016,
pages 251‑256
Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau
Proceedings of the 25th
International Joint Conference on Artificial Intelligence, IJCAI 2016,
pages 950‑956
2015
Average Linear Time and Compressed Space Construction of the Burrows-Wheeler Transform
Proceedings of the 9th
International Conference on Language and Automata Theory and Applications, LATA 2015,
pages 587‑598
Editorships
2020
Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis
(OVERLAY 2019),
CEUR Workshop Proceedings, volume 2509,
CEUR-WS.org
Ph.D. thesis
My Ph.D. thesis, titled Timeline-based Planning: Expressiveness and Complexity, discussed many theoretical questions regarding the timeline-based approach to automated planning problems.
You can find it on the arXiv as the record n.° 1902.06123.
The following BibTeX file can be used to cite it.