“Beyond each corner new directions lie in wait.”
|--(Stanislaw Lec, 1909–1966)|
SPIN is based on the fact that we can use finite state automata to model the behavior of asynchronous processes in distributed systems. If process behavior is formalized by automata, the combined execution of a system of asynchronous processes can be described as a product of automata.
Consider, for instance, a system A of n processes, each process given in automaton form, say: A1, A2, . . ., An. Next, consider an LTL formula f and the Büchi automaton B that corresponds to its negation ¬f. Using the automata theoretic verification procedure, we can check if A satisfies f by computing the global system automaton S
We use the operator ∏ here ...