CHECKMATE VERIFICATION TOOL

1 Introduction

CheckMate implements the verification technique that conservatively approximates the original hybrid system model by purely discrete and finite models called quotient transition systems or approximating automata. The verification is initiated by typing the command verify in the MATLAB command window. The verification process in CheckMate follows the flow diagram shown on the left.
 
The CheckMate verification procedure is implemented in the m-file verify.m located in the directory ~/approximation. The m-file can be invoked from the MATLAB command window.

The class of hybrid systems that can be modeled in CheckMate front end is called the threshold-event-driven hybrid systems (TEDHS). The verification process starts by the conversion of the Simulink model into an equivalent model called a polyhedral-invariant hybrid automaton (PIHA). The resulting PIHA is discretized to form a quotient transition system (QTS) by an initial partition that is constructed according to the parameters specified by the user. Transitions between states in the QTS are computed using the continuous reachability analysis technique called the flow pipe approximations. The QTS is then verified against the ACTL specification using standard model checking technique for finite-state transition systems. Since the verification may fail due to the coarseness of the hybrid system approximation by the QTS, the partition for the QTS can be refined to give a tighter approximation. After the partition refinement, the flow pipe approximation is used to redefined the transitions in the QTS. The process repeats until the QTS satisfies the specification or the user chooses to terminate the verification. The subsequent sections describe each step of the verification in more detail.

Verification Overview

2 Models of Hybrid Systems

In order to understand how CheckMates works, the user should familiarize oneself with two models of hybrid systems, the threshold-event-driven hybrid systems (TEDHS) and the hybrid automata, which are the bases for modeling and analysis in CheckMate, respectively.

2.1 Threshold-event-driven Hybrid Systems (TEDHS)

A threshold-event-driven hybrid system consists of three types of subsystems, the switched continuous  system (SCS), the threshold event generator (TEG), and the finite state machine (FSM).  Without loss of generality we assume that there is only one subsystem of each type as shown in figure below. Multiple subsystems of the same type can be reduced into a single subsystem by vectorizing the input and output signals.


Threshold-event-driven Hybrid System

The SCS is the continuous dynamics systems that takes in the discrete-valued input u and produces its continuous state vector x as the ouput. The continuous dynamics for x evolves according to the differential equation or differential inclusions selected by the discrete input u as shown in the above figure. The output of the SCS is fed into the TEG, which produces an event when a component of the vector function g of x crosses its corresponding threshold from the specified direction (rising, falling, or both). The event signals from the TEG drives the discrete transition in the FSM whose output, in turn, drives the continuous dynamics of the SCS.

2.2 Hybrid Automata

A hybrid automaton, shown below, is a generalization of the finite automaton that includes continuous dynamics in with each discrete state. Each discrete state in the hybrid automaton is called a location. Associated with each location is the invariant, the condition which the continuous state must satisfy while the hybrid automaton resides in that location, and the flow equation representing continuous dynamics in that location.

Hybrid Automaton

Transitions between locations are called edges. Each edge is labeled with the guard and the reset conditions on the continuous state. The location transition is enabled, i.e. allowed to be taken, when the guard condition is satisfied. Upon the location transition, the values of the continuous state before and after the transition must satisfy the reset condition.


Location Transition in a Hybrid Automaton

2.3 Polyhedral-Invariant Hybrid Automata

In general, the analysis of hybrid automata can be very difficult. In CheckMate, we restrict our attention to a subclass of hybrid automata called polyhedral-invariant hybrid automata (PIHA). A polyhedral-invariant hybrid automaton is a hybrid automaton with the following restrictions:

Polyhedral-Invariant Hybrid Automaton

3 Simulink Front End

The modeling front end for CheckMate is built on top of Simulink to take advantage of it simulation capability. While numerical simulations cannot guarantee the correct operation of the systems under all possible circumstance, the user can learn a great deal about the behaviors of the system and evaluate wheter the possibly lengthy verification should be attempted. CheckMate uses the following customized (masked) blocks in Simulink to model the three components of the TEDHS discussed previously.

3.1 Switched Continuous System Block (SCSB)

A switched continuous system block (SCSB) represents a continuous system whose dynamics for the continuous variable x depends on the value of the discrete input u, i.e. the continuous dynamics is of the form
.
Currently, 3 types of continuous dynamics can be specified for each value of the discrete input u. They are shown in the table below.
 
Type
Description
'clock' Continuous dynamics of the form where c is a constant vector.
'linear' Continuous dynamics of the form where A and b are constant nxn matrix and nx1 vector, respectively.
'nonlinear' General continuous dynamics dynamics of the form .

See Using CheckMate Verification Tool for detail on how to specify the parameters for an SCSB.

3.2 Polyhedral Threshold Block (PTHB)

A polyhedral threshold block (PTHB) represents a polyhedral region Cx <= d in the continuous space of the input variable x. The output is a binary signal indicating whether x is inside the region or not, i.e. whether the condition Cx <= d is true. See Using CheckMate Verification Tool for detail on how to specify the parameters for a PTHB.

3.3 Finite State Machine Block (FSMB)

A finite state machine block (FSM) represents a finite state transition system driven by the event and data input. It is implemented by the regular Stateflow block with the following restrictions: See Using CheckMate Verification Tool or the CheckMate models in the ~/demo directory for examples of FSMBs that comply with the above rules.

A sample CheckMate diagram is shown below.

4 TEDHS to PIHA Conversion

Although TEDHS support block diagram modeling, which is a very intuitive way to model hybrid systems, much of the theoretical work in the field of hybrid systems has been developed using the hybrid automaton framework. Thus, CheckMate converts the TEDHS in the Simulink front-end into an equivalent PIHA (up to the analysis region) before performing any further analysis for the hybrid systems. The conversion, as implemented in the m-file piha.m, proceeds as follows.
 
The procedure for converting the TEDHS in the front end into a PIHA is implemented in the m-file piha.m located in the directory ~/frontend/@piha. The m-file is implemented as the constructor for the object class 'piha' but the return variable is never treated as an object in the subsequent code in verify.m. Instead the PIHA is converted into a regular structure variable so that its fields can be accessed directly. Implementing the object class 'piha', however, could prove useful when composition of multiple PIHA is considered in the future.

4.1 Verifying the Model Syntax

In this step the function piha() calls the subroutine check_model_syntax() to make sure that the Simulink model that the user enters belongs to the class of hybrid systems that CheckMate can handle.
 
Disclaimer: The function check_model_syntax() is not completed yet. The user needs to make sure that the Simulink model conforms to the rules outlined in the previous section. 

4.2 Compiling the List of Blocks and Threshold Hyperplanes

Next, the function piha() creates the list of SCSBs, FSMBs, and PTHBs found in the Simulink model. CheckMate goes through the list of PTHBs and extract all the hyperplanes contained in the rows of the (C,d) matrix-vector pair associated with each PTHB. Since each PTHB may not be connected to all SCSBs, the columns of the matrix C is rearranged and augmented with zero columns to obtain the new C matrix that corresponds to the cross product of the continuous state spaces from the SCSBs in the order compiled earlier.
 
Each block in the Simulink model is an object identified by a unique number called a handle. Simulink has its own system of assigning the object handles which is separated from the handle systems of MATLAB standard GUI and Stateflow. Using the function get_param() and set_param(), the user can manipulate various properties of a Simulink object.

4.3 Partitioning the Analysis Region into Cells by the Threshold Hyperplanes

CheckMate limits its scope of analysis to the bounded region in the continuous state space called analysis region. A bounded convex analysis region must be specified as one of the parameters for each SCSB. The overall analysis region is first computed from the cross product of all SCSB analysis regions (in the order obtained in Section 3.2) then partitioned by the threshold hyperplanes into cells. The figure below shows an example of the analysis region partitioning by three hyperplanes.

Analysis Region Partitioning by Threshold Hyperplanes

Threshold hyperplanes are introduced into the partition one by one in each stage of the partitioning. In each stage, the partition information is maintained in a tree structure with the whole analysis region at the root as shown in the figure below.


Analysis Region Partition Tree (Animated)

The tree is expanded when a hyperplane is introduced by spliting the leaf nodes as needed. In our examples, the hyperplanes are introduced in the ascending numerical order. Once all hyperplanes are introduced, the leaf nodes consitutes the cells in the analysis region partition as shown in the above figure. The same figure without the animation is reproduced below so that the reader can examine the final tree structure more carefully.


Analysis Region Partition Tree

After the partitioning is completed, the leaf nodes (the cells) are intersected with the initial continuous sets (augmented for the full continuous statespace) from SCSBs. The cells that overlap with the initial continuous sets are called the initial cells. These are the cells from which the continuous trajectory of the hybrid system may originate.

Note that we need not consider any subtree for which the hyperplane does not pass through the polytope of the root node. Thus, using the tree structure can improve efficiency of the partitioning process significantly in the case where the number of threshold hyperplanes is large. The same kind of efficiency can be achieved when finding the initial cells by traversing the partition tree and ignore the subtree for which the root node does not overlap with the initial continuous set.

The tree should be as balanced as possible for the analysis region partitioning or the initial cell intersection algorithm to be most efficient. Thus, before the analysis region partitioning begins, the hyperplanes are sorted so that the ones that are most centered with respect to the analysis region are introduced first. To do this, we introduce the quantity called the normalized deviation (not a standard term in literature) which is a non-negtive number that measures the centered-ness of each hyperplane with respect to the analysis region. The smaller the normalized deviation, the more centered that hyperplane is with respect to the analysis region.

CheckMate maintains the following information about the each cell in the analysis region partition.
 

boundary the indices to hyperplanes (in the list compiled earlier) constituting the cell boundary
hpflags an array of boolean flags, one for each hyperplane ciTx = di in the list, indicating whether the inequality ciTx <= di is true when the continuous state x of the hybrid system lies in the cell.
pthflags an array of boolean flags, one for each PTHB in the list compiled earlier, indicating the output value of the corresponding PTHB when the continuous state of the hybrid system lies in the cell.
neighbors indices to other neighboring cells. Note that for any two neighboring cells, their hpflags must be different by exactly one hyperplane.
The reader is referred to the m-file partition_ss.m in the directory ~/frontend for more information on the analysis region partitioning.

4.4 Compiling the Information on FSMBs

By tracing the Simulink block diagram, CheckMate computes the strings containing the expressions for all event and data signals for all FSMBs in terms of the outputs of the all PTHBs and FSMBs. For example, consider the partial Simulink diagram shown below

with the event and data signals for each Stateflow (FSM) block listed in the following table.
 
Block
Events
Data
fsm1
v1 v2
d1 d2
fsm2
v3
d3 d4

CheckMate will produce the following results for the expressions of all event and data signals. For the block fsm1,

v1 = 'pth1'
v2 = 'pth2 | pth3'
d1 = 'pth1'
d2 = '2 ~= fsm2'
For the block fsm2,
v3 = 'pth3'
d3 = 'fsm1'
d4 = 'pth1'
Note that once the values are assigned to the variables with the same names as the PTHBs and FSMBs, the value of the event and data signals can be evaluated using the command eval in MATLAB (see MATLAB on-line help for more detail). This is indeed what CheckMate does to evaluate the event and data signals later on the PIHA conversion process. To evaluate whether changes in the event signals actually produces any event, CheckMate also maintains the information on the type of each event which could be rising edge, falling edge, and either edge.

The initial FSM states are the states which are the destination of the default transition in the Stateflow diagram for each FSMB. The current implementation of CheckMate allows only one default transition per Stateflow block, that is, the initial state for each FSMB is deterministic.

4.5 Building PIHA Locations

A location in our target PIHA is a pair (p,q) where p is the index to a cell in the analysis region partition obtained in Section 4.3 and q is a vector of FSM states in the order determined in Section 4.2. In other words, a location in the PIHA keeps track the cell the continuous state of the hybrid system is currently residing in and current states of the FSMBs which determines the continuous dynamics.

4.5.1 Initial Locations

Locations from which the hybrid automaton may start are called the initial locations. In our target PIHA, these are locations with the cell that overlaps with the initial continuous set and the FSM state vector that corresponds to the initial states of the FSMBs in the Simulink diagram. Specifically, the initial locations are constructed from the cross product of the initial cells found in Section 4.3 and initial FSM state vector found in Section 4.4.

4.5.2 Location Transitions and Locations Construction

Starting from the current set of locations, CheckMate finds new locations by exploring the location transitions out of the current locations. New locations are added until the fixed-point is reached, i.e. no new location is found. This iterative approach to constructing the PIHA locations is used to, although not always effective, avoid the explosion in the number of locations resulting from all possible combinations of cell and FSM state vector.

The location transitions in the PIHA are determined as follows. For each location (p1,q1), the cell p1 serves as the location invariant (see Section 2.2). The number of outgoing transitions from the location are the same as the number of hyperplanes on the boundary (faces) of p1. To determine the destination of the transition for each hyperplane hi, we first compute the event that can occur in the FSMBs when the continuous trajectory leaves the cell p1 through the hyperplane hi. Recall that each cell in the analysis region partition uniquely determines the output of all PTHBs when the continuous trajectory resides in that cell. Thus, all event signals can be computed by comparing the values of PTHB outputs in the cells before and after crossing the hyperplane hi. There are three possible cases as illustrated in the figure shown below.


Determining Location Transitions

4.6 Data Structure Summary

The above PIHA conversion procedure in the m-file verify.m produces a global variable called GLOBAL_PIHA in the main work space. The document on the data structure of GLOBAL_PIHA can be found in the file piha_structure.txt located in the directory ~/frontend/@piha. The content of the piha_structure.txt is reproduced here for convenience.

--------------------------------
Data structure for a PIHA object
--------------------------------

A PIHA object, HA, obtained after the conversion from a C/E system consists of
the following fields:

   HA.Hyperplanes          : List of threshold hyperplanes in the C/E system
   HA.NAR                  : Number of hyperplanes on analysis boundary
   HA.InitialContinuousSet : Set of initial continuous states
   HA.InitialDiscreteSet   : Set of initial discrete states
   HA.Cells                : List of cells in the continuous state space
                             partition
   HA.InitialCells         : List of cells which overlaps with the initial
                             continuous set
   HA.Locations            : List of hybrid automaton locations
   HA.InitialLocations     : Indices to initial locations
   HA.SCSBlocks            : List of switch continuous system blocks in the
                             C/E system
   HA.PTHBlocks            : List of polyhedral threshold blocks in the C/E
                             system
   HA.FSMBlocks            : List of finite state machine blocks in the C/E
                             system

The data structure for each field is described below.

(1) Hyperplanes
---------------

Threshold hyperplanes from all PTHBs and the analysis region AR are collected
in this field. The field is a cell array of hyperplane structures, each with
the following format

   Hyperplanes{i}.pthb  : -1 if it belongs to analysis region AR, otherwise
                          it is the index to the parent PTHB in PTHBlocks
   Hyperplanes{i}.index : The hyperplane index within the parent PTHB
   Hyperplanes{i}.c     : Vector and constant pair representing the hyperplane
   Hyperplanes{i}.d     : c*x = d

(2) NAR
-------

This field is an integer indicating the number of hyperplanes on the analysis
region boundary. The first NAR hyperplanes in the Hyperplanes list are the
hyperplanes from the analysis region.

(3) InitialContinuousSet
------------------------

A linearcon object with parameters CE,dE,CI, and dI representing the initial
continuous set

   CE*x  = dE
   CI*x <= dI

(4) InitialDiscreteSet
----------------------

A cell array of initial discrete states. Each initial discrete state (cell
element) is a vector of state indices for FSMBlocks in the same order as in
FSMBlocks list.

(5) Cells
---------

A cell array of "cells" in the partition of the continuous state space. Each
cell is a structure of the following format

   Cells{i}.boundary  : A vector of indices to hyperplanes in Hyperplanes list
                        that comprises the boundary of the ith cell.
   Cells{i}.hpflags   : A vector of the same length as the Hyperplanes list.
                        hpflags(j) is a boolean flag indicating the side of
                        the jth hyperplane in Hyperplanes list in which the
                        cell lies. Specifically,
                           hpflags(j) = 1 --> c_j*x <= d_j
                           hpflags(j) = 0 --> c_j*x >= d_j
                        for any x in the ith cell.
   Cells{i}.pthflags  : A vector of the same length as the PTHBlocks list.
                        pthflags(j) is a boolean flag indicating the output
                        value of the jth PTHB in PTHBlocks list for any x
                        in the ith cell.
   Cells{i}.neighbors : A vector of indices to the neighboring cells.

(6) InitialCells
----------------

A vector of indices to the continuous state space cells in the field Cells
that overlaps with the initial continuous set.
 

(7) Locations
-------------

A cell array of locations, each with the following format
   LOCATIONS{i}.p           : Index to a continuous cell in the field Cells
   LOCATIONS{i}.q           : A vector of discrete state numbers (same format
                              as each element of InitialDiscreteSet)
   LOCATIONS{i}.transitions : A cell array of location indices. transitions{j}
                              indicates the destination location(s) for the
                              location transition taken when the continuous
                              trajectory exits through the jth hyperplane of
                              on the boundary of the cell p.

                              transitions{j} is a structure array with each
                              elements containing 2 field 'type' and 'value'

                              If crossing the jth hyperplanes means
                              leaving the analysis region, then
                              transition{j} contains a single element with
                              the following field values
                                type: 'out_of_bound'
                                destination: []

                              If crossing the jth hyperplane may lead to
                              a "terminal" FSM state q' (a state for
                              which there is no transition out of any
                              of the component states), then
                              transition{j} contains an element with the
                              following field values
                                type: 'terminal'
                                destination: q'
                              where q' is a row FSM state vector

                              For each regular location transition,
                              transition{j} contains an element with the
                              following field values
                                type: 'regular'
                                destination: idx
                              where idx is the destination location index
                              (a scalar)
 

(8) InitialLocations
--------------------

A vector of indices to the locations in the field Locations that are the
initial locations.

(9) SCSBlocks
-------------

A cell array of switched continuous system blocks, each with the following
format

   SCSBlocks{i}.name        : Name of the ith SCSB
   SCSBlocks{i}.nx          : Number of continuous variables
   SCSBlocks{i}.nu          : Number of discrete inputs
   SCSBlocks{i}.swfunc      : Name of the switching function m-file
   SCSBlocks{i}.fsmbindices : A vector of indices to FSMBs in the FSMBlocks
                              fields in the order that feeds into the input
                              of the block SCSBlock{i}.

(10) PTHBlocks
--------------

A cell array of polyhedral threshold blocks, each with the following format

   PTHBlocks{i}.name : Name of the ith PTHB.

Name of PTHBs will be used as atomic propositions for CTL verifications.

(11) FSMBlocks
--------------

A cell array of finite state machine blocks, each with the following format
   FSMBlocks{i}.name   : Name of the ith FSMB.
   FSMBlocks{i}.states : A cell array listing the discrete states in the ith
                         FSMB by name.

5 Quotient Transition Systems

A quotient transition system (QTS) is a finite state transition system that is a conservative approximation of the hybrid system. A QTS is defined from a partition of the state space of the hybrid system with each state in the QTS corresponding to a member of the partition. In the QTS, a transition is defined from a state (a set) P1 to another state P2 if and only if there is a state p2 in P2 that is reachable from a state p1 in P1 in the original hybrid system. The figure on the right illustrates the QTS where T denotes the hybrid system which makes transitions between states according to its dynamics and T/P denotes the QTS of T defined from the partition P of the state space of T.

A QTS is a conservative approximation in the sense that for every trajectory in the original hybrid system, there is a trajectory in the QTS corresponding to the set of states that the trajectory in the hybrid system goes through. Thus, if we can verify that all trajectories in the QTS satisfy some property, we can conclude that all trajectories in the hybrid system also satisfy the same property.

CheckMate only pays attention to the behavior of the hybrid system at the switching instants. Thus, approximates the QTS for the hybrid system from the partition of the switching surfaces, which are the boundaries of the location invariants in the PIHA, and the set of continuous initial states. The reachability analysis used to define the transitions in the QTS is performed using the approximation method called the flow pipe approximations, discussed in the next section. The heuristics for choosing the initial partition is also discussed in a later section. The actual data structure for the quotient transition system, also called approximating automaton, is described in the m-file iauto_part.m in the directory ~/approximation.

6 Flow Pipe Approximations

To compute a QTS for a PIHA, it is necessary to compute the set of reachable states under the continuous dynamics for a given location of the PIHA. We consider the problem of computing the reachable sets under the three types of continuous dynamics discussed previously.

6.1 Clock Dynamics

For systems with simple continuous dynamics such as the linear hybrid automata, the reachable set can be computed easily. In a linear hybrid automaton, the continuous dynamics in any location is of the form  where F is a constant polyhedron. In this case, the reachable set from any polyhedral initial set is also a polyhedron which can be obtained by projecting the initial set in all possible directions for the derivative as shown below. In CheckMate, the reachable seta for the 'clock' continuous dynamics are also computed using this technique (see the m-file clk_reach.m in the directory ~/approximation/flowpipe/clock).

6.2 Nonlinear Dynamics

The reachable sets for more general continuous dynamics can only be approximated. CheckMate uses the flow pipe approximation technique to approximate the reachable sets under ordinary differential equation by a sequence of convex polyhedra. The method starts by dividing the reachable set into time segments and approximates each the reachable set for each segment by enclosing it in a bounded convex polyhedron, called a polytope, as shown in the figure below.
Each reachable set segment S is approximated by the following steps:
 

1.Choose the set of enclosing direction vectors.

2. Solve the optimization problem
to obtain the supporting hyperplane for each of the direction vector obtained in step 1. The intersection of all non-positive half-spaces of the supporting hyperplanes is the approximation to each reachable segment.

For the reachble set between time [tk,tk+1], the optimization problem in step 2 can be posed as

where x(t,x0) denotes the solution to the differential equation from the initial state x0 at time t and X0 denotes the set of initial states. CheckMate solves this optimization problem by using the optimization toolbox in MATAB and embedding the numerical simulation of ODEs inside the objective function computation (see the m-file seg_approx_ode.m in the directory ~/approximation/flowpipe/nonlinear). We note that since the optimization problem in non-convex in general, local optimization routines in MATLAB cannot guarantee the global optimum.

6.3 Linear Dynamics

For 'linear' (affine) dynamics , the above optimization problem is solve a bit differently. We first observe that the reachable set at any time is an affine transformation of the initial set X0
.
We rewrite the optimization problem as
.
Since X0 is a polyhedron Rt(X0) is also a polyhedron and the inner optimization problem is a linear program. Note that we can at least guarantee the global optimum for the inner optimization problem in this case. See the m-file seg_approx_lin.m in the directory ~/approximation/flowpipe/linear for the implementation of the optimization for linear systems.

For linear systems, we do not have to solve the optimization problems for each time segment as we have the following result that the flow pipe segment can be obtained by transforming another segment with the same time step Dt.

CheckMate only solves the optimization problems for the first reachable segment and then transforms it the get the subsequent segments in its computation of the reachable sets. An example of the flow pipe computations in CheckMate is shown below where the red rectangle is the initial set.
The flow pipe approximation is used to define transitions in the quotient transition system for the PIHA as follows. A state in the quotient transition system is a triple (p,p,q) where p is a polytope in the location (p,q) of the PIHA. For each state in the quotient transition system, the flow pipe is computed for the associated polytope under the associated continuous dynamics. The mapping set, the set of states on the invariant boundary that can be reached from p is computed. A transitiion is then defined from (p,p,q) to any other state whose polytope overlaps with the mapping from p, as illustrated below. See the m-file compute_mapping.m in the directory ~/approximation for more information on the mapping set computation and the m-files iauto_build.m and rauto_tran.m in the same directory for the computation of the transitions in the quotient transition system (called the approximating automaton in the code).

7. Initial Partition

The faces of the invariant for each location q of the PIHA are partitioned using the following heuristics. The heuristics is based on the direction and variation of the continuous vector field on each face and the size of the polytope on each face. The basic idea is to partition each face of the invariant recursively until each polytope in the partition satisfies the following criteria: The first two criteria are intended to group continuous states with similar qualitative behavior together. The third criterion is aimed at getting the QTS that is a good approximation of hybrid system model. The three criteria are implemented through the use of tolerances on the vector field direction, vector field variation, and the size of polytope, as depicted below.

The user specifies these tolerances in the parameter files that CheckMate references during the verification process (see Using CheckMate Verification Tool). The above heuristics for partitioning the invariant faces is implemented for each type of the continuous dynamics in the m-files clock_partition.m, linear_partition.m, and nonlinear_partition.m in the directory ~/approximation/partition.

The heuristics for splitting a polytope in CheckMate follows the following general steps:

  1. Choose a split direction c. For a polytope of dimension n-1, c is usually chosen to be orthogonal to the normal vector to the polytope. Particular criteria for choosing c can be found in the m-files mentioned above.
  2. Solve two linear program to find the supporting hyperplanes in the c direction which bound the polytope P, as shown in the figure below.
  3. Split the polytope P by the hyperplane that lies in the middle of the two supporting hyperplanes.


Disclaimer: The initial continuous set is partitioned using the same heuristics if it is of dimension n-1, i.e. same dimension as the invariant faces. Similar heuristics may be generalized to partition polytopes of other dimensions. However, this remains a future work. Currently, no partitioning is done for polytopes of dimensions other than n-1 in the m-file iauto_part.m in the directory ~/approximation.

After using the above heuristics, the invariant face partitions are partitioned further with the polytopes obtained from the reachability analysis from each initial continuous set. Roughly, this additional partitioning schemes proceeds as follows.

This step is done so that the paths (sequences of states) in the QTS reflects For further information, see the m-file iauto_part.m in the directory ~/approximation.

8. ACTL Verification

8.1 Computation Tree Logic

This section briefly describes the formulation of the computation tree logic (CTL)  and the subclass of CTL called ACTL, which CheckMate uses as the framework for specification and verification. Given a finite-state transition system, a set of boolean properties, called the atomic propositions, are attached to each state of the transition system. Unfolding the state transition graph from a given initial state, we obtain an infinite tree called the computation tree. The concept of a computation tree is illustrated below.
Finite-State Transitiion System
Computation Tree
Computation tree logic is a language that is used to specify the system evolution in terms of the truth values of the atomic propositions along the paths of the computation tree. A CTL formula consists of temporal operators and path quantifiers. Temporal operators specify the system evolution along a single path of the computation tree. There are four basic temporal operators, X, F, G, and U. The temporal operator X ("next time") asserts that the property holds at the next state in the path. F ("in the future") asserts that a property holds at some state in the future (including the current state). G ("globally") asserts that a property holds globally, i.e. at every state along the path. The operator U ("until") invloves two properties. The assertion f U g requires that g holds at some state in the future (including the current state) and that f holds at every state along the path prior to the occurrence of g. Path quantifiers A and E specify whether the path assertion holds along all paths or some ("there exists") path in the computation tree, respectively. The following table summarizes the aforementioned CTL operators.
Path Quantifiers
Temporal Operators
A
E
For all computation paths
For some compution paths
F
G
X
U
In the future
Globally
Next time
Until
Formally, the syntax of a CTL formula f is given by the grammar
 
CTL Grammar:   f  --> ap, ~f, f & f, f | f, AX f, AF f, AG f, A fUf, EXf,EFf,EG f, E fUf

where ap denotes an atomic proposition and ~, &, and | denote logical not, and, and, or, respectively. CheckMate only considers a subclass of CTL called ACTL which is given by the grammar
 

ACTL Grammar:   f  --> ap, ~ap, f & f, f | f, AX f, AF f, AG f, A fUf

Note that only the universal path quantifier A is allowed in an ACTL formula. This is due to the fact that CheckMate uses the conservative approximations (the quotient transition systems) to verify properties of the hybrid system. One can conclude that the original hybrid system satisfies the specification from the conservative approximation only when a universal specification (a specification which requires that a certain property holds for all behaviors of the system) is used. We give a few examples of the ACTL expressions.

Given a CTL specification and a finite-state transition system, the verification problem, also called the model checking problem, is formulated as
 
Model Cheking Problem:Find the set of states where the given CTL formula is true.

The above problem can be solved by performing the reachability analysis on the finite-state transition graph using well-known graph search algorithms. The reader is referred to the m-files in the directory ~/ACTL for the implementation of the model checking algorithms in CheckMate.

8.2 Atomic Propositions in CheckMate

CheckMate allows the user to make assertions on the whereabouts of both the continuous and discrete states (x,u) of the Simulink model in their respective state spaces by specifying them as atomic propositions in an ACTL formula. There are two forms of atomic propositions in CheckMate, which are summarized in the following table.
 
Syntax
Description
Truth Value
PTHB
PTHB is the name of a PTHB in the Simulink diagram. True iff the output of the block PTHB is 1 for the given continuous state x of the Simulink model.
FSMB == state
FSMB is the name of an FSMB in the Simulink diagram and state is the name of a state in the Stateflow diagram for the block FSMB. True iff state is the active state of the block FSMB for the given discrete state u of the Simulink model.

9.0 Partition Refinement

If the verification on the current quotient transition system fails due to the coarseness of the discretization, the user has an option to refine the partition, construct the next QTS, and attempt the verification again. To slow down the state explosion resulting from the refinement, CheckMate only refine states which satisfies one of the following criteria: The above criteria are motivated by the following reasonings. For the first criterion, there is no need to refine a state if it only has one behavior, always going to a single destination state, since no new information is gained by doing so. For the second criterion, recall that the ACTL specification is universal. Thus, all behaviors from the initial states that satisfy the specification are the QTS is guaranteed to satisfy the specification in the hybrid system. Thus, the verification result cannot be improved by refining these initial states and their descendants.

The following refinement scheme is used in CheckMate for each state that is to be refined:

The above refinement scheme is designed to separate the polytope for each state into the parts that can be reached from different combinations of the source states. It is implemented in the function refine_face_state() in the m-file refine_auto.m in the directory ~/approximation.