The-decidability-of-guarded-fixed-point-logic.pdf
《The-decidability-of-guarded-fixed-point-logic.pdf》由会员分享,可在线阅读,更多相关《The-decidability-of-guarded-fixed-point-logic.pdf(14页珍藏版)》请在三一文库上搜索。
1、The decidability of guarded fi xed point logic Erich Gr adel Abstract Guarded fi xed point logics are obtained by adding least and greatest fi xed points to the guarded fragments of fi rst-order logic that were recently introduced by Andr eka, van Benthem and N emeti. Guarded fi xed point logics can
2、 also be viewed as the nat- ural common extensions of the modal -calculus and the guarded fragments.In a joint paper with Igor Walukiewicz, we proved recently that the satisfi ability problems for guarded fi xed point logics are decidable and complete for deterministic double ex- ponential time. Tha
3、t proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. We present here an elementary proof for the decidability of guarded fi xed point logics which is based on guarded bisimulations, a tree model property for guarded logi
4、cs and an interpretation into the monadic second-order theory of countable trees. Contents 1Introduction2 2 Guarded fi xed point logics4 3The tree model property7 4Reduction to the monadic theory of trees10 5Variations13 1 1Introduction Modal logics are widely used in a number of areas in computer s
5、cience, in par- ticular for the specifi cation and verifi cation of hardware and software systems, for knowledge representation, in databases, and in artifi cial intelligence. The most important reason for the successful applications of these logics is that they provide a good balance between expres
6、sive power and computational complex- ity. A great number of logical formalisms have been successfully tailored in such a way that they are powerful enough to express interesting properties for a spe- cifi c application but still admit reasonably effi cient algorithms for their central computational
7、 problems, in particular for model checking and for satisfi ability or validity tests. Many of these formalisms are essentially modal logics although this is not always apparent from their offi cial defi nitions (as for instance in the case of description logics). The basic propositional (poly)modal
8、 logic ML (for a given set A of actions or modalities) extends propositional logic by the possibility to construct for- mulae hai and a (where a A) with the meaning that holds at some, respectively each, a-successor of the current state. Although ML is too weak for most of the really interesting app
9、lications, it can be extended by features like path quantifi cation, transitive closure operators, counting quantifi ers, least and greatest fi xed points, and it has turned out that most of these extensions are still decidable and indeed of considerable practical importance. Up to now, the reasons
10、for these good algorithmic properties of modal log- ics have not been suffi ciently understood. In 15 Vardi explicitly asked the question: “Why is modal logic so robustly decidable?”. To discuss this question, it is useful to consider propositional modal logic as a fragment of fi rst-order logic. Kr
11、ipke structures which provide the semantics for modal logics, are relational structures with only unary and binary relations. Every formula ML can be translated into a fi rst-order formula (x) with one free variable, which is equivalent in the sense that for every Kripke structure K with a distingui
12、shed node w we have that K,w |= if and only if K |= (w).This translation takes an atomic proposition P to the atom Px, it commutes with the Boolean connectives, and it translates the modal operators by quantifi ers as follows: hai ; (hai)(x) := y(Eaxy (y) a ; (a)(x) := y(Eaxy (y), where (y) is obtai
13、ned from (x) by replacing all occurrences of x by y and vice versa and where Eais the transition relation associated with the modality a. The modal fragment of fi rst-order logic is the image of propositional modal logic under this translation. It is properly contained in FO2 , relational fi rst- or
14、der logic with only two variables. But although FO2is decidable and has the fi nite model property (see 12, 6), it lacks the nice model-theoretic properties 1, 9 and, in particular, the robust decidability properties of modal logics. Indeed while the extensions of modal logic by path quantifi cation
15、, transitive closure 2 operators, least fi xed points etc. are still decidable, most of the corresponding extensions of FO2are highly undecidable (see 7, 8).In particular this is the case for fi xed-point logic with two variables, which is the natural common extension of FO2and the -calculus. The em
16、bedding of ML in FO2therefore does not give a satisfactory answer to Vardis question. An important property that is shared by modal logic and its extensions, but not by FO2, and whose importance for the decidability of modal logics has been pointed out by Vardi 15 is the tree model property: Every s
17、atisfi able sentence has a model that is a tree of bounded branching. The tree model property is the basis for the use of automata theoretic techniques to decide the satisfi ability problems for modal logics. An alternative explanation for the good properties of modal logics has been proposed by And
18、r eka, van Benthem and N emeti 1. Starting from the obser- vation that in the translation of modal formulae into fi rst-order formulae, the quantifi ers are used only in a very restricted way, they defi ned the guarded frag- ment of fi rst-order logic. They dropped the restriction to use only two va
19、riables and only monadic and binary predicates, but imposed that all quantifi ers must be relativized by atomic formulae. This means that quantifi ers appear only in the form y(x,y) (x,y)ory(x,y) (x,y). Thus quantifi ers may range over a tuple y of variables, but are guarded by an atom that contains
20、 all the free variables of . The guarded fragment GF extends the modal fragment and turns out to have interesting properties 1, 5: (1) The satisfi ability problem for GF is de- cidable; (2) GF has the fi nite model property, i.e., every satisfi able formula in the guarded fragment has a fi nite mode
21、l; (3) GF has (a generalized variant of) the tree model property; (4) Many important model theoretic properties which hold for fi rst-order logic and modal logic, but not, say, for the bounded- variable fragments FOk, do hold also for the guarded fragment; (5) The notion of equivalence under guarded
22、 formulae can be characterized by a straightfor- ward generalization of bisimulation. In a further paper, van Benthem 2 generalized the guarded fragment to the loosely guarded fragment (LGF) where quantifi ers are guarded by conjunctions of atomic formulae of certain forms (details will be given in
23、the next section.) Most of the properties of GF generalize to LGF. In 5 it is shown that the the satisfi ability problems for GF and LGF are complete for 2Exptime, the class of problems solvable by a deterministic algorithm in time 22 p(n), for some polynomial p(n). Probably the most important exten
24、sion of ML is the -calculus, introduced in 11, which extends propositional modal logic by least and greatest fi xed points and subsumes most of the other program logics such as PDL, CTL and CTLand also many description logics. It is known that the satisfi ability problem for the -calculus is decidab
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- The decidability of guarded fixed point logic
链接地址:https://www.31doc.com/p-3800735.html