Jan 22, 2013: Gijs Kant: Partial Model Checking for Linear Process Specifications
January 22, 2013  Partial Model Checking for Linear Process Specifications 
Room: Zi 5126  Gijs Kant 
12:3013: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. This is still work in progress. Comments and suggestions are welcome.
References
