scientific article; zbMATH DE number 1424021

MaRDI QIDQ4945211zbMATH OpenFDO

Authors Klaus Schneider, Dirk W. Hoffmann

Publication date 5 September 2000

zbMATH Keywords

decision proceduresHOL theorem prover\(\omega\)-automatalinear time temporal logicsymbolic model checkers

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Recommendations

• Verifying the LTL to Büchi automata translation via very weak alternating automata
• Theorem Proving in Higher Order Logics
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Improving automata generation for linear temporal logic by considering the automaton hierarchy
• scientific article; zbMATH DE number 6401143

Cited in

(5)

• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Owl: a library for \(\omega \)-words, automata, and LTL
• GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
• Theorem Proving in Higher Order Logics
• Verifying the LTL to Büchi automata translation via very weak alternating automata

Describes a project that uses

Uses Software

• SPIN
• HOL

This page was built for publication:

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