Symbolic Model Checking of Non-regular Properties

This paper presents a symbolic model checking algorithm for Fixpoint Logic with Chop, an extension of the modal µ-calculus capable of defining non-regular properties. Some empirical data about running times of a naive implementation of this algorithm are given as well.

• Type: Conference
• Year: 2004
• Where: CAV
• Authors: Martin Lange
• Keywords: CAV 2004, Formal Methods, Model Checking Algorithm, Naive Implementation, Non-regular Properties