Solving Alternating Boolean Equation Systems in Answer Set Programming

Abstract. In this paper we apply answer set programming to solve alternating Boolean equation systems. We develop a novel characterization of solutions for variables in disjunctive and conjunctive Boolean equation systems. Based on this we devise a mapping from Boolean equation systems with alternating fixed points to normal logic programs such that the solution of a given variable of an equation system can be determined by the existence of a stable model of the corresponding logic program. The technique can be used to model check alternating formulas of modal µ-calculus.

• Type: Conference
• Year: 2004
• Where: WLP
• Authors: Misa Keinänen, Ilkka Niemelä
• Keywords: Boolean Equation Systems, Check Alternating Formulas, Conjunctive Boolean Equation, WLP 2004