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 subformu-las 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.
展开▼
