摘要：We propose a new and practical framework for integrating the behavioral reasoning about distributed systems with model-checking methods. Our proof methods are based on trace abstractions, which relate the behaviors of the program and the specification. We show that for finite-state systems such symbolic abstractions can be specified conveniently in Monadic Second-Order Logic (M2L). Model-checking is then made possible by the reduction of non-determinism implied by the trace abstraction. Our method has been applied to a recent verification problem by Broy and Lamport. We have transcribed their behavioral description of a distributed program into temporal logic and verified it against another distributed system without constructing the global program state space. The reasoning is expressed entirely within M2L and is carried out by a decision procedure. Thus M2L is a practical vehicle for handling complex temporal logic specifications, where formulas decided by a push of a button are as long as 10-15 pages.
