Optimal Translation of LTL to Limit Deterministic Automata

DOI10.1007/978-3-662-54580-5_7MaRDI QIDQ3303923zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 6527944
• LTL to Büchi automata translation: fast and more deterministic
• Efficient approach of translating LTL formulae into Büchi automata
• scientific article; zbMATH DE number 1796123
• Comparison of LTL to Deterministic Rabin Automata Translators
• From LTL to Symbolically Represented Deterministic Automata
• Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
• scientific article; zbMATH DE number 7649960
• LTL to deterministic Emerson-Lei automata
• scientific article; zbMATH DE number 1973991

Cites work

• Are good-for-games automata good for probabilistic model checking?
• Deterministic generators and games for LTL fragments
• Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
• Experiments with deterministic -automata for formulas of linear temporal logic
• From LTL to deterministic automata. A safraless compositional approach
• From LTL to Symbolically Represented Deterministic Automata
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• Lazy probabilistic model checking without determinisation
• Limit deterministic and probabilistic automata for \(\mathrm{LTL}\backslash GU\)
• Limit-deterministic Büchi automata for linear temporal logic
• Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
• Rabinizer 3: Safraless translation of LTL to small deterministic automata
• Solving Games Without Determinization
• The complexity of probabilistic verification
• Verification, Model Checking, and Abstract Interpretation

Cited in

(7)

• Efficient approach of translating LTL formulae into Büchi automata
• Limit deterministic and probabilistic automata for \(\mathrm{LTL}\backslash GU\)
• Functional encryption for inner product with full function privacy
• scientific article; zbMATH DE number 6527944 (Why is no real title available?)
• Limit-deterministic Büchi automata for linear temporal logic
• Good-for-MDPs automata for probabilistic analysis and reinforcement learning
• Certified reinforcement learning with logic guidance

Describes a project that uses

Uses Software

• PRISM
• Rabinizer
• MoChiBA

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303923)