Fast Cone-Of-Influence Computation and Estimation in Problems with Multiple Properties

This paper introduces a new technique for a fast computation of the Cone-Of-Influence (COI) of multiple properties. It specifically addresses frameworks where multiple properties belongs to the same model, and they partially or fully share their COI. In order to avoid multiple repeated visits of the same circuit sub-graph representation, it proposes a new algorithm, which performs a single topological visit of the variable dependency graph. It also studies mutual relationships among different properties, based on the overlapping of their COIs. It finally considers state variable scoring, based on their own COIs and/or their appearance in multiple COIs, as a new statistic for variable sorting and grouping/clustering in various Model Checking algorithms. Preliminary results show the advantages, and potential applications of these ideas.