About the expressive power of CTL combinators

DOI10.1016/0020-0190(95)00053-FzbMath0875.68632OpenAlexW2027418885MaRDI QIDQ672975

François Laroussinie

Publication date: 28 February 1997

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

Full work available at URL: https://doi.org/10.1016/0020-0190(95)00053-f

zbMATH Keywords

CTLTemporal logicSpecification languagesProgram specification

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (7)

Adequate Sets of Temporal Connectives in CTL ⋮ Model checking abilities of agents: a closer look ⋮ On the expressiveness of TPTL and MTL ⋮ Easy Yet Hard: Model Checking Strategies of Agents ⋮ The Complexity of Satisfiability for Fragments of CTL and CTL⋆ ⋮ THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆ ⋮ The model checking fingerprints of CTL operators

Cites Work

• A hierarchy of temporal logics with past
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• Unnamed Item
• Unnamed Item

This page was built for publication: About the expressive power of CTL combinators