Model Checking

NuSmv (http://nusmv.fbk.eu/) is a symbolic model checker tool based of Model Checking theory. This latter, is a set of techniques to check the correctness of reactive systems like operation on database, operating systems tasks or any other job that require a continuous processing.

Model checking is an automatic technique that requires only the model of the task to check.  If the model is wrong, the model checker is able to return the counterexample in order to show which is the unexpected behaviour.

Let me show you an example: Shared / Exclusive Locking

The shared exclusive lock is a locking protocol used for serveral purpose like in DMBS item locking , or Kernel resources locking and so on. The purpose of this protocol is to make possible solely to read a resource when this resource is locked in read mode and avoid to read or write the resource if it is already locked in write mode.

This is the conflict matrix:

	Read	Write
Read	Y	N
Write	N	N

Below the NuSmv code:

MODULE main                                    
 VAR   
         
     rqueue_bool  : boolean;
      x_lock : {unlocked, write_locked, read_locked};
                                    
   t1 : process transaction(x_lock,rqueue_bool);             
   t2 : process transaction(x_lock,rqueue_bool);
  

    INIT x_lock=unlocked & rqueue_bool=FALSE;

---------------------------------------------------------------------
-----------------  CTL LANGUAGE ------------------------
---------------------------------------------------------------------

------ Conflict matrix for SHARED/EXCLUSIVE LOCK
------
------           _Read__Write_
------ Read  |___Y__|___N__|
------ Write  |___N__|__ N__|
------      

-- Impossible to W   when the itam is  W
SPEC  AG  !(t1.state =write_lock & t2.state =write_lock);   
SPEC  AG  !(t1.state =writing & t2.state =writing);   
    -- Impossible to W when the itam is R
SPEC  AG  !(t1.state =write_lock & t2.state =read_lock);   
SPEC  AG  !(t1.state =writing & t2.state =reading);   


-- Impossible R when the itam is W
SPEC  AG  !(t1.state =read_lock & t2.state =write_lock);   
SPEC  AG  !(t1.state =reading & t2.state =writing);


-- Possibile  to R when the item is R
SPEC  EF (t1.state =read_lock &  t2.state =read_lock);
-- counterexample
SPEC  AG !(t1.state =reading &  t2.state =reading);

 


MODULE transaction(x_lock,rqueue_bool)                         
 VAR                                           
   
   state   :{write_lock ,read_lock , wait, writing,reading};
 INIT             
      state = wait;
     
     
 ASSIGN 
 next (state) :=
  case

         -- if a transaction is waiting and item is not locked
         -- then the transaction can make read_lock/write_lock        
state = wait        & x_lock = unlocked                          : {read_lock,write_lock};
       
        -- if a transaction is waiting and the item is read locked 
        -- then the trasaction can only make  read_lock       
state = wait    & x_lock =read_locked                        : read_lock;
       
        -- if a transaction is in waiting and the item is locked in write mode then
        -- the transaction goes in wait
        state = wait    & x_lock =write_locked                    : wait;

        -- When a transaction is in read_lock then in the next state it must be in reading
        state = read_lock                                       : reading;

        -- When a transaction is in write_lock then in the next state it can go in reading or writing
        state = write_lock                                                        : {writing,reading};
        -- When a transaction is in reading o writing the in the next state it must be in wait
        state = writing | state = reading                             : wait;                
     
      TRUE :state;
  esac;
 
  next (x_lock) :=
  case
            -- If the next transaction state is read_lock then the item must be locked  in read mode 
            next(state) = read_lock   :read_locked;
            -- if the next transaction state is write_lock then the item must be locked in write mode
            next(state) = write_lock  :write_locked;
 
             -- if the transaction wrote/red the item then in the next state the transaction has to release the lock
            (state = writing | state = reading) &
            x_lock = write_locked & next(state) = wait  :unlocked;
             -- if the transaction wrote/read the item can release the lock only if no other transaction are locking it
            state = reading & x_lock = read_locked &  next(state) = wait & !rqueue_bool  :unlocked;
      TRUE :x_lock;
  esac;
 
  --- no_of_reads:
  next (rqueue_bool) :=
      case
            x_lock = read_locked & next(state)  = read_lock  :TRUE;
            x_lock = read_locked & next(state)  = wait  :FALSE;
              TRUE: rqueue_bool;
  esac;
 
 
FAIRNESS
    running      

Reinforcement Learning

Reinforcement Learning

Reinforcement Learning is an area of Machine Learning that provides to the computer applications a way to mimic a human behaviour. It is based on concept of reward the Agent who has to do something. Usually any realistic task is a very hard task for an Agent, because it doesn't understand what it is doing. In fact he has to learn the task from scratch. To grasp the sense of what we are talking about, one can imagine a baby who has to learn to stand up. Usually a baby need more than 15 month before he starts this task and during this learning phase a lot of trials are needed to accomplish the task.

Actually, what the baby brain is trying to do in this phase is to training his neural network in order to understand which is the right combination of spikes to send through the  spianal column. It's easy to suppose that this task is a very hard task,because no instructions are provided to the baby but only the genetic can cause this kind of self learning. The way to learn to stand up is to know what can happen if the baby falling down. He feels pain when he is down and he feels good when he is stand up. So the key of this learning is the negative or positive reward. In same way one can imagine a horse that receive a sugar cube when it had accomplished any task in order to communicate to horse that it did something well.

For an Agent try to find the way out from a maze could be a hard task too. The only information that it knows is that it can move up,down,left or right and that it can't go through a wall. If it reaches a cell with an apple then it receive a positive reward and if it try to pass on a wall then it receive a negative reward. This mechanism is the same raw technique used from a unware man or girl who try to departure from a maze where he is never been before.
  
Qmaze is a project realized attending Intelligent Systems course that try to simulate the learning explained above. It uses the Qlearning algorithm and initially it blindly explores some cells  until it finds the first time the apple(exit or Terminal State). In the next episode again it tries to explore the maze  but if it finds cells that are a part of way out then it exploits them.

To show how it works I make some video of the agent in action:

 

The Agent in action (in this instance a blue-ball) is trying to find two different Terminal States with diffent reward. So the Agent has to learn first of all the way to the apples and then choose the apple with major reward.