Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Static Analysis of Logic Programs via Boolean Networks

Van-Giang Trinh, Belaid Benhamou

TL;DR

This work addresses static analysis in ASP by establishing a principled link to Boolean Networks. By encoding a logic program $P$ as a BN $f$ with $var_f = \text{atom}(P)$ and $f_v = \bigvee_{r:\, h(r)=v} bf(r)$, it is shown that $\text{supp}(P)=\text{fix}(f)$ and $\text{ig}(f) \subseteq \text{dg}(P)$, enabling BN fixed-point theory to inform ASP. The authors derive new results on how positive and negative cycles in the Dependence Graph influence the number and existence of stable models, including a PFVS-based upper bound $| ext{sm}(P)| \leq 2^{|U^{+}|}$ and conditions for one or two stable models. They discuss computation via BN fixed points, possible program-correction applications, and the potential to extend these insights to broader logic-programming frameworks. Overall, the work provides a unified, theory-driven approach to analyzing and potentially repairing ASP programs by importing BN methods and cycle-based reasoning.

Abstract

Answer Set Programming (ASP) is a declarative problem solving paradigm that can be used to encode a combinatorial problem as a logic program whose stable models correspond to the solutions of the considered problem. ASP has been widely applied to various domains in AI and beyond. The question "What can be said about stable models of a logic program from its static information?" has been investigated and proved useful in many circumstances. In this work, we dive into this direction more deeply by making the connection between a logic program and a Boolean network, which is a prominent modeling framework with applications to various areas. The proposed connection can bring the existing results in the rich history on static analysis of Boolean networks to explore and prove more theoretical results on ASP, making it become a unified and powerful tool to further study the static analysis of ASP. In particular, the newly obtained insights have the potential to benefit many problems in the field of ASP.

Static Analysis of Logic Programs via Boolean Networks

TL;DR

This work addresses static analysis in ASP by establishing a principled link to Boolean Networks. By encoding a logic program as a BN with and , it is shown that and , enabling BN fixed-point theory to inform ASP. The authors derive new results on how positive and negative cycles in the Dependence Graph influence the number and existence of stable models, including a PFVS-based upper bound and conditions for one or two stable models. They discuss computation via BN fixed points, possible program-correction applications, and the potential to extend these insights to broader logic-programming frameworks. Overall, the work provides a unified, theory-driven approach to analyzing and potentially repairing ASP programs by importing BN methods and cycle-based reasoning.

Abstract

Answer Set Programming (ASP) is a declarative problem solving paradigm that can be used to encode a combinatorial problem as a logic program whose stable models correspond to the solutions of the considered problem. ASP has been widely applied to various domains in AI and beyond. The question "What can be said about stable models of a logic program from its static information?" has been investigated and proved useful in many circumstances. In this work, we dive into this direction more deeply by making the connection between a logic program and a Boolean network, which is a prominent modeling framework with applications to various areas. The proposed connection can bring the existing results in the rich history on static analysis of Boolean networks to explore and prove more theoretical results on ASP, making it become a unified and powerful tool to further study the static analysis of ASP. In particular, the newly obtained insights have the potential to benefit many problems in the field of ASP.
Paper Structure (10 sections, 14 theorems, 2 figures)

This paper contains 10 sections, 14 theorems, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Main Results
  4. Logic Programs and Boolean Networks
  5. Cycles and Stable Models
  6. Discussion
  7. Computation of stable models
  8. Program correction
  9. Interplay between positive and negative cycles
  10. Conclusion and Future Work

Key Result

Theorem 1

Let $P$ be an LP. If $\text{dg}^+({P})$ has no cycle, then the set of stable models of $P$ coincides with the set of supported models of $P$.

Figures (2)

  • Figure 1: (a) $\text{dg}({P})$. (b) $\text{ig}({f})$.
  • Figure 2: (a) $\text{dg}({P_1})$. (b) $\text{dg}({P_2})$.

Theorems & Definitions (31)

  • Theorem 1: cois1994consistency
  • Definition 1
  • Theorem 2
  • proof
  • Theorem 3
  • proof
  • Example 1
  • Proposition 4
  • proof
  • Proposition 5
  • ...and 21 more