Jan 22, 2013: Gijs Kant: Partial Model Checking for Linear Process Specifications

January 22, 2013Partial Model Checking for Linear Process Specifications
Room: Zi 5126Gijs Kant
12:30-13:30

The talk is about Partial Model Checking, introduced by Andersen [1] in 1995 and extended by Lang & Mateescu [3].

Partial Model Checking here means that checking whether a formula φ holds for a compositional system P1 || P2 || ... || Pn is reduced to checking whether a formula φ' holds for the smaller system P2 || .. || Pn. This new formula φ' is the result of a translation and is called the quotient of the formula φ for process P1. The main bottleneck is the size of the computed quotient formula, that may capture all of the behaviour of P1. In [3] a lot of effort is put in simplification of the quotient formula.

We extend the work on partial model checking by defining it for Linear Process Specifications (LPSs) [2] and do the quotienting on a symbolic level. 

The idea is to compute the quotient formula φ' such that not for every concrete state in the LPS a new variable (and associated subformula) is introduced for every state, but that the state is encoded in the parameters of the variable. This is quite natural, as states in LPSs are encoded in the data parameters of the processes.
The benefit of this approach would be that symbolic reduction/simplification is possible on the level of the formula or on the level of the PBES that encodes the game P |= φ.

This is still work in progress. Comments and suggestions are welcome.

 

References

  1. Henrik Reif Andersen. Partial Model Checking. LICS 1995. IEEE, 1995. doi:10.1109/LICS.1995.523274
  2. J.F. Groote and T.A.C. Willemse. Model-checking processes with data. Science of Computer Programming, 56(3), 2005. doi:10.1016/j.scico.2004.08.002
  3. Frédéric Lang and Radu Mateescu. Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems. TACAS 2012, LNCS 7214, 2012. doi:10.1007/978-3-642-28756-5_11