Uniform inevitability is tree automaton ineffable

DOI10.1016/0020-0190(87)90097-4MaRDI QIDQ1108048zbMATH OpenOpenAlexFDO

Authors E. Allen Emerson

Publication date 1987

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(87)90097-4

zbMATH Keywords

temporal logicexpressive powertree automatonMuller automatacorrectness of concurrent programsfinite automata on infinite treesuniform inevitability

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 6680130
• scientific article; zbMATH DE number 3982544
• scientific article; zbMATH DE number 6741931
• Topological characterizations of infinite tree languages
• A characterization of Büchi tree automata

Cites work

• scientific article; zbMATH DE number 3887063 (Why is no real title available?)
• scientific article; zbMATH DE number 3876574 (Why is no real title available?)
• scientific article; zbMATH DE number 3972842 (Why is no real title available?)
• scientific article; zbMATH DE number 3714896 (Why is no real title available?)
• Deciding full branching time logic
• Propositional dynamic logic of looping and converse is elementarily decidable
• Results on the propositional \(\mu\)-calculus
• “Sometimes” and “not never” revisited

Cited in

(10)

• Automated temporal reasoning about reactive systems
• Infinite trees and automaton-definable relations over -words
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• Automata on infinite objects and their applications to logic and programming
• scientific article; zbMATH DE number 49206 (Why is no real title available?)
• Temporal Logic with Recursion.
• To know or not to know: Epistemic approaches to security protocol verification
• Temporal logic with recursion
• The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata
• The complexity of model-checking tail-recursive higher-order fixpoint logic

This page was built for publication: Uniform inevitability is tree automaton ineffable

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