The Complexity of Tree Automata and Logics of Programs

DOI10.1137/S0097539793304741zbMath0937.68074MaRDI QIDQ4268874

Charanjit S. Jutla, E. Allen Emerson

Publication date: 28 October 1999

Published in: SIAM Journal on Computing (Search for Journal in Brave)

zbMATH Keywords

complexity; tree automata; games; logics of programs

Mathematics Subject Classification ID

68Q45: Formal languages and automata

03B45: Modal logic (including the logic of norms)

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Deciding the unguarded modal -calculus, Expressiveness and succinctness of a logic of robustness, Unnamed Item, Unnamed Item, Unnamed Item, A Decision Procedure for CTL* Based on Tableaux and Automata, Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints, Branching-time logics with path relativisation, A survey of stochastic \(\omega \)-regular games, A tableau-based decision procedure for CTL\(^*\), Complexity of synthesis of composite service with correctness guarantee, On aggregation of normed structures, On the equivalence of recursive and nonrecursive Datalog programs, The average running time of an algorithm as a midpoint between fuzzy sets, A unifying semantics for time and events, Compactness and finite dimension in asymmetric normed linear spaces, On the proof theory of the modal mu-calculus, Determinization and memoryless winning strategies, Games for synthesis of controllers with partial observation., Mathematical modal logic: A view of its evolution, Sublogics of a branching time logic of robustness, CTL\(^\ast\) with graded path modalities, On the expressive power of hybrid branching-time logics, Hierarchical cost-parity games, Program schemata technique for propositional program logics: a 30-year history, Aggregation of asymmetric distances in computer science, Model checking for hybrid branching-time logics, The model checking fingerprints of CTL operators, Compositional construction of most general controllers, A goal-directed decision procedure for hybrid PDL, Compositional analysis for verification of parameterized systems, To be fair, use bundles, A survey on temporal logics for specifying and verifying real-time systems, Unnamed Item, Decidability and Expressivity of Ockhamist Propositional Dynamic Logics, Branching Time? Pruning Time!, Parameterized Algorithms for Parity Games, The complexity space of partial functions: a connection between complexity analysis and denotational semantics, The Modal μ-Calculus Caught Off Guard, The mu-calculus and Model Checking, Program Schemata Technique to Solve Propositional Program Logics Revised, A Tableau for Bundled Strategies, EXPTIME Tableaux for the Coalgebraic μ-Calculus, On the Complexity of Branching-Time Logics