``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
From MaRDI portal
Publication:5897061
DOI10.1007/B93958zbMATH Open1179.68095OpenAlexW219731125MaRDI QIDQ5897061FDOQ5897061
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
Recommendations
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (16)
- Finding and fixing faults
- Model Checking Software
- Experiments with deterministic \(\omega\)-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
Uses Software
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)
