Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP

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 $\mu$-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