Publication:4945211

zbMath0943.03008MaRDI QIDQ4945211

Klaus Schneider, Dirk W. Hoffmann

Publication date: 5 September 2000

zbMATH Keywords

\(\omega\)-automata; decision procedures; HOL theorem prover; linear time temporal logic; symbolic model checkers

Mathematics Subject Classification ID

03D05: Automata and formal grammars in connection with logical questions

68Q60: Specification and verification (program logics, model checking, etc.)

03B35: Mechanization of proofs and logical operations

03B44: Temporal logic

Related Items

Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL

Uses Software

• SPIN
• HOL