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

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

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