The Complexity of Tree Automata and Logics of Programs
From MaRDI portal
Publication:4268874
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)
Formal languages and automata (68Q45) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (52)
Compactness and finite dimension in asymmetric normed linear spaces ⋮ Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints ⋮ Compositional analysis for verification of parameterized systems ⋮ The mu-calculus and Model Checking ⋮ A focus system for the alternation-free \(\mu \)-calculus ⋮ A Tableau for Bundled Strategies ⋮ Program Schemata Technique to Solve Propositional Program Logics Revised ⋮ Branching Time? Pruning Time! ⋮ Unnamed Item ⋮ Determinization and memoryless winning strategies ⋮ To be fair, use bundles ⋮ Branching-time logics with path relativisation ⋮ Deciding the unguarded modal -calculus ⋮ Parameterized Algorithms for Parity Games ⋮ Expressiveness and succinctness of a logic of robustness ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ A survey on satisfiability checking for the \(\mu \)-calculus through tree automata ⋮ Games for synthesis of controllers with partial observation. ⋮ A survey of stochastic \(\omega \)-regular games ⋮ A tableau-based decision procedure for CTL\(^*\) ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ Hierarchical cost-parity games ⋮ On aggregation of normed structures ⋮ Mathematical modal logic: A view of its evolution ⋮ Program schemata technique for propositional program logics: a 30-year history ⋮ Unnamed Item ⋮ Temporal logics with language parameters ⋮ Sublogics of a branching time logic of robustness ⋮ The complexity space of partial functions: a connection between complexity analysis and denotational semantics ⋮ On the equivalence of recursive and nonrecursive Datalog programs ⋮ The Modal μ-Calculus Caught Off Guard ⋮ On the expressive power of hybrid branching-time logics ⋮ Temporal Logic with Recursion. ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Decision Procedure for CTL* Based on Tableaux and Automata ⋮ Aggregation of asymmetric distances in computer science ⋮ Temporal logics with language parameters ⋮ CTL\(^\ast\) with graded path modalities ⋮ The average running time of an algorithm as a midpoint between fuzzy sets ⋮ Model checking for hybrid branching-time logics ⋮ Unnamed Item ⋮ On the proof theory of the modal mu-calculus ⋮ Unnamed Item ⋮ Temporal logic with recursion ⋮ EXPTIME Tableaux for the Coalgebraic μ-Calculus ⋮ On the Complexity of Branching-Time Logics ⋮ The model checking fingerprints of CTL operators ⋮ Decidability and Expressivity of Ockhamist Propositional Dynamic Logics ⋮ Compositional construction of most general controllers ⋮ A goal-directed decision procedure for hybrid PDL ⋮ A unifying semantics for time and events
This page was built for publication: The Complexity of Tree Automata and Logics of Programs
