CTML/asCTML Application

Computation Tree Measurement Language (CTML) is a backend analysis engine for the dependability and performance evaluation of computer systems such as database system, network communication system, software system, distributed systems, etc..

asCTML stands for Action and State based CTML (asCTML). It is an extension of CTML for answering additional queries that involve sequence of traces with edges.

Currently, the theoretical work as well as tools for both CTML and asCTML are done, but looking into various applications for practical experiments.

CTML vs. PLTL in Theory and Practice

PLTL stands for Probabilistic Linear Temporal Logic which is widely known for its application in parallel systems. CTML covers a nontrivial sublanguage of PLTL that cannot be expressed by an existing probabilistic model checking logic by far. Theoretically, it shows that CTML runs polynomial time in the size of an input formula and model, whereas the overal time complexity of PLTL is exponential in the size of an input formula and polynomial in the size of the model. For this project, we intend to investigate in applications where CTML does give significant advantages in run time as well as space.