Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints

. As a case study, we apply a constraint-oriented state-based proof methodology to Fischer's protocol. The method exploits compositionality and abstraction to reduce the investigated verification problem. This reduction avoids state space explosion. Key concepts of the reduction process are modal constraints, separation of proof obligations, Skolemization and abstraction. Formal basis for the method are Timed Modal Specifications (TMS) allowing loose state-based specifications, which can be refined by successively adding constraints. TMS's can be easily translated into Modal Timed Automata, thus enabling automatic verification. A central issue of the method is the use of Parametrized TMS's. 1 Introduction The use of state-based formal methods -- in particular formal verification of concurrent systems -- is still limited to very specific problem classes, mainly due to the state explosion problem: the state graph of the system grows exponentially with the number of its parallel compone..