Gergely Kovasznai, H. Veith, Andreas Fröhlich, Armin Biere,
"On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic"
: Proc. 39th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS'14), Serie Lecture Notes in Computer Science (LNCS), Vol. 8635, Springer, Seite(n) 481-492, 2014
Original Titel:
On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 39th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS'14)
Original Kurzfassung:
We study the complexity of decision problems encoded in
bit-vector logic. This class of problems includes word-level model checking,
i.e., the reachability problem for transition systems encoded by bitvector
formulas. Our main result is a generic theorem which determines
the complexity of a bit-vector encoded problem from the complexity
of the problem in explicit encoding. In particular, NL-completeness of
graph reachability directly implies PSpace-completeness and ExpSpace-
completeness for word-level model checking with unary and binary arity
encoding, respectively. In general, problems complete for a complexity
class C are shown to be complete for an exponentially harder complexity
class than C when represented by bit-vector formulas with unary encoded
scalars, and further complete for a double exponentially harder
complexity class than C with binary encoded scalars. We also show that
multi-logarithmic succinct encodings of the scalars result in completeness
for multi-exponentially harder complexity classes. Technically, our
results are based on concepts from descriptive complexity theory and
related techniques for OBDDs and Boolean encodings.
Forschungs-