Model Checking for Nonmonotonic Logics: Algorithms and Complexity

1 Introduction

In recent years the problem of model checking has been widely studied in knowledge representation and AI [Levesque, 1986; Halpern and Vardi, 1991]. Informally, model checking for a logical formalism L corresponds to the following problem: given an interpretation structure I and a logical formula I:, does I satisfy I: according to the semantics of L?

Model checking has been convincingly advocated as an alternative to classical reasoning, i.e. logical inference. The main advantage of model checking lies in the fact that in general it is computationally easier than logical inference: For instance, it is well-known that, in first­ order logic, model checking is polynomial in the size of the interpretation structure. Besides "classical" applica­ tion domains (like hardware verification), model check­ ing techniques have been recently employed in the field of planning and cognitive robotics [Cimatti et al., 1997].

Lately, model checking has been studied in some propositional nonmonotonic settings [Cadoli, 1992; Lib­ eratore and Schaer£, 1998]. In particular, [Liberatore and Schaer£, 1998] analyze the problem of checking whether a classical (propositional) interpretation "satisfies" a given default theory, in the sense that such interpretation sat­ isfies at least one extension of the default theory.

The results obtained show that for propositional de­ fault logic this kind of model checking is in general as hard as logical inference, hence the computational ad­ vantages of model checking over theorem proving do not seem to hold in the case of default logic.

The work presented in this paper originates from a different definition of model checking for default logic and several other nonmonotonic logics. Such a notion is an immediate consequence of the fact that many non­ monotonic formalisms make use of interpretation struc­ tures (i.e. default extensions, autoepistemic expansions, universal Kripke models) which are more complex than standard interpretations of classical logic, and which can be represented in a compact way by means of logical for­ mulas. Hence, we argue that model checking in such frameworks corresponds to verify whether a given inter­ pretation structure of this form satisfies a nonmonotonic theory, according to the semantics of the formalism. E.g., according to this notion, a model of a default theory is a default extension, and model checking for proposi­ tional default logic corresponds to verify whether a given propositional formula represents an extension of a given default theory. Hence, the notion of model checking in such nonmonotonic formalisms is peculiar in the sense that the interpretation structure is represented by means of a logical formula.

We thus provide a computational analysis of the above notion of model checking for several propositional non­ monotonic logics. In particular, we characterize the com­ plexity of model checking in Reiter's default logic [Reiter, 1980], disjunctive default logic [Gelfond et al., 1991], and for several syntactic restrictions of such formalisms ; we also study model checking in Moore's autoepistemic logic AEL [Moore, 1985], and in several other nonmonotonic modal logics, including McDermott and Doyle's (MDD) modal logics [Marek and Truszczynski, 1993], the modal logic of minimal knowledge SSe [Halpern and Moses, 1985], and the logic of minimal knowledge and negation as failure MKNF [Lifschitz, 1991].

Our analysis shows that the problem of model check­ ing is easier than logical inference in all the cases ex­ amined: typically, model checking for propositional nonmonotonic formalisms is complete with respect to the class 0~ [Eiter and Gottlob, 1997], while logical infer­ ence is typically II~-complete in such logics. We also provide model checking algorithms for both default logic and several nonmonotonic modal logics.

In the following, we first briefly recall Reiter's default logic and Moore's autoepistemic logic. Then, in Sec­ tion 3 we analyze model checking in default logic, and in Section 4 we study model checking in nonmonotonic modal logics. Finally, in Section 5 we compare our ap­ proach with recent related work, and conclude in Sec­ tion 6.

2 Preliminaries

We start by briefly recalling Reiter's default logic [Reiter, 1980]. Let £ be the usual propositional language. A default rule is a rule of the form

where n 2: 0 and a (called the prerequisite), (31, ... , f3n (called justifications), and 1 (called the conclusion) are all formulas from £. A default theory is a pair (D, W) where W E £ and D is a set of default rules.

Default theories in which each rule is of the form o:;f are called normal (i.e. the justification is equal to the consequence of the default). Moreover, if each default is of the form ~, then the default theory is called super­ normal.

The characterization of default theories is given through the notion of extension, i.e. a deductively closed set of propositional formulas. In the following, given a set of propositional formulas G, we denote with Cn( G) the deductive closure of G, i.e. the set of propositional formulas logically implied by G.

Let E <;;;; £, and let D be a set of default rules. We denote with D(E) (and say that D(E) is the reduct of D with respect to E) the set

We say that a set E <;;;; £ is closed under a set of justification-free default rules D if, for each ~ E D , if a E E then 1 E E.

Definition 1 [Gelfand et a!., 1991, Theorem 2.3} Let (D, W) be a default theory, and let E <;;;; £. E is an extension for (D, W) iff W E E and E is the minimal set closed under deduction and closed under the set D(E).

We recall that each extension is fully characterized by the set of conclusions of the default rules applied during this construction: in fact, it is easy to see that, for each extension of (D, W), there exists a subset G of the set of conclusions {11 , ... , 1d of the default rules in D (which is denoted as Con(D)) such that E = Cn(W A/\,,EG li). Hence, each extension of a given default theory can be represented in terms of a propositional formula f (or any propositional formula equivalent to f). Moreover, the propositional formula f = W 1\ /\,, EG li provides a finite representation of an infinite structure (i.e. the extension).

In [Gelfond et al., 1991] default logic has been ex­ tended to the case of disjunctive conclusions, in the fol­ lowing way. A disjunctive default rule is a rule of the form

where n, m 2: 0 and a,(31, ... ,f3n, 11, ... , lm E £. A dis­ junctive default theory is a pair (D, W) where W E £ and D is a set of disjunctive default rules. The char­ acterization of disjunctive default theories is given by changing (in a conservative way) the above notion of ex­ tension as follows.

The reduct D(E) wrt E <;;;; £ of a set of disjunctive defaults D is the set

We say that a set E <;;;; £ is closed under a set of justification-free disjunctive default rules D if, for each ,, t ' 1 ,m E D, if a E E then li E E for some i such that 1 < i < m. E C £ is an extension for a disjunctive default theory (D~W) iff WEE and Eisa minimal set closed under deduction and under the set D(E).

We finally briefly recall Moore's autoepistemic logic (AEL). We denote with LK the modal extension of£ with the modality K. Moreover, we denote with £J; the set of fiat modal formulas, that is the set of formulas from LK in which each propositional symbol appears in the scope of exactly one modality.

Definition 2 A consistent set of formulas T from LK is a stable expansion for a formula I: ELK ifT satisfies the following equation:

where CnKo45 is the logical consequence operator of modal logic KD45.

Given I:, cp E LK, I: FAEL cp iff cp belongs to all the stable expansions of I:. Notably, each stable expansion T is a stable set, i.e. (i) T is closed under propositional consequence; (ii) if cp E T then K cp E T; (iii) if cp (/_ T then ·K cp E T. We recall that each stable set S corresponds to a maximal universal 55 model Ms such that S is the set of formulas satisfied by Ms (see e.g. [Marek and Truszczynski, 1993]).

With the term AEL model for I: we will refer to an 55 model whose set of theorems corresponds to a stable expansion for I: in AEL: without loss of generality, we will identify such a model with the set of interpretations it contains. Moreover, each 55 model corresponding to a stable expansion S of a formula I: can be characterized by a propositional formula f such that Ms = {I: If= f}; f is called the objective kernel of the stable expansion S. As in the case of default logic, f provides a finite representation of an infinite structure.

Finally, notice that, as in e.g. [Marek and Truszczynski, 1993], we have adopted the notion of con­ sistent autoepistemic logic, i.e. we do not allow the in­ consistent theory consisting of all modal formulas to be a (possible) stable expansion. The results we present can be easily extended to this case (corresponding to Moore's original proposal).

We finally briefly introduce the complexity classes mentioned throughout the paper (we refer to [Johnson, 1990] for further details). All the classes we use reside in the polynomial hierarchy. In particular, the complexity class I:~ is the class of problems that are solved in poly­ nomial time by a nondeterministic Turing machine that uses an NP-oracle (i.e., that solves in constant time any problem in NP), and IT~ is the class of problems that are complement of a problem in I:~. The class 8~ [Eiter and Gottlob, 1997] (also known as ~~[O(log n)]) is the class of problems that are solved in polynomial time by a deterministic Turing machine that makes a number of calls to an NP-oracle which is logarithmic in the size of the input. Hence, the class 8~ is "mildly" harder than the class NP, since a problem in 8~ can be solved by solving "few" (i.e. a logarithmic number of) instances of problems in NP. It is generally assumed that the poly­ nomial hierarchy does not collapse, and that a problem in the class 8~ is computationally easier than a I:~-hard or 1l~-hard problem.

3 Model checking in default logic

In this section we analyze the complexity of model check­ ing for propositional default logic. We start by proving that such a problem belongs to the complexity class 8~. To this aim, we define the algorithm DL-Check (reported in Figure 1) for checking whether a propositional formula f represents an extension of a default theory (D, W). The algorithm first computes D', the reduct of D with respect to f, then computes a formula representing the extension of (D', W), and finally checks whether such a formula is equivalent to f.

In the algorithm, we make use of the well-known fact that a justification-free default theory (D', W) has ex­ actly one extension. We denote as Ext( (D', W)) the propositional formula representing such an extension, which can be naively computed through a quadratic (in the cardinality of D') number of NP-calls, starting from Ext( (D', W)) = W and conjoining to Ext( (D', W)) the conclusions 'Yi of each default rule di = ~ in D' such that O:i is logically implied by Ext((D', W)).

Correctness of the algorithm follows immediately from Definition 1.

Lemma 3 Let (D, W) be a default theory, and let f E £ . Then, Cn(f) is an extension of (D, W) iff DL­ Check((D, W), f) returns true.

The computational analysis of the algorithm DL­ Check provides an upper bound for the model checking problem in default logic.

Algorithm DL-Check((D, W),f) Input: default theory (D, W), formula f E £ ; Output: true if Cn(f) is an extension of (D, W) , false otherwise begin D' =0; for each d = a :{31 , . . ,[3n E D do "' iff ~ ·fJ; for each i = 1, ... , n then add £.=. to D' · "' ' compute Ext((D', W)); if F f = Ext((D', W)) then return true else return false end

Theorem 4 Let (D, W) be a default theory, and let f E £ . Then, the problem of establishing whether Cn(f) is an extension of (D, W) is in 8~.

Proof sketch. First, we prove that it is possible to com­ pute the formula Ext( (D', W)) through a linear number (in the cardinality of D') of calls to an NP-oracle, by using the following procedure:

Then, based on the use of the above procedure for computing Ext( (D', W) ), we show that the algorithm DL-Check can be reduced to an NP-tree [Eiter and Got­ tlob, 1997], which immediately implies an upper bound of 8~ for the problem of model checking in propositional default logic. D

We now turn our attention to establishing lower bounds for model checking in default logic. We first prove that such a problem is 8~-hard even if default rules are normal.

Theorem 5 Let (D, W) be a normal default theory, and let f E £ . Then, the problem of establishing whether Cn(f) is an extension of (D, W) is 8~ -hard.

Proof sketch. We reduce the 8~-complete problem PAR­ ITY(SAT) [Eiter and Gottlob, 1997] to model check­ ing for a normal default theory. Informally, an in­ stance of PARITY(SAT) is a set of propositional for­ mulas cp1, ... , 'Pn, such that if 'Pi is not satisfiable then, for each j 2: i, 'Pi is not satisfiable. The problem is to establish if the number of satisfiable formulas is odd.

Given an instance of such a problem, in which we as­ sume n odd without loss of generality, we construct the normal default theory (D, W), in which W = true and

where p' is a propositional symbol not appearing in 'PI, · · · , 'Pn·

We prove that there is an odd number of satisfiable formulas in 'PI, ... , 'Pn iff true is an extension of (D, W). Informally, this is due to the fact that the number of satisfiable formulas is even if and only if either all for­ mulas are not satisfiable (i.e. 'PI is not satsfiable) or, for some even i, it holds that 'Pi is satisfiable and 'PHI is not satisfiable. Now, the rules in D are built in such a way that, if this situation occurs, then there is a default rule which is applied, thus forcing knowledge of p' in the ex­ tension. Therefore, in this case true is not an extension for (D, W) . 0

The above property, together with Theorem 4, imme­ diately implies that model checking is 0~-complete both for general propositional default theories and for normal default theories.

Then, with a proof similar to the previous one, it is possible to show that model checking is 8~-hard also in the case of prerequisite-free default theories.

Theorem 6 Let (D, W) be a prerequisite-free default theory, and let f E £.· Then, the problem of establishing whether Cn(f) is an extension of (D, W) is 0~ -hard.

Again, the above theorem and Theorem 4 prove that model checking is 0~-complete for prerequisite-free de­ fault theories.

We now turn our attention to supernormal (i.e. both normal and prerequisite-free) default theories, and prove that in this case model checking is computationally easier than for unrestricted default theories.

Theorem 7 Let (D, W) be a supernormal default the­ ory, and let f E £. The problem of establishing whether Cn(f) is an extension of (D, W) is coNP-complete.

Proof sketch. As for membership in coNP, we reduce the problem to a propositional validity problem. The key property is the fact that, given

Cn(f) is an extension of (D, W) iff the following two conditions hold:

1. for each i, either f f= (3; or f f= ·(3;;
2. W 1\ l\n=f3· (3; is equivalent to f.

We prove that it is possible to encode each of the two above conditions in terms of a propositional valid­ ity problem, through two polynomial transformation of the input. We thus obtain two propositional formulas ri( (D, W), f) and r2 ( (D, W), f) such that condition 1. holds iff ri( (D, W), f) is valid and condition 2. holds iff ri( (D, W), f) is valid. Then, by simply using two dis­ tinct alphabets for the two formulas, it is possible to reduce the two problems to a single validity problem.

Hardness with respect to coNP follows from the fact that propositional validity of a formula f can be reduced to the problem of establishing whether f is an extension of (0, true) . 0

Algorithm AEL-Check(I:, f) Input: formula I: E LK, formula f E £; Output: true if M = {I : I f= !} is AEL model for I:, false otherwise begin while I: f/. £ do begin choose a subformula K<p from I: such that <p E £; if t F= 1P then I: := I:(K <p -+ true) else I: := I:(K <p -+ false) end; if F= t =I: then return true else return false end

As for disjunctive default logic, the easiest way to characterize model checking is to exploit known corre­ spondences between such a formalism and nonmonotonic modal logic MKNF [Lifschitz, 1991]. In particular, the existence of a polynomial embedding of disjunctive de­ fault theories in the fiat fragment of the logic MKNF makes it possible to show that model checking is in 0~. Moreover, 0~-hardness follows from Theorem 5 and from the fact that disjunctive default logic is a conserva­ tive generalization of default logic. Hence, the following property holds.

Theorem 8 Let (D, W) be a disjunctive default theory, and let f E £. Then, the problem of establishing whether Cn(f) is an extension of (D, W) is 8~-complete.

The above property and Theorem 6 also imply 0~­ completeness of model checking for prerequisite-free dis­ junctive default theories.

In Table 1 we summarize the complexity results de­ scribed in this section. Each column of the table corre­ sponds to a different condition on the conclusion part of default rules.

The results reported in the table, together with known complexity characterizations of the inference problem in default logic (for a survey see [Cadoli and Schaerf, 1993]), show that model checking is easier than logical inference in all the cases considered. In fact, logical inference is already I1~-hard (skeptical reasoning) or ~~-hard ( cred­ ulous reasoning) for supernormal default theories, while model checking is always in 0~.

4 Model checking in nonmonotonic modal logics

In this section we analyze model checking for non­ monotonic modal logics. Due to lack of space, in the followin& we only sketch our complexity analysis, and refer to lMarek and Truszczynski, 1993; Lifschitz, 1991] for a formal definition of MDD logics and MKNF: all the results obtained are summarized in Table 2.

We start by examining the case of autoepistemic logic. In Figure 2 we report the algorithm AEL-Check for checking whether a propositional formula represents an autoepistemic model of a modal formula. In the algo­ rithm, I:(K <p -+ true) represents the formula obtained from I; by replacing each occurrence of the subformula Kc.p with true, while I:(Kc.p-+ false) represents the for­ mula obtained from I: by replacing each occurrence of the subformula K <p with false.

Informally, the algorithm iteratively computes the value of all modal subformulas (without nested occur­ rences of the modality) in I: according to f , until all modal subformulas have been replaced by a truth value. The resulting propositional formula is compared with f, and the algorithm returns true if and only if the two formulas are equivalent.

Correctness of the algorithm can be established by means of previous results on reasoning in autoepistemic logic [Marek and Truszczynski, 1993].

Lemma 9 Let I: E £ K, f E £ . Then, M = {I : I F !} is an AEL model of I: iff AEL-Check{I;, f) returns true .

The above property allows us to prove 0~­ completeness of model checking in AEL.

Theorem 10 Let I: E LK , f E £ . Then, the problem of establishing whether M = {I : I F !} is an AEL model of I; is 0~ -complete.

Proof sketch. Membership in 0~ follows from Lemma 9 and from the fact that the algorithm AEL-Check can be polynomially reduced to an NP-tree. Hardness follows from the fact that it is possible to reduce an instance of the problem of model checking for prerequisite-free default theories to model checking in AEL: the reduction is based on the correspondence between the prerequisitefree default * and the modal formula ·K ·fJ :) 1 in autoepistemic logic. D

It can actually be shown that model checking for AEL is 8~-hard (and thus, from the above theorem, 0~­ complete) even under the restriction that the formula I: is fiat, i.e. each propositional symbol in I: lies within the scope of exactly one modality. The proof of this property can be obtained through a reduction from PAR­ ITY(SAT).

A similar analysis allows for establishing . the same complexity characterization for the problem of model checking in two well-known nonmonotonic modal for­ malisms of the McDermott and Doyle's (MDD) family, i.e. the nonmonotonic logics based on the modal systems SW5 and S4F [Marek and Truszczynski, 1993].

Theorem 11 Let I: E LK, f E £ . Then, the problem of establishing whether M = {I : I F !} is an S4FMDD model (or an SW5MDD model) of I: is 8~-complete.

As in the case of autoepis~emic logic, the above prop­ erty also holds if we restrict to flat formulas.

For modal logics based on the minimal knowledge par­ adigm, we prove that model checking is harder than for the above presented nonmonotonic logics. In particular, it is a I:~-complete problem. However, logical inference in such logics of minimal knowledge is harder than in default logic and autoepistemic logic, since it is a II~­ complete problem both in MKNF and in S5c [Donini et al., 1997; Rosati, 1997]. Hence, also in such formalisms model checking is easier than logical inference. We first analyze modal logic S5c, i.e. the logic of minimal knowl­ edge introduced in [Halpern and Moses, 1985].

Theorem 12 Let I: E LK, f E £. Then, the problem of establishing whether M = {I : I F !} is an S5c model of I: is I:~ -complete.

Interestingly, if we impose that the modal formula I: is flat, then model checking in S5c becomes easier.

Theorem 13 Let I: ELk, f E £. Then, the problem of establishing whether M = {I : I F !} is an S5c model of I; is 0~ -complete.

The same computational characterization of model checking can be shown for the logic MKNF, i.e. the logic of minimal knowledge and negation as failure introduced in [Lifschitz, 1991], which extends S5c with a second modal operator interpreted in terms of negation as fail­ ure.

Comparing the above results with known computa­ tional characterizations of the inference problem in non­ monotonic modal logics, it turns out that model checking is easier than logical inference in all the cases consid­ ered. Moreover, we remark that logical inference in the flat fragment of S5c and MKNF is II~-complete. This implies that , for each of the cases reported in the table, if logical inference is II~-complete, then model checking is 0~-complete, and if logical inference is II~-complete, then model checking is I:~-complete.

5 Related work

Model checking has been recently studied in some non­ monotonic settings (see e.g. [ Cadoli, 1992; Liberatore and Schaerf, 1998]). In particular, the work reported in [Liberatore and Schaerf, 1998] is the closest to the approach presented in this paper, since it deals with the model checking problem for propositional default logic.

The notion of model checking introduced in [Liber­ atore and Schaerf, 1998] for default logic corresponds to check whether a propositional interpretation I "sat­ isfies" a given default theory (D, W), in the sense that I satisfies at least one extension of (D, W). Such a no­ tion of model checking relies on the usage of standard propositional interpretations, thus avoiding the need to resort to the representation of an interpretation struc­ ture in terms of a logical formula. On the other hand, a propositional interpretation cannot be considered as a "model" of a default theory: in fact, model-theoretic characterizations of default logic are based on possible­ world structures analogous to universal 55 models intro­ duced for autoepistemic logic. Hence, a propositional interpretation is a component of an interpretation struc­ ture of a default theory. Instead, our formulation of the model checking problem is based on the idea of checking a whole interpretation structure of this form against a nonmonotonic theory: in this sense, our notion is a more natural extension to nonmonotonic logics of the "classi­ cal" notion of model checking.

From the computational viewpoint, it turns out that Liberatore and Schaerf's notion of model checking is harder than the one presented in this paper. In fact, comparing Table 1 with the results reported in [Liber­ atore and Schaerf, 1998], it can be seen that our for­ mulation of model checking is computationally easier in almost all the cases examined, with the exception of nor­ mal and supernormal default theories, for which the com­ plexity of the two versions of model checking is the same.

6 Conclusions

In this paper we have studied the complexity of model checking in several nonmonotonic logics. Our results show that , as in classical logic, model checking is com­ putationally easier than logical inference in many non­ monotonic formalisms. We have also provided algo­ rithms for model checking in default logic and nonmo­ tonic modal logics.

Our results provide a positive answer to the question whether it is convenient to use "model-based" represen­ tations of knowledge in the case of nonmonotonic log­ ics. It therefore appears possible to use the analysis pre­ sented in this paper as the basis for the development of model checking techniques in knowledge representation systems with nonmonotonic abilities.

Acknowledgments

The author wishes to thank Paolo Liberatore for useful discussions about the subject of this paper.