I hadn't really thought about it in those terms, but the implementation of bounded model checking is very similar to the proof of the Cook-Levin theorem. You encode the nondeterministic transition relation of your model of computation as a formula in propositional logic, unroll it to some fixed depth (given by the polynomial-time bound in the case of Cook-Levin), and check for satisfiability of the unrolled transition relation formulas and an auxiliary formula.
=> More informations about this toot | More toots from pervognsen@mastodon.social
To do the first step (encode the transition relation in propositional logic) you need to unroll in space, not just in time. In the case of Cook-Levin that relies on the usual argument that TIME(f(n)) is a subset of SPACE(f(n)) since the Turing machine's tape head starts in a fixed position, so the nondeterminism is only for the transitions. In model checking I think they usually allow an arbitrary initial-state predicate, so I guess for BMC you'd have to constrain that as well.
=> More informations about this toot | More toots from pervognsen@mastodon.social
(If the tape head starts in a fixed initial position then within time T you can only access tape cells within distance T of that initial position, so there's no need to encode instances of the transition relation corresponding to machine states beyond the "light cone" emanating from the initial position.)
=> More informations about this toot | More toots from pervognsen@mastodon.social
By the way, I like the space-time variant of the standard proof that van Emde Boas gives in https://people.irisa.fr/Francois.Schwarzentruber/sif2_thx/articles/tiling.pdf. "Basing the proof on the space-time diagram, uniqueness of the head position is a direct consequence of local consistency throughout the diagram and does not have to be enforced explicitly."
=> More informations about this toot | More toots from pervognsen@mastodon.social
text/geminiThis content has been proxied by September (ba2dc).