The challenge
MC tries to solve the problem of System
?
|= Spec which is undecidable
(Rice).
OK, all real systems are finite and thus decidable be enumerating all
possible states.
A simple example: 64 Bytes RAM
state space size: 2
512
Suppose we need 1mSec per state space
⇒ 2
512
≈ 13, 4 · 10
157
mSec
Age of the universe < 14 billion years (44 ∗ 10
19
mSec approx.)
. . .
Alexander Asteroth (BRSU:CS) BuK2:MC 3 / 57
