Branching-time logics repeatedly referring to states

DOI10.1007/s10849-009-9093-xzbMath1193.03034OpenAlexW2017460625MaRDI QIDQ1047801

Volker Weber

Publication date: 6 January 2010

Published in: Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10849-009-9093-x

zbMATH Keywords

complexityhybrid logictemporal logicsatisfiabilityalternating tree automataCTLbranching time logicpebble automatasymmetric automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44) Combined logics (03B62)

Related Items (3)

The complexity of satisfiability for fragments of hybrid logic. I. ⋮ Model checking for hybrid branching-time logics ⋮ Expressiveness of Hybrid Temporal Logic on Data Words

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity of hybrid logics over transitive frames
• A hierarchy of temporal logics with past
• The temporal logic of branching time
• 25 years of model checking. History, achievements, perspectives
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Domino-tiling games
• Specification in CTL + past for verification in CTL.
• Model checking hybrid logics (with an application to semistructured data)
• Hybrid logics: characterization, interpolation and complexity
• LTL with the freeze quantifier and register automata
• Bounded-Variable Fragments of Hybrid Logics
• “Sometimes” and “not never” revisited
• Computer Science Logic
• The Complexity of CTL* + Linear Past

This page was built for publication: Branching-time logics repeatedly referring to states