On the Relationship between -automata and Temporal Logic Normal Forms

DOI10.1093/LOGCOM/12.4.561MaRDI QIDQ3146301zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 22 March 2003

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/12.4.561

zbMATH Keywords

automataclausal resolutionnormal formstemporal logictheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05)

Recommendations

• Alternating automata and temporal logic normal forms
• scientific article; zbMATH DE number 3989329
• scientific article; zbMATH DE number 3922633
• On the relationship between LTL normal forms and Büchi automata
• scientific article; zbMATH DE number 5872401

Cited in

(4)

• Alternating automata and temporal logic normal forms
• A clausal resolution method for extended computation tree logic ECTL
• On the expressive power of the normal form for branching-time temporal logics
• Variable and clause elimination for LTL satisfiability checking

This page was built for publication: On the Relationship between  -automata and Temporal Logic Normal Forms

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