The power of first-order quantification over states in branching and linear time temporal logics

DOI10.1016/J.IPL.2004.05.003MaRDI QIDQ2390310zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Pallab Dasgupta, P. P. Chakrabarti

Publication date 21 July 2009

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2004.05.003

zbMATH Keywords

verificationmodel checkingformal methodslinear temporal logic

Mathematics Subject Classification ID

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

Recommendations

• Quantified computation tree logic
• On the expressivity and complexity of quantitative branching-time temporal logics
• Quantified CTL: expressiveness and complexity
• scientific article; zbMATH DE number 1512710
• Augmenting branching temporal logics with existential quantification over atomic propositions

Cites work

• scientific article; zbMATH DE number 3922633 (Why is no real title available?)
• scientific article; zbMATH DE number 1059247 (Why is no real title available?)
• Augmenting branching temporal logics with existential quantification over atomic propositions
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Quantified computation tree logic
• Results on the propositional \(\mu\)-calculus
• The complexity of propositional linear temporal logics

Cited in

(1)

• The expressive power of the temporal query language \(L_{\mathcal H}\)

This page was built for publication: The power of first-order quantification over states in branching and linear time temporal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2390310)