Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties.

PropertyValue
dbpprop:abstract
  • Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties. It is in a class of temporal logics that include linear temporal logic.
  • Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, die speziell zur Spezifikation und Verifikation von Computersystemen dient. Meist wird sie auch mit CTL* bezeichnet. CTL bezeichnet dann eine spezielle Teilmenge der CTL*-Formeln. Eine weitere wichtige spezielle Teilmenge von CTL* ist die Linear Time Temporal Logic (kurz LTL). Wie allgemein bei temporalen Logiken geht es nicht um die Beschreibung von zeitlichen Abläufen (dies wäre die Real Time Logik), sondern um die Eigenschaften von Zuständen und deren Änderung in Systemabläufen. CTL* ist dabei eine Erweiterung der Aussagenlogik.
  • 計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。
dbpprop:reference
rdfs:comment
  • Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realised. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers which determine if a given artifact possesses safety or liveness properties.
  • Die Computation Tree Logic (kurz CTL) ist eine Temporale Logik, die speziell zur Spezifikation und Verifikation von Computersystemen dient. Meist wird sie auch mit CTL* bezeichnet. CTL bezeichnet dann eine spezielle Teilmenge der CTL*-Formeln. Eine weitere wichtige spezielle Teilmenge von CTL* ist die Linear Time Temporal Logic (kurz LTL).
  • 計算木論理（けいさんきろんり、Computational Tree Logic、CTL）は、分岐時相論理の一種である。その時間モデルでは未来は決定されておらず木構造のように分岐している。未来の複数の経路のうちの1つが実際に現実の経路となる。
rdfs:label
  • Computation tree logic
  • Computation Tree Logic
  • 計算木論理
skos:subject
foaf:page
is dbpprop:redirect of