``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking

DOI10.1007/B93958MaRDI QIDQ5897061zbMATH OpenOpenAlexFDO

Authors Roberto Sebastiani, Stefano Tonetta

Publication date 5 February 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b93958

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1670781
• LTL to Büchi automata translation: fast and more deterministic
• Model Checking Software
• Limit-deterministic Büchi automata for linear temporal logic
• scientific article; zbMATH DE number 1973991

Cited in

(16)

• Finding and fixing faults
• Model Checking Software
• Experiments with deterministic -automata for formulas of linear temporal logic
• GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
• From LTL and limit-deterministic Büchi automata to deterministic parity automata
• Automata-driven partial order reduction and guided search for LTL model checking
• Linear temporal logic symbolic model checking
• Tool support for learning Büchi automata and linear temporal logic
• Graph Games and Reactive Synthesis
• GSTE is partitioned model checking
• Limit-deterministic Büchi automata for linear temporal logic
• Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
• Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)
• Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
• How hard is finding shortest counter-example lassos in model checking?
• On the relationship between LTL normal forms and Büchi automata

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking

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