From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Mon Apr 18 2005 - 14:01:27 MDT
>>>>> "JD" == Junkie Dolphin <junkie.dolphin_at_libero.it> writes:
JD> Hello everyone,
JD> when bounded_model_check returns "formula undecided", but zchaff
JD> has died trying to SAT-solving some CNF (for example, because it
JD> tried to malloc() too much memory, and so on), the undecidability
JD> of the formula is simply due to the abortion of zchaff, or one
JD> can say it is a "true" undecidability?
LTL properties are decidable for finite models. When BMC says
"undecided" it's because it could not come to a conclusion within the
allotted limits. These limits may be explicitly specified (via the -k
option) or may arise from memory or CPU limitations. In all cases,
including when the SAT solver runs out of memory, an LTL property can
be proved, in theory, by checking for sufficiently long paths.
(Again, we are talking about finite models.)
Fabio
This archive was generated by hypermail 2.1.7 : Mon Apr 18 2005 - 14:10:28 MDT