Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

This paper introduces a new methodology for epistemic logic, to analyze communication protocols that uses knowledge structures, a specific form of Kripke semantics over hostile networks. The paper particularly focuses on automatic verification of authentication protocols. Our approach is based on the actual definitions of a protocol, not on some difficultto-establish justifications. The proposed methodology is different from many previous approaches to automatic verification of security protocols in that it is justification-oriented instead of falsification-oriented, i.e., finding bugs in a protocol. The main idea is based on observations： separating a principal executing a run of protocol from the role in the protocol, and inferring a principal＇s knowledge from the local observations of the principal. And we show analytically and empirically that this model can be easily reduced to Satisfiability （SAT） problem and efficiently implemented by a modern SAT solver.     

Framework of knowledge management in education based on knowledge grid

Knowledge grid is a kind of knowledge sharing environment based on the World Wide Web, and its essence is the synergy and sharing of internet knowledge resource and knowledge service. KM （knowledge management） in education based on KG （knowledge grid） makes use of the grid technology and integrates the methods and tools of KM in Education to support the whole cycle of knowledge application. Based on the advantages of KM in Education, in this paper, we construct a service-oriented model of KM in Education in order to achieve more effective knowledge sharing and knowledge service in education.     

Modular approach to the design and analysis of password-based security protocols

In this paper, a general framework for designing and analyzing password-based security protocols is presented. First we introduce the concept of "weak computational indistinguishability" based on current progress of password-based security protocols. Then, we focus on cryptographic foundations for password-based security protocols, i.e., the theory of "weak pseudorandomness". Furthermore, based on the theory of weak pseudorandomness, we present a modular approach to design and analysis of password-based security protocols. Finally, applying the modular approach, we design two kinds of password-based security protocols, i.e., password-based session key distribution (PSKD) protocol and protected password change (PPC) protocol. In addition to having forward secrecy and improved efficiency, new protocols are proved secure.     

Observer and observer-based H_∞control of generalized Hamiltonian systems

~~Observer and observer-based H_∞control of generalized Hamiltonian systems1. Luenberger, D. G., Observers for multivariable systems, IEEE Trans, on Autom. Contr., 1966, 11: 190-197. 2. O'Reilly, J., Observer for linear systems, New York: Academic Press, 1983. 3. Slotine, J. J. E., Hedrick, J. K., Misawa, E.A., On sliding observers for nonlinear systems, Journal of Dynamic Systems, Measurement and Control, 1987, 109: 245-252. 4. Hunt, L. R., Verma, M. S., Obse…     

基于本体的医学知识获取

In this paper, we introduce an ontology-mediated method for medical knowledge acquisition and analysis.Using the method we establish an ontological structure and ontologies for the Medical Knowledge Base (or NKIMed ). To check the consistency of the acquired knowledge, we use a set of medicine-specific axioms. These axioms are also used in knowledge inference, and interconnection between diiferent medical concepts. Finally, two applications of NKIMed, i.e. intelligent teachinu systems and speech diagnosis are illustrated.     

A programmable approach to revising knowledge bases

Knowledge base revision,which is also called belief revision,is an important topic in artificial intelligence and philosophy,and many approaches have been introduced in re-cent years[1―26].An important topic for knowledge base revision is to introduce a pro-grammable approach[9].This paper focuses on showing a programmable approach to revise a knowledge base consisting of clauses.Knowledge base revision is important from both the theoretical and applied point of view[27].Doyle’s truth mainte…     

Designing a Top-Level Ontology of Human Beings: A Multi-Perspective Approach

Knowledge about human beings is an integral part of any intelligent agent of considerable significance. Delimiting, modeling and acquiring such knowledge are the central topics of this paper. Because of the tremendous complexity in knowledge of human beings, we introduce a top-level ontology of human beings from the perspectives of psychology, sociology, physiology and pathology. This ontology is not only an explicit conceptualization of human beings, but also an efficient way of acquiring and organizing relevant knowledge.     

Knowledge base grid: A generic grid architecture for semantic web

The emergence of semantic web will result in an enormous amount of knowledge base resources on the web. In this paper, a generic Knowledge Base Grid Architecture (KB-Grid) for building large-scale knowledge systems on the semantic web is presented. KB-Grid suggests a paradigm that emphasizes how to organize, discover, utilize, and manage web knowledge base resources. Four principal components are under development: a semantic browser for retrieving and browsing semantically enriched information, a knowledge server acting as the web container for knowledge, an ontology server for managing web ontologies, and a knowledge base directory server acting as the registry and catalog of KBs. Also a referential model of knowledge service and the mechanisms required for semantic communication within KB-Grid are defined. To verify the design rationale underlying the KB-Grid, an implementation of Traditional Chinese Medicine (TCM) is described.     

Call for Papers The First International Conference on Rough Sets and Knowledge Technology (RSKT2006)

Overview Since the introduction of rough sets in 1982 by Professor Zdzistaw Pawlak. we have witnessed great advances in both theory and appications. There has been a rapid growth inresearch and applications of rough sets in Asia, particulary in China. Rough set theory is closely related to knowledge technology ina variety of forms such as knowledge discovery, approximate reasoning, intelligent and multiagent systems design, knowledgeintensive computations that signal the emergence of a knowledge technology age. The essence of growth in cutting-edge, state-of-the-art and promising knowledge technologies is closely related to learning, pattern recognition, machine intelligence and automation ofacquisition, transformation, communication, exploration and exploitation of knowledge. A principal thrust of such technologies is theutilization of methodologies that facilitate knowledge processing. To present state-of-the-art scientific results, encourage academicand industrial interaction, and promote collaborative reserch and developmental activities, in rough sets and knowledge technologyworldwide, a new intemational confrence named Rough Sets and Knowledge Technology (RSKT) is proposed. It will provide a newforum for researchers in rough sets and knowledge technology.     

文本知识发现:基于信息抽取的文本挖掘蝌

In the general context of Knowledge Discovery, Knowledge Discovery in Text (KDT), which uses TextMining techniques to extract and induce hidden knowledge from unstructured text data, surges in the data and naturallanguage processing research. KDT is a multi-discipline of Artificial Intelligence, Machine learning, Natural Lan-ing with a stressing on its IE (Information Extraction)-based induction and specific sublanguage fields oriented prac-tices.     

An investigation of modal structures as an alternative semantic basis for epistemic logics

In the past, Kripke structures have been used to specify the semantic theory of various modal logics. More recently, modal structures have been developed as an alternative to Kripke structures for providing the semantics of such logics. While these approaches are equivalent in a certain sense, it has been argued that modal structures provide a more appropriate basis for representing the modal notions of knowledge and belief. Since these notions, rather than the traditional notions of necessity and possibility, are of particular interest to artificial intelligence, it is of interest to examine the applicability and versatility of these structures. This paper presents an investigation of modal structures by examining how they may be extended to account for generalizations of Kripke structures. To begin with, we present an alternative formulation of modal structures in terms of trees; this formulation emphasizes the relation between Kripke structures and modal structures, by showing how the latter may be obtained from the former by means of a three-step transformation. Following this, we show how modal structures may be extended to represent generalizations of possible worlds, and to represent generalizations of accessibility between possible worlds. Lastly, we show how modal structures may be used in the case of a full first-order system. In all cases, the extensions are shown to be equivalent to the corresponding extension of Kripke structures.     

Kripke Semantics for Modal Substructural Logics

We introduce Kripke semantics for modal substructural logics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructural logics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, Méndez's logics and relevant logics.     

Reference and perspective in intuitionistic logics

What an intuitionist may refer to with respect to a given epistemic state depends not only on that epistemic state itself but on whether it is viewed concurrently from within, in the hindsight of some later state, or ideally from a standpoint “beyond” all epistemic states (though the latter perspective is no longer strictly intuitionistic). Each of these three perspectives has a different—and, in the last two cases, a novel—logic and semantics. This paper explains these logics and their semantics and provides soundness and completeness proofs. It provides, moreover, a critique of some common versions of Kripke semantics for intuitionistic logic and suggests ways of modifying them to take account of the perspective-relativity of reference.     

Topological Perspective on the Hybrid Proof Rules

We consider the non-orthodox proof rules of hybrid logic from the viewpoint of topological semantics. Topological semantics is more general than Kripke semantics. We show that the hybrid proof rule BG is topologically not sound. Indeed, among all topological spaces the BG rule characterizes those that can be represented as a Kripke frame (i.e., the Alexandroff spaces). We also demonstrate that, when the BG rule is dropped and only the Name rule is kept, one can prove a general topological completeness result for hybrid logics axiomatized by pure formulas. Finally, we indicate some limitations of the topological expressive power of pure formulas. All results generalize to neighborhood frames.     

Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation

Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist calculus, is presented, (4) a strongly normalizable typed λ-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory.     

一种新的类BAN逻辑模态语义模型——兼论类BAN逻辑的语法缺陷

由于类BAN逻辑缺乏明确而清晰的语义，其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型，在此基础上定义了符合模态逻辑的类BAN逻辑“可能世界”语义模型，并从语义的角度证明了在该模型下的类BAN逻辑语法存在的缺陷，同时，指出了建立或改进类BAN逻辑的方向。     

Coalgebraic semantics of modal logics: An overview

Coalgebras can be seen as a natural abstraction of Kripke frames. In the same sense, coalgebraic logics are generalised modal logics. In this paper, we give an overview of the basic tools, techniques and results that connect coalgebras and modal logic. We argue that coalgebras unify the semantics of a large range of different modal logics (such as probabilistic, graded, relational, conditional) and discuss unifying approaches to reasoning at this level of generality. We review languages defined in terms of the so-called cover modality, languages induced by predicate liftings as well as their common categorical abstraction, and present (abstract) results on completeness, expressiveness and complexity in these settings, both for basic languages as well as a number of extensions, such as hybrid languages and fixpoints.     

Exogenous Probabilistic Computation Tree Logic

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non–deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so–called quantum one–time pad.     

On Non-axiomatizability of Superintuitionistic Predicate Logics of Some Classes of Well-founded and Dually Well-founded Kripke Frames

The article presents general results on non-axiomatizabilityfor superintuitionistic predicate logics. In particular, thelogics of all well-ordered, all dually well-ordered, and alldually well-founded Kripke frames (in the semantics with nestedand with constant domains) are -hard, and the logic of all Kripke frames of finite heightis not recursively axiomatizable (although it is known to be -arithmetical). A resulton Kripke-incompleteness is stated as well.