DEMOCTL1.m

Contents

Introduction

Computational-Tree Logic is a temporal logic for formally specifying and verifying dynamic properties of finite state machines. A CTL formula has the following form

 s = A p | E p | <ap>
 p = X s | G s | F s|  s1 U s2 | s1 R s2

where s is called a state formula (which specifies the property of a state) and p is called a path formula (which specifies the property of a path of execution of the finite state mathine. The meaning of the quantifiers stands for:

Path quantifiers:

Temporal quantifiers

For example AG "safe" specifies that the atomic proposition "safe" is always globally true for a state s. Meaning that starting from s, property "safe" is always true along every path of execution. As a second example example AF "ready" specifies that starting from the current state, every path will eventually leads to a state where "ready" is true.

Data structure

ACTL package uses global variables to specify the finite state machine, it is stored in a global variable called "GLOBAL_TRANSITION". The variable is a cell array, each cell correspond to a state. And the content of that cell is a vector consisting of the destination states of the out-going transitions from that state. For example, consider the following structure.

The transition system shown above will be modeled as

clear global
global GLOBAL_TRANSITION
GLOBAL_TRANSITION = {[2 3], 3, 2};

An atomic proposition is modeled as a region object, which represents a set of states. The set of atomic propositions of the system are put in a global variable called "GLOBAL_AP". Besides the user-defined atomic propositions, it has to containt two trivial atomic propositions, "true" for all states in the system and "false" for an empty set.

global GLOBAL_AP
GLOBAL_AP.true = region(3, 'true');
GLOBAL_AP.false = region(3, 'false');
GLOBAL_AP.f = region(3, [2 3]);
GLOBAL_AP.g = region(3, 2);

Model checking

As a preprocess step, we need to compute the reverse transition system. This is used in the model checking algorithm together with the original transition system.

global GLOBAL_REV_TRANSITION
GLOBAL_REV_TRANSITION = revtran(GLOBAL_TRANSITION);

Next we check two properties, AG f and AF g.

a = model_check('AG f')

Total states: 3
States in region: 	2	3

We can check the result in the following way. Starting from 2, we can see that the system can only make transitions between 2 and 3, which are both in f. Hence f is globally true. But since 1 is not in f, AG f is not true for state 1.

b = model_check('AX AG f')

Total states: 3
States in region: All

We add the AX clause, it specifies that AG f is true for the next state. Starting from state 1 it either goes to state 2 or three, for which the property AG f is true. Hence AX AG f is true for state 1. It can be easily verified it is true for states 2 and 3.

c = model_check('AF g')

Total states: 3
States in region: All

Note that starting from any state, the system will always reach state 2, for which g is true. Hence AF g is true for all states.

Plotting transition system

There are some auxillary routines to facilitate viewing the transition system.

write_dot('result1.dot'); % writes the transition system to a DOT file
dotdraw('result1.dot','png'); % This requires the AT&T graphviz binary files on the MATLAB path
imshow('result1.png')

To plot the transition system in MATLAB figure. Use the following command.

figure;
hold on;
axis([0 1 0 1]);
coord = rand(3,2); % generate random coordinate for the states
plot_tran(coord); % plot transition system using the coorinate
movingrectangle; % allowing the user to move the states using mouse

References

[1] M. R. A. Huth and M. D. Ryan, "Logic In Computer Science: Modeling and reasoning about systems", Cambridge University Press, 2001.

[2] E. M. Clarke Jr, O. Grumberg and D. A. Peled, "Model Checking", The MIT Press, 2001.

Published with MATLAB® 7.5