@TechReport{	  it:2006-052,
  author	= {Parosh Aziz Abdulla and Noomene Ben Henda and Giorgio
		  Delzanno and Ahmed Rezine},
  title		= {Regular Model Checking without Transducers (On Efficient
		  Verification of Parameterized Systems)},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2006},
  number	= {2006-052},
  month		= dec,
  note		= {To appear in the proceedings of TACAS 2007},
  abstract	= {We give a simple and efficient method to prove safety
		  properties for parameterized systems with linear
		  topologies. A process in the system is a finite-state
		  automaton, where the transitions are guarded by both local
		  and global conditions. Processes may communicate via
		  broadcast, rendez-vous and shared variables. The method
		  derives an over-approximation of the induced transition
		  system, which allows the use of a simple class of regular
		  expressions as a symbolic representation. Compared to
		  traditional regular model checking methods, the analysis
		  does not require the manipulation of transducers, and hence
		  its simplicity and efficiency. We have implemented a
		  prototype which works well on several mutual exclusion
		  algorithms and cache coherence protocols.}
}