scientific article; zbMATH DE number 1424021

MaRDI QIDQ4945211zbMATH OpenFDO

Authors Klaus Schneider, Dirk W. Hoffmann

Publication date 5 September 2000

zbMATH Keywords

\(\omega\)-automatadecision proceduresHOL theorem proverlinear time temporal logicsymbolic model checkers

Mathematics Subject Classification ID

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

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)

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

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)