The CheckMate Functions

Introduction

Although CheckMate is useful as a fully automatic tool for verifying hybrid systems, in practice it is sometimes difficult to make sure that a CheckMate model can be successfully verified. The reason ranges from highly involved issues such as the computational complexity to extremely trivial use of variable names. For example, if a SCSB block name has space in it, sometimes the explore code failed due to the fact that CheckMate is trying to a variable in the workspace with the same name. Since the developement of CheckMate is essentially inactive, we have described in this page a few useful (and very basic) functionalities of CheckMate, which can help the user to debug or use CheckMate as a toolbox instead of using it as a fully automatic verification tool.

The CheckMate code consists of five parts

The ACTL and Polylib are lower level functions. These functions can normally be invoked alone from MATLAB command line. The front-end, exploration and verification are higher level functions, which can be used only with CheckMate models. It is difficult to use these functionalities alone. However, the mid-level funcationalities for reachability analysis can be used as stand-alone functions, which are also documented in this page.

ACTL functions

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

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:

For example, AG "safe" specifies that the atomic pr oposition "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. Please refer to the books at the end of this section for an extensive discussion on CTL and ACTL.

Finite Transition System

In CheckMate, the finite transition system is modeled in the global variable GLOBAL_TRANSITION. The variable is a cell array, each element correspond to the out-going transition of that state. The element is a vector consisting of the destination states of the out-going transitions. For example, consider the transition system shown in the following figure.

The transition system has three states. State 1 has transitions to 2 and 3. State 2 to 3 and State 3 to 2. The transition system can be modeled in CheckMate using the following MATLAB code.
>> global GLOBAL_TRANSITION;
>> GLOBAL_TRANSITION = {[2 3], 3, 2};

Region

Next we define a region object in CheckMate. A region object represents a subset of a finite set of states. The following command construct a set of all states of a three-state set.
 
>> a = region(3, 'true');
Variable a consists of all three states 1, 2, 3, which is the universe for the 3-state transition system.
 
>> b = region(3, 'false');
Variable b consists of no states, which is the empty set.
 
>> c = region(3, [1 2]);
Variable c consists of states 1,2 out of a three-state set. A region object can be viewed either as a subset or equivalently as a boolean expression. Region object supports basic set operations, such as intersection (and), union (or), and compliment (not).

Model Checking

In CheckMate, it is necessary to first construct the atomic propositions of the formula to verify. Each atomic proposition in the ACTL formula must be put in the global variable GLOBAL_AP. ". Besides the user-defined atomic propositions, it has to contain two trivial atomic propositions, "true" for all states in the system and "false" for an empty set. The following code construct the global atomic proposition for a three-state system, f consists of state 2 and 3, and proposition g consists of state 2 only.
>> 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);
As a preprocess step, it is necessary to construct the reverse transition system. This is used in the model checking algorithm together with the original transition system. In CheckMate, the reverse transition system is stored in the global variable GLOBAL_REV_TRANSITION. The following command construct the reverse transition system.
>> global GLOBAL_REV_TRANSITION
>> GLOBAL_REV_TRANSITION = revtran(GLOBAL_TRANSITION);
The model checking routine assumes that
  1. A transition system (GLOBAL_TRANSITION) and reverse transition system (GLOBAL_REV_TRANSITION) is available
  2. All the atomic propositions (GLOBAL_AP) in the given ACTL formula are available
The model checking algorithm can be invoked via:
>> a = model_check('AX AG f')

The return argument a is a region object consists of the states where the forumula is true. The command model_check first parse the ACTL formula and then evaluate the ACTL formula by traversing the parse tree of the specification and evaluate each node in a bottom-up manner. A detailed reference of the implementation can be found in [2].

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

Polylib: a library for polyhedra computation

CheckMate uses closed convex polyhedra, i.e., polytopes, to represent sets in the continuous states. A polytope can either be represented as the intersection of a number of closed halfspaces or as the convex hull of a finite set of points. Note that an intersection of a finite set of closed halfspaces may not be a polytope, since it may be unbounded. On the other hand, the convex hull of a finite number of points may not be a full-dimensional polytope. For example, the convex hull may be a line segment if all the points happen to be on the line segment. To avoid confusion and facilitate the computation, three classes are implemented in CheckMate:

Conversion

Each object can be converted to other object using the constructor.

Linearcon and polyhedron are both used to represent polytopes. The conversion is just converting from one representation to the other representation of the set. One limitation is that when a linearcon is used to represent open polytope, the result can be unexpected: Either error or wrong result can be found.

Vertices objects are essentially different from linearcon or polyhedron. When constructing a linearcon or polyhedron object from a vertices object, a convex over-approximation of the set of point is computed. Depending on the underlying algorithm, CheckMate may compute either a convex hull or a rectangular hull of the set of point.

The following example illustrates the differences between the convex hull and oriented rectangular hull. Suppose we have three points (0,0), (0,1) and (1,0), the convex hull is the red triangle shown in the following figure and the rectangular hull is the blue box. To generate the plot, use the following command in MATLAB. For an extensive discussion of rectangular hull, see [1]. The convex hull algorithm of CheckMate relies on the qhull built-in functions in MATLAB.

NOTE The global variable GLOBAL_APPROX_PARAM is used in polylib, which should first be set to use the library.

 
GLOBAL_APPROX_PARAM = parameters(0);
global GLOBAL_APPROX_PARAM
a = vertices([0 0; 0 1; 1 0]')
a1 = polyhedron(a)
GLOBAL_APPROX_PARAM.hull_flag = 'convexhull';
a2 = polyhedron(a);
plot(a1);
plot(a2, 'r');
Converting a set to a vertices object will result in the set of vertices of the polytope. This is done by enumerating all the extremal points (vertices) of the polytope. CheckMate uses a version of CDD ([3]) implementation for enumerating all the vertices.

Computation with linearcon

Although all three classes are implemented for set operations, only linearcon is the workhorse for set computation. For continuous set in n-D space, CheckMate only support sets in n-D or (n-1)-D polytopes. Polytopes with dimension less than n-1 is either considered as empty or over-approximated by an n-d polytope. Polyhedron and vertices are normally first converted to linearcon objects and then converted back after the set computations. The most commonly used computations on sets are

[1] B. H. Krogh and O. Stursberg, On efficient representation and computation of reachable sets for hybrid systems, in Hybrid Systems: Computation and Control (HSCC'03), Lecture Notes in Computer Science (LNCS), Springer.

[2] Qhull website: http://www.qhull.org

[3] CDD website: http://www.ifor.math.ethz.ch/~fukuda/cdd_home/cdd.html

Reachability analysis of CheckMate

The reachability analysis of CheckMate involves the computation of continuous successor of a given location of a PIHA. Given a polyhedral invariant (note it can be unbounded), the continuous dynamics given in the format of Matlab ODE suite, and an initial set given as a bounded, full-dimensional polytope. CheckMate computes what can be informally called consinuous successor, i.e., the intersection of the flow-pipe (from 0 to a given t_max) with the facets of the invariant.

Limitation of CheckMate

Note that in the above description, the continuous successor is merely an over-approximation of the continuous part of actual reach set. Consider the situation illustrated in the following figure, the continuous successor computed from CheckMate is illustrated as the bold line segment. The invariant I is the shaded area in the figure. Consider one of the trajectory in the flow, the state first reaches the boundary of the invariant, where the hybrid system leaves the location. The trajectory after that does not exist because the dynamics depends on the new location. Therefore the parts illustrated by the red curve does not belong to the reach set. One may argue that this can be done by intersecting the reach set in each small time step, or even taking the vector field into consideration. In CheckMate, this intersection is not implemented to avoid the complexity of set computation (intersection of polytopes). The actual reach set should only contain the lower half of the line segment (below the dashed trajectory). But CheckMate computes the whole line segment as an over-approximation.

The reachability analysis algorithms have the form

 xxx_map( sys, X0, I, T, T_max )
where sys gives the system dynamics, X0 is the initial state polytope, I is the polyhedral invariant set, T is the step size and T_max is the maximum analysis time. Depending on the dynamics of the location, CheckMate implments three different procedures to compute the continuous successors

The main difference between these algorithms are the input parameters for the functions and the underlying algorithms. The input/output format for these functions are quite similar. The global variable GLOBAL_APPROX_PARAM has to be set to use these functions.

Affine dynamics

In affine dynamics, the system ODE is given as

 f(x) = A* x + b
. The procedure fs_lin_map takes A and b as input arguments. A sample code to use fs_lin_map is shown as the following

%DEMO2 A 2-D reach set demo script 
global GLOBAL_APPROX_PARAM
GLOBAL_APPROX_PARAM = parameters(1);
GLOBAL_APPROX_PARAM.T = 1e-2; % time step 

% Construct the invariant for x_1 < 1 
INV = linearcon([],[],[1 0],[1]); 

A = [-1 1; 0 -1];
b = [1 2]';
X0 = linearcon([],[],[eye(2); -eye(2)],1e-2*[1;1;1;1]);
% Compute continuous successor for the system
[MAPPING,null_event,time_limit] = fs_lin_map(A,b,X0,INV)

Nonlinear dynamics

In nonlinear dynamics, the system ODE is given as general nonlinear function f(x). The procedure fs_nonlin_map takes the function handle to f(x) as one of the input arguments. Where function f(x) must be implemented in the format of MATLAB ODE suite. A sample code to use fs_nonlin_map is shown as the following

%DEMO2 A 2-D reach set demo script 
global GLOBAL_APPROX_PARAM
GLOBAL_APPROX_PARAM = parameters(1);
GLOBAL_APPROX_PARAM.T = 1e-2; % time step 

% Construct the invariant for x_1 < 1 
INV = linearcon([],[],[1 0],[1]); 

X0 = linearcon([],[],[eye(2); -eye(2)],1e-1*[1;1;1;1]);
% Compute continuous successor for the system
mapping = fs_nonlin_map(@dblclk,[],X0,INV,linearcon,0.1,2)

Clock dynamics

In clock dynamics, the system ODE is given as constant rates. The procedure clk_map takes the rates of the state variables as one of the input arguments. CheckMate assumes t_max is infinity for clock dynamics. And no step size is used. A sample code to use clk_map is shown as the following

%DEMO2 A 2-D reach set demo script 
global GLOBAL_APPROX_PARAM
GLOBAL_APPROX_PARAM = parameters(1);
GLOBAL_APPROX_PARAM.T = 1e-2; % time step 

% Construct the invariant for x_1 < 1 
INV = linearcon([],[],[1 0],[1]); 

X0 = linearcon([],[],[eye(2); -eye(2)],1e-1*[1;1;1;1]);
v = [1;2];
% Compute continuous successor for the system
mapping = clk_map(X0,v,INV);