@TechReport{	  it:2003-001,
  author	= {Parosh Abdulla and Johann Deneux and Pritha Mahata and
		  Aletta Nyl{\'e}n},
  title		= {Downward Closed Language Generators},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2003},
  number	= {2003-001},
  month		= jan,
  abstract	= {We use downward closed languages for representing sets of
		  states when performing forward reachability analysis on
		  infinite-state systems. Downward closed languages are often
		  more succinct than exact representations of the set of
		  reachable states. We introduce a formalism for representing
		  downward closed languages, called \emph{downward closed
		  language generators (dlgs)}. We show that standard set
		  operations needed for performing symbolic reachability
		  analysis are computable for dlgs. Using a class of
		  hierarchically defined dlgs, we have implemented a
		  prototype for analysing timed Petri nets and used it to
		  analyze a parameterized version of Fischer's protocol. We
		  also show how dlgs can be used for uniform representation
		  of formalisms previously presented for models such as Petri
		  nets and lossy channel systems. }
}