Optimal Translation of LTL to Limit Deterministic Automata

DOI10.1007/978-3-662-54580-5_7zbMath1452.68121OpenAlexW2590126170MaRDI QIDQ3303923

Dileep Kini, Mahesh Viswanathan

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2142/95004

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (3)

Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning ⋮ Certified reinforcement learning with logic guidance ⋮ Functional Encryption for Inner Product with Full Function Privacy

Uses Software

• PRISM
• Rabinizer
• MoChiBA

Cites Work

• Unnamed Item
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• Limit deterministic and probabilistic automata for \(\mathrm{LTL}\backslash GU\)
• From LTL to deterministic automata. A safraless compositional approach
• Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
• Solving Games Without Determinization
• The complexity of probabilistic verification
• Limit-Deterministic Büchi Automata for Linear Temporal Logic
• Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
• Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
• Deterministic generators and games for Ltl fragments
• Lazy probabilistic model checking without determinisation
• Are Good-for-Games Automata Good for Probabilistic Model Checking?
• From LTL to Symbolically Represented Deterministic Automata
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Optimal Translation of LTL to Limit Deterministic Automata