Bounded Model Checking for Weak Alternating Büchi Automata

DOI10.1007/11817963_12MaRDI QIDQ5756750zbMATH OpenOpenAlexFDO

Authors Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, Timo Latvala

Publication date 5 September 2007

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

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

zbMATH Keywords

bounded model checkingNuSMVPSLweak alternating Büchi automata

Mathematics Subject Classification ID

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

Recommendations

• Bounded model checking with SNF, alternating automata, and Büchi automata
• Bounded model checking for all regular properties
• Linear Encodings of Bounded LTL Model Checking
• scientific article; zbMATH DE number 1796122
• Bounded model checking of infinite state systems

Cited in

(5)

• Bounded model checking with SNF, alternating automata, and Büchi automata
• SAT-Based Model Checking
• An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking
• Solving parity games by a reduction to SAT
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: Bounded Model Checking for Weak Alternating Büchi Automata

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