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 | View the thread | More toots from pervognsen@mastodon.social
text/geminiThis content has been proxied by September (3851b).