Published on 2014-11-24


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 realized. 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.

The language of well formed formulas for CTL is generated by the following grammar:

CTL Grammer

Compare to LTL, CTL also have path operatiors:

  • the All operator A
    The formula * A p* specifies p has to hold on all paths starting from the current state.
  • the Exists operator E
    The formula * E p* specifies there exists at least one path starting from the current state where p holds.

And the semantics of CTL is:

CTL Semantics

The following figure might be helpful to understand the semantics.

CTL Understand


About Syntax & Semantics

About State Variables

  • Atom: any sequence of characters in the set {a-z, A-Z, 0-9, _, -}, beginning with a alphabetic character.
  • Instance of Module Atom: an atom optionally followed by a list of expressions in parentheses [].
  • Process: keyword process causes the atom to be a instantiated module as an asynchronous process. A process will be chosen by the program non-deterministically and the assignment statements in it will be executed in parallel.
  • Identifiers: an id is an atom, or id.atom, or id[exp].

About Modules

A module is an encapsulated collections of declarations. Once defined, a module can be reused as many times as necessary. Modules can also be parameterized, so that each instance of a module can refer to different data values. A module can contain instances of other modules, allowing a structural hierarchy to be built.

Note that the parameters of a module is called by reference.

There must be one module with the name main and no formal parameters. The module main is the one evaluated by the interpreter.

Our Limitation

For later use, we add some limitation to SMV.

The modules are classified into several categories.

  • Structures: modules only contain variable declarations, and optional initialization of the variables.
  • Transitons: modules only contain assignments which specifies transitions with a guard-assignment form, usually parameterized.
  • Main: the main module which contains all process.


Given a set of observations (x1, x2, …, * xn), where each observation is a *d-dimensional real vector, k-means clustering aims to partition the n observations into k (≤ n) sets S = {S1, S2, …, Sk} so as to minimize the within-cluster sum of squares (WCSS). In other words, its objective is to find:

*k*-means object

where μi is the mean of points in Si.

Standard Algorithm

The structure of standard k-means algorithm is

1. Choose k points as initial means called centroid
2. repeat
3.    k clusters are created by associating every observation with the nearest mean.
4.    The centroid of each of the k cluster becomes the new mean.
5. until convergence has been reached

This algorithm is initialization sensitive.