Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker & Jan Strejček (2015):
The Hanoi Omega-Automata Format.
In: Computer Aided Verification.
Springer Intl. Publishing,
Cham,
pp. 479–486,
doi:10.1007/978-3-319-21690-4_31.
Tomáš Babiak, František Blahoudek, Mojmír Křetínsk\`y & Jan Strejček (2013):
Effective translation of LTL to deterministic Rabin automata: Beyond the (F, G)-fragment.
In: Automated Technology for Verification and Analysis.
Springer,
pp. 24–39,
doi:10.1007/10722167_21.
Fahiem Bacchus, Craig Boutilier & Adam Grove (1996):
Rewarding Behaviors.
In: Proc. of the Thirteenth Natl. Conf. on Artificial Intelligence - Volume 2,
AAAI’96.
AAAI Press,
pp. 1160–1167.
Fahiem Bacchus, Craig Boutilier & Adam Grove (1997):
Structured Solution Methods for Non-Markovian Decision Processes.
In: Proc. of the (AAAI-97) and (IAAI-97),
AAAI’97/IAAI’97.
AAAI Press,
pp. 112–117.
Christel Baier & Joost-Pieter Katoen (2008):
Principles of Model Checking.
The MIT Press.
Ronen I. Brafman, Giuseppe De Giacomo & Fabio Patrizi (2018):
LTLf/LDLf Non-Markovian Rewards.
In: Proc. of (AAAI-18), (IAAI-18), and (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018.
AAAI Press,
pp. 1771–1778.
Alberto Camacho, Oscar Chen, Scott Sanner & Sheila A. McIlraith (2017):
Non-Markovian Rewards Expressed in LTL: Guiding Search Via Reward Shaping.
In: SOCS.
Costas Courcoubetis & Mihalis Yannakakis (1995):
The Complexity of Probabilistic Verification.
J. ACM 42(4),
pp. 857–907,
doi:10.1145/210332.210339.
Luca De Alfaro (1998):
Formal Verification of Probabilistic Systems,
Stanford, CA, USA.
Giuseppe De Giacomo & Moshe Y Vardi (2013):
Linear Temporal Logic and Linear Dynamic Logic on Finite Traces..
In: Intl. Joint Conf. on Artificial Intelligence (IJCAI) 13,
pp. 854–860.
Giuseppe De Giacomo & Moshe Y Vardi (2015):
Synthesis for LTL and LDL on Finite Traces.
In: Intl. Joint Conf. on Artificial Intelligence (IJCAI) 15,
pp. 1558–1564.
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Étienne Renault & Laurent Xu (2016):
Spot 2.0 — a framework for LTL and ω-automata manipulation.
In: Automated Technology for Verification and Analysis (ATVA'16),
Lecture Notes in Computer Science 9938.
Springer,
pp. 122–129,
doi:10.1007/3-540-60915-6_6.
Keliang He, Morteza Lahijanian, Lydia E Kavraki & Moshe Y Vardi (2018):
Automated Abstraction of Manipulation Domains for Cost-Based Reactive Synthesis.
IEEE Robotics and Automation Letters 4(2),
pp. 285–292,
doi:10.1109/LRA.2018.2889191.
Keliang He, Andrew M Wells, Lydia E Kavraki & Moshe Y Vardi (2019):
Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks.
In: 2019 Intl. Conf. on Robotics and Automation (ICRA).
IEEE,
pp. 8993–8999,
doi:10.1109/ICRA.2019.8794170.
Keling He, Morteza Lahijanian, Lydia E. Kavraki & Moshe Y. Vardi (2017):
Reactive Synthesis for Finite Tasks Under Resource Constraints.
In: Int. Conf. on Intelligent Robots and Systems (IROS).
IEEE,
Vancouver, BC, Canada,
pp. 5326–5332,
doi:10.1109/IROS.2017.8206426.
Jesper G Henriksen, Jakob Jensen, Michael Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe & Anders Sandholm (1995):
Mona: Monadic second-order logic in practice.
In: Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems.
Springer,
pp. 89–110,
doi:10.1007/3-540-60630-0_5.
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert & Christopher Ziegler (2018):
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton.
In: Computer Aided Verification.
Springer International Publishing,
Cham,
pp. 567–577,
doi:10.1007/978-3-319-46520-3_9.
M. Kwiatkowska, G. Norman & D. Parker (2011):
PRISM 4.0: Verification of Probabilistic Real-time Systems.
In: Proc. 23rd Intl. Conf. on Computer Aided Verification (CAV'11),
LNCS 6806.
Springer,
pp. 585–591,
doi:10.1007/3-540-45657-0_17.
Jianwen Li, Kristin Y Rozier, Geguang Pu, Yueling Zhang & Moshe Y Vardi (2019):
SAT-Based Explicit LTLf Satisfiability Checking.
In: Proc. of the AAAI Conf. on Artificial Intelligence 33,
pp. 2946–2953,
doi:10.1007/978-3-030-25543-5_1.
Lucas Martinelli Tabajara & Moshe Y. Vardi (2019):
Partitioning Techniques in LTLf Synthesis.
In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19.
International Joint Conferences on Artificial Intelligence Organization,
pp. 5599–5606,
doi:10.24963/ijcai.2019/777.
Amir Pnueli (1977):
The temporal logic of programs.
In: Foundations of Computer Science, 1977., 18th Annual Symposium on.
IEEE,
pp. 46–57.
Salomon Sickert & Jan Kretínský (2016):
MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata.
In: Automated Technology for Verification and Analysis (ATVA'16),
Lecture Notes in Computer Science 9938,
pp. 130–137,
doi:10.1007/978-3-319-45856-4.
Sylvie Thiébaux, Charles Gretton, John Slaney, David Price & Froduald Kabanza (2006):
Decision-Theoretic Planning with Non-Markovian Rewards.
J. Artif. Int. Res. 25(1),
pp. 17–74,
doi:10.1613/jair.1676.
Moshe Y. Vardi (1985):
Automatic Verification of Probabilistic Concurrent Finite State Programs.
In: Proceedings of the 26th Annual Symposium on Foundations of Computer Science,
SFCS '85.
IEEE Computer Society,
USA,
pp. 327–338,
doi:10.1109/SFCS.1985.12.
Shufang Zhu, Lucas M Tabajara, Jianwen Li, Geguang Pu & Moshe Y Vardi (2017):
Symbolic LTLf synthesis.
In: Proc. of the 26th Intl. Joint Conf. on Artificial Intelligence.
AAAI Press,
pp. 1362–1369.
eptcs@eptcs.org