Limit-Deterministic Büchi Automata for Linear Temporal Logic

DOI10.1007/978-3-319-41540-6_17zbMath1411.68054OpenAlexW2487186542MaRDI QIDQ4633559

Stefan Jaax, Salomon Sickert, Jan Křetínský, Javier Esparza

Publication date: 3 May 2019

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-41540-6_17

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (20)

Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning ⋮ Determinization and limit-determinization of Emerson-Lei automata ⋮ Index appearance record with preorders ⋮ On the power of finite ambiguity in Büchi complementation ⋮ Markov chains and unambiguous automata ⋮ Certified reinforcement learning with logic guidance ⋮ Unnamed Item ⋮ Ambiguity, weakness, and regularity in probabilistic Büchi automata ⋮ Unnamed Item ⋮ Unnamed Item ⋮ From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata ⋮ Optimal Translation of LTL to Limit Deterministic Automata ⋮ Deep reinforcement learning with temporal logics ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Unnamed Item ⋮ A novel learning algorithm for Büchi automata based on family of DFAs and classification trees ⋮ Practical synthesis of reactive systems from LTL specifications via parity games ⋮ Model-Free Reinforcement Learning for Stochastic Parity Games ⋮ Minimizing GFG Transition-Based Automata ⋮ Complexity of model checking MDPs against LTL specifications

Uses Software

• PRISM
• BEEM
• Rabinizer

This page was built for publication: Limit-Deterministic Büchi Automata for Linear Temporal Logic