Sciweavers

IANDC
2010

Underapproximation for model-checking based on universal circuits

13 years 2 months ago
Underapproximation for model-checking based on universal circuits
For two naturals m, n such that m < n, we show how to construct a circuit C with m inputs and n outputs, that has the following property: for some 0 ≤ k ≤ m, the circuit defines a k-universal function. This means, informally, that for every subset K of k outputs, every possible valuation of the variables in K is reachable. Now consider a circuit M with n inputs that we wish to model-check. Connecting the inputs of M to the outputs of C gives us a new circuit M with m inputs, that its original inputs have freedom defined by k. This is a very attractive feature for underapproximation in model-checking: on one hand the combined circuit has a smaller number of inputs, and on the other hand it is expected to find an error state fast if there is one. We show a random construction of a k-universal circuit that guarantees that k is very close to m, with an arbitrarily high probability. We also present a deterministic construction of such a circuit, but here the value of k is smaller ...
Arie Matsliah, Ofer Strichman
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where IANDC
Authors Arie Matsliah, Ofer Strichman
Comments (0)