@TechReport{	  it:2003-024,
  author	= {Parosh Aziz Abdulla and Bengt Jonsson and Marcus Nilsson
		  and Julien d'Orso},
  title		= {Algorithmic Improvements in Regular Model Checking},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2003},
  number	= {2003-024},
  month		= apr,
  note		= {Extended version of paper accepted for publication in in
		  CAV'2003},
  abstract	= {Regular model checking is a form of symbolic model
		  checking for parameterized and infinite-state systems,
		  whose states can be represented as finite strings of
		  arbitrary length over a finite alphabet, in which regular
		  sets of words are used to represent sets of states. In
		  earlier papers, we have developed methods for computing the
		  transitive closure (or the set of reachable states) of the
		  transition relation, represented by a regular
		  length-preserving transducer. In this paper, we present
		  several improvements of these techniques, which reduce the
		  size of intermediate approximations of the transitive
		  closure: One improvement is to pre-process the transducer
		  by {\em bi-determinization}, another is to use a more
		  powerful equivalence relation for identifying histories
		  (columns) of states in the transitive closure. We also
		  present a simplified theoretical framework for showing
		  soundness of the optimization, which is based on commuting
		  simulations. The techniques have been implemented, and we
		  report the speedups obtained from the respective
		  optimizations.}
}