Uniform inevitability is tree automaton ineffable

DOI10.1016/0020-0190(87)90097-4zbMath0653.68079OpenAlexW2061141623MaRDI QIDQ1108048

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) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic ⋮ To know or not to know: Epistemic approaches to security protocol verification ⋮ Temporal Logic with Recursion. ⋮ Infinite trees and automaton-definable relations over \(\omega\)-words ⋮ Temporal logic with recursion ⋮ The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Propositional dynamic logic of looping and converse is elementarily decidable
• Deciding full branching time logic
• “Sometimes” and “not never” revisited

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