Quantified CTL: Expressiveness and Complexity

DOI10.2168/LMCS-10(4:17)2014zbMath1448.68304arXiv1411.4332MaRDI QIDQ2938770

François Laroussinie, Nicolas Markey

Publication date: 15 January 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1411.4332

zbMATH Keywords

model checkingexpressivenesstree automatatemporal logics

Mathematics Subject Classification ID

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

Related Items (15)

\(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers ⋮ On Composing Finite Forests with Modal Logics ⋮ To be announced ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ Augmenting ATL with strategy contexts ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Second-order propositional modal logic: expressiveness and completeness results ⋮ Unnamed Item ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ Quantifying Bounds in Strategy Logic ⋮ On Temporal and Separation Logics ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ Verification of multi-agent systems with public actions against strategy logic ⋮ Good-for-Game QPTL: An Alternating Hodges Semantics

This page was built for publication: Quantified CTL: Expressiveness and Complexity