The model checking fingerprints of CTL operators

DOI10.1007/s00236-018-0326-9zbMath1423.68288arXiv1504.04708OpenAlexW2885823445MaRDI QIDQ2317834

Arne Meier, Martin Mundhenk, Andreas Krebs

Publication date: 13 August 2019

Published in: Acta Informatica (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

The model checking fingerprints of CTL operators

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An \(\mathsf{AC}^{1}\)-complete model checking problem for intuitionistic logic
• About the expressive power of CTL combinators
• A near-optimal method for reasoning about action
• Number of quantifiers is better than number of tape cells
• The complexity of short two-person games
• Propositional dynamic logic of regular programs
• The model checking fingerprints of CTL operators
• Erratum: The Complexity of Satisfiability for Fragments of CTL and CTL^⋆
• The tractability of model checking for LTL
• Model Checking CTL is Almost Always Inherently Sequential
• Alternating-time temporal logic
• The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions
• The Complexity of Generalized Satisfiability for Linear Temporal Logic
• THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL⋆
• A taxonomy of problems with fast parallel algorithms
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• Alternation
• The Complexity of Tree Automata and Logics of Programs
• The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)