## 2014-11-24

Published on 2014-11-24## CTL

*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:

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:

The following figure might be helpful to understand the semantics.

## SMV

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

*k*-Means

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

where *μ _{i}* is the mean of points in

*S*.

_{i}### 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*.