Appendix A. Automata Products
“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 ...
Get Spin Model Checker, The: Primer and Reference Manual now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
