### Abstract

This paper introduces a technique for localizing model checking of
concurrent state-based systems. The technique, called partial
model checking, isfully automatic and performs model checking by
gradually specializing the specification with respect to the
concurrent components one by one,computing a `concurrent weakest
precondition.' Specifications are invariance properties and the
concurrent components sets of transitions. Bothare expressed as
predicates represented by Reduced Ordered Binary Decision Diagrams
(ROBDDs). The self-reducing properties of ROBDDs areimportant for
the success of the technique. We describe experimental results
obtained on four different examples.

Original language | English |
---|---|

Title of host publication | Proceedings of TACAS'97, LNCS 1217 |

Place of Publication | Berlin,Heidelberg |

Publisher | Springer Verlag |

Publication date | 1997 |

Pages | 35-49 |

Publication status | Published - 1997 |

Event | TACAS'97, Tools and Algorithms for the Construction and
Analysis of Systems - Enschede, Netherlands Duration: 1 Jan 1997 → … |

### Conference

Conference | TACAS'97, Tools and Algorithms for the Construction and Analysis of Systems |
---|---|

City | Enschede, Netherlands |

Period | 01/01/1997 → … |

## Cite this

Andersen, H. R., Maretti, N., & Staunstrup, J. (1997). Partial Model Checking with ROBDDs. In

*Proceedings of TACAS'97, LNCS 1217*(pp. 35-49). Springer Verlag.