Alternating automata and temporal logic normal forms

DOI10.1016/J.APAL.2005.03.002MaRDI QIDQ2488275zbMATH OpenOpenAlexWikidataFDO

Authors Yanyan Li

Publication date 25 August 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.03.002

zbMATH Keywords

Alternating automataSpecification and verificationTemporal logic

Mathematics Subject Classification ID

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

Recommendations

• On the Relationship between  -automata and Temporal Logic Normal Forms
• Alternating automata: unifying truth and validity checking for temporal logics
• Converting a Büchi alternating automaton to a usual nondeterministic one
• How to translate efficiently extensions of temporal logics into alternating automata
• scientific article; zbMATH DE number 1759492

Cites work

• A clausal resolution method for CTL branching-time temporal logic
• A clausal resolution method for extended computation tree logic ECTL
• A Normal Form for Temporal Logics and its Applications in Theorem-Proving and Execution
• Alternating automata: unifying truth and validity checking for temporal logics
• Alternating finite automata on -words
• Alternation
• Clausal temporal resolution
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1538010 (Why is no real title available?)
• Multiobjective Heuristic Search in AND/OR Graphs
• On equations for regular languages, finite automata, and sequential networks
• On the Relationship between  -automata and Temporal Logic Normal Forms
• Reasoning about infinite computations
• Resolution for temporal logics of knowledge

Cited in

(5)

• Transformation from PLTL to automata via NFGs
• On the Relationship between  -automata and Temporal Logic Normal Forms
• Converting a Büchi alternating automaton to a usual nondeterministic one
• On the expressive power of the normal form for branching-time temporal logics
• Dynamic logic assigned to automata

This page was built for publication: Alternating 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 Q2488275)