Forward analysis procedures for infinite-state systems such as timed systems were limited to safety properties. We give the
first constraint-based forward analysis for infinite-state systems that goes beyond safety properties. Namely, we take the
restriction of the μ-calculus to least-fixpoint formulas where negation is applied to closed subformulas only. We characterize these properties
as perfect models of constraint logic programs, and we present a tabulation procedure for the top-down evaluation of stratified
constraint logic programs.
Support from the grants NSF award CCR99-70925, SRC award 99-TJ-688, and DARPA ITO Mobies award F33615-00-C-1707 is gratefully
acknowledged.