In  this  paper, we apply   a  compositional proof technique  to  an
  automatic    verification of  the  correctness  of  Fischer's mutual
  exclusion protocol. It is  demonstrated that the technique may avoid
  the  state--explosion problem.    Our   compositional technique  has
  recently been implemented in  a tool CMC\footnote{CMC: Compositional
    Model Checking},  which verifies the protocol  for  50 processes within
  172.3 seconds  and  using only 32MB main  memory.    In contrast all
  existing verification tools for timed  systems will suffer from  the
  state--explosion problem, and no tool has to our knowledge succeeded
  in verifying the protocol for more than $11$ processes.