Baoyuan Qi

Gang Ma

Zhongzhi Shi
email: shizz@ics.ict.ac.cn

Wei Wang
email: waywang@hotmail.com

Collecting Valuable Information from Fast Text Streams

Keywords: Fast Text Stream, Information Collection, Trie, N-Gram

It has become a challenging work to collect valuable information from fast text streams. In this work, we propose a method which gains useful information effectively and efficiently. Firstly, we maintain an analyzer based on the Trie structure and the dynamic N-Gram tokenizer; secondly, unlike the traditional search engine principle, we consider the documents as a query by building the indexes for the whole query base. The experimental results show that it has the strong adaption ability, low latency and high quality support for the complex query combination compared with the conventional methods.

Introduction

Text streams is a kind of data stream, which is composed of texts, such as news feed, blog, weibo, etc.. Knowledge discovery from data stream has attracted more research recent years [START_REF] Gama | Knowledge discovery from data streams[END_REF][START_REF] Aggarwal | Data streams: models and algorithms[END_REF][START_REF] Graham | Synopses for Massive Data: Samples, Histograms, Wavelets[END_REF][START_REF] Muthukrishnan | Data streams: Algorithms and applications[END_REF]. Data stream mining in the time and space constraints challenges traditional methods and algorithms [START_REF] Li | Time and space efficient spectral clustering via column sampling[END_REF][START_REF] Zhang | Space-efficient relative error order sketch over data streams[END_REF]. There is always concept drift in the data streams, which make the prediction accuracy decrease along with the time [START_REF] Xioufis | Dealing with concept drift and class imbalance in multilabel stream classification[END_REF][START_REF] Gama | Learning with Drift Detection[END_REF].

It is always easy for a user to retrieve relative records from a static document set. The inverted document index methods are always fast for querying. However, under the streaming, many problems always arise in the evolving environments. The first one comes from the analyzer that has to be used during indexing and search process. There are always new words emerging and combining in the coming documents and querying, the system has to reindex all the documents periodically to help improve search accuracy. Another problem among the conventional practice is the response time for the query with the increasing size of documents. The time for a query will expand excessively when the index base receives endless incoming documents.

User may change his query at any time and he only concerns the results since the newly query is settled. The case always holds in the monitor systems like network traffic and public safety. Under these systems, the speed of incoming data is very fast and the queries waiting for processed are plenty. To tackle this problem, we propose a method to effectively collect valuable information from text streams which cost less time and space and dynamically update the query base in time. In this paper we make contributions on various aspects:

 We design a new flexible analyzer to automatically expand and quickly adapted to user defined dictionary. We use Trie tree data structure to insert new items and at the same time the max length are recorded for further N-Gram tokenizer. The dynamically maintained length is used to implement a maximum segmentation analyzer and the tree is used as a fast dictionary lookup table. The advantage is new entry can be handled as soon as new data arrives, so no data will be lost. Still this can reduce the index size as we only use the user defined term to index the incoming documents.  A new angle to collect valuable information from the endless text streams.

Since there is always the time consuming and space demanding to index all the documents when user indexes the query base set. While constructing the query index, the analyzer changes its parameters accordingly. Newly coming document are tokenized by the analyzer and then searched in the index repository. The advantage is that each query is often short and simple; it is often easy to rebuild query index.

Related Work

Information retrieval (IR) obtains information relevant to a need from many documents. Many models have been proposed like Vector Space Model(VSM) [START_REF] Salton | A vector space model for automatic indexing[END_REF], Okapi BM2.5, etc.. The web search engines like Google, Baidu are the most significant applications. The indexed documents are always static and need to be reindexed once new terms are used for indexing. To return the result in time, there is always query length limit in the input box as long as the operation between the query terms, like OR, AND, etc.. Batch-incremental index mechanism like Zoie1 is always used in dynamic environment. The newly coming documents come first into the small index, it will merge when the small index becomes big enough. This strategy is helpful when the process time of the merge operation doesn't take too much time and it will hang the system when the index size goes larger. The terminology prospective search [START_REF] Irmak | Efficient query subscription processing for prospective search engines[END_REF] is widely used in text stream. There are a lot of applications based on this method, like Google News Alerts, Google Search. Rather than targeting full text search of infrequent queries over huge persistent data archives (historic search), this class targets full text search of huge numbers of querying over comparatively small transient real-time data. Our method extends this idea and we propose dynamical N-Gram tokenizer to reduce the index size and reduce the response time.

Trie tree, as a data structure makes its good performance in unknown words and variant length conditions [START_REF] Kanlayanawat | Automatic indexing for Thai text with unknown words using trie structure[END_REF][START_REF] Kijkanjanarat | Fast IP lookups using a two-trie data structure[END_REF]. In this paper we use Trie tree to maintain the added terms extracted from the query phrases and make a fast lookup for prefix check. N-Gram, as another useful technology, is always used in computational lan-guage and translation [START_REF] Doddington | Automatic evaluation of machine translation quality using ngram co-occurrence statistics[END_REF][START_REF] Brown | Class-based n-gram models of natural language[END_REF]. We integrate these two technologies to construct a dynamic analyzer that can be further used for indexing and searching.

3

The Proposed Method

In this paper we propose a method to effectively collect valuable information from text streams and it is composed of two key elements supporting the idea: the first one is maintaining an analyzer that adjust dynamically to the query and the maximum length used for N-Gram tokenizer; secondly, based on the tailored analyzer, the method collecting valuable data proposed by us is different from the conventional ones.

Dynamic Analyzer

The analyzer is essential for tokenizing the document in inverted document search system. The conventional analyzer is always static and doesn't keep pace with the input documents. Under the text stream environment, the data flow is always endless and the processing server should never stop. This causes serious problems including new words that will hurt the performance of the system. The common solution is to periodically rebuild all the documents or to use batch-incremental indexing method. These solutions will incur the high latency of the accurate results, the memory and space cost may be heavily grown along with the time goes by. The size of the data index is always expanding excessively and the valuable data always hides from normal search strategy.

To cope with the problems, we build and maintain a dynamic analyzer. We integrate the commonly used Trie data structure and N-Gram terminology to gain an effective and efficient analyzer.

Trie data structure coms from the word 'Retrieval' and it is a string tree. Its philosophy is to reduce time complexity by improving space complexity. The operations like INSERT and QUERY can be processed instantly and so it is commonly used as a lookup tables especially in PREFIX/SUFFIX computation settings. As an example to build a Trie, suppose the input terms are T=[ b, abc, abd, bcd, abcd, efg, hii ], the constructed Trie is illustrated in Figure 1. The red circle indicates a complete term through the root, the white circle indicates an intermediate node.

Fig.1. An Illustrative Trie Example

From Figure 1 we can see it is easy to retrieve all term that begin with a specified prefix, for example b and bcd are all begin with letter b. Trie can be used in suggestion complete to improve the search experience. In this paper we use them as a lookup table to store and search the query base.

N-Gram partitions the input into N continuous segments used for predicting in the form of (N-1)-Markov. N-Gram is very simple to understand and easy to scale up. We can simply increase the parameter N, then a model can be used to store more context with a space-time tradeoff, enabling experiments to scale up very efficiently. We implement the dynamic trie update algorithm in details in Algorithm 1. We sort the query to the leaf of the trie and update the maximum length of the query along with the construction process.

Algorithm 1. Dynamically update the Trie

Input: Given an empty or already existed Trie trie and query set qset. Output: An updated trie and maximum length N in the query base.

1. Extract all meaning and single words from the qset. We do this because there may be operators and quoted keywords. For simplicity, all the quoted letters are extracted to the set trimedQSet. 2. if trie is empty then 3.

Initialize trie; 4. N=0; 5. for each trimedQ in trimedQSet do 6.

Use trie to trimedQ to the trie leaf; 7.

if the length of trimedQ is larger than N then 8.

N:=length(trimedQ); 9. Output trie and N.

We segment the upcoming document according to the trie obtained in Algorithm 1, then extract the hit term and transfer them to the indexing or searching process. Algorithm 2 details how to segment the document accordingly. We segment the document content and return all the tokens existing in the trie.

Algorithm 2. Segment a document using analyzer based on N-Gram

Input: Given a document doc. trie, lookup tables for token search. N, the current maximum length among all the queries. Output: The tokens existing in the trie.

1. Extract the content content from doc. For indexing there may be other meta information, like timestamp, author etc.. In this step we just use content part like title and text.

tokens=[];

3. for i:=0 to length(content) do 4.

for j:=i+1 to i+N do 5.

token:=content.substring(i,j); 6.

if trie.contains(token) then 7.

tokens.add(token); 8. Output tokens.

In this part, we give two algorithms to show how to update trie and segment the document using N-Gram. The dynamic analyzer can insert the query fast and segment the input document, which makes the index size smaller than conventional method and collects valuable information according to the condition user specified.

Information Collecting Method

In the dawn of big data, the speed of the content generated grows fast. In some specific domains, people always want to focus the valuable information and filter out the information not relating to them. The traditional IR base methods require operating on the full data don't adapt to the data flow format. Another problem is the complex query conditions that will cost too much time to compute and load all the relative record from the index.

We propose an information-collecting method from another angle based on the previous dynamic analyzer. In the old-fashioned roadmap, documents are collected and indexed by the analyzer, then, the query are sent to the index repository, the possible BOOLEAN operation goes and the different RANK algorithms are used to sort the relative documents. Our work, however, index all the user query beforehand, we consider the incoming document as a query, if the score is larger than zero, we will collect it and store it, otherwise drop it. The score is a similarity between the query and the document, we could use VSM model to help calculating it easily. We illustrate the logic in Algorithm 3.

Algorithm 3. The method to collect valuable information from text streams

Input: Given endless text stream ts. analyzers, generated by each query. Output: Add the valuable document to its own list.

1. while true do 2.

Pick up a document document from the text stream; 3.

for each query in the querySet do 4.

Segment document using the corresponding analyzer, we get SEG; 5.

Similarity_Score:=sim(query,SEG); 6.

if Similarity_Score > 0 then 7.

Add document to the document list of this query.

We assume there are plenty of query sets and they are complex, which is very common in the platform of monitoring system, like traffic control of network, sensitive information detecting for a corporation. We obtain the valuable information through checking the each document to the query base from which the score is calculated as a metric for similarity distance.

Experimental Results

We conduct experiments on real data and make comparative results according to various settings.

Data Sets

We use Chinese patent data to evaluate the method proposed in this paper. The date range of the data is between 1985 and 2011 years. We extract all the keywords from the raw data and remove duplicated ones, and we get 350,000 distinct keywords. To simulate the text stream, we sort the document by the date and then iterate them in order.

Measurements of Trie Implementations

Since Trie is essential for our method, we evaluate the state-of-the-art implementations. The patricia-trie(for short PAT)2 and concurrent-trees (for short CT) 3 are used, and we compare the time cost and memory cost in each insertion with the number of keywords. All the keywords are inserted under the same condition; the results are illustrated in Figure 2. The time and memory cost change with the growth of the dictionary number. It is clear from the figure that PAT is always better than CT on both time and memory factors.

Performances of Analyzers

We evaluate our proposed dynamic analyzer( for short DA) with ICTCLAS [START_REF] Zhang | HHMM-based Chinese lexical analyzer ICTCLAS[END_REF] analyzer. ICTCLAS is based on HHMM and is considered as a baseline for many analyzers. In this paper we focus on not its performance but the index growth ratio and time cost about indexing speed with documents increase. We use Lucene 4 as an index engine. The document set is constrained to the subset of the total data. We used all the CLAIM and KEYWORD field in the patent during 2012s. We got totally 219,144 patents and 105744 keywords for PAT and the final maximum length is 7. Additionally, the maximum number can be adjusted according to the current dictionary and is able to cover the entire possible window for indexing.

Figure 3 illustrates the results, from the figures we can see our proposed analyzer DA could reduce the index size drastically and still it could reduce the index latency in each update. We should notice that the keyword is added dynamically when the patent document arrives; it proves the applicability of the dynamic mechanism proposed in this paper.

Performances of Collecting Methods

We compare our proposed method (for short Stream Search) and the traditional batchincremental method (for short BI Search). We test totally 40,000 patent documents. For text stream, the documents are sorted chronologically and are sent in order. For batch-incremental method, the size of documents is 1000 for each batches and the small index is merged to the big index. The Figure 4 gives an illustration of the two methods in time cost, what we can see is our method reduces the time cost to half of the batch-incremental method. To evaluate the soundness when the query is very complex and the combination of different joint operations, we increase the number of keywords and use OR and AND operation to evaluate the time cost for the batches with different document size, the results are listed in Figure 5. From the figures, we can see that the time increases linearly with the number of keywords, obviously, this phenomenon is reason-able in a practical production environment. Additionally, the AND operator is always cost much time than the OR operator.

Conclusions

In this paper, we propose and evaluate a new information-collecting method from fast text streams. Our experimental results indicate that dynamic analyzer based on N-Gram performs well in the speed for tokenizing, smaller index size and its automatic adaption character. The method considering the query set as index base and the incoming document as query can significantly reduce the time cost in fast text stream environment.

  Fig.1. An Illustrative Trie ExampleFrom Figure1we can see it is easy to retrieve all term that begin with a specified prefix, for example b and bcd are all begin with letter b. Trie can be used in suggestion complete to improve the search experience. In this paper we use them as a lookup table to store and search the query base.N-Gram partitions the input into N continuous segments used for predicting in the form of (N-1)-Markov. N-Gram is very simple to understand and easy to scale up. We can simply increase the parameter N, then a model can be used to store more context with a space-time tradeoff, enabling experiments to scale up very efficiently. As an example to generate an N-Gram sequence, suppose the sample S=ABCA, then the 1-gram sequences (also known as unigram) are [A, B, C, A], 2-gram sequences (also known as bigram) are [AB, BC, CA]. In this paper the base parameter N is set during the Trie construction process, so, it does not need predefined by an expert.We implement the dynamic trie update algorithm in details in Algorithm 1. We sort the query to the leaf of the trie and update the maximum length of the query along with the construction process.

2 .

 2 (a)Time Cost with the increase of the keywords count (b)Memory Cost with the increase of the keywords count Fig. Comparison of Time Cost and Memory Cost between CT and PAT with the Number of Keywords

3 .

 3 (a) Index Size changes with the increase of document size (b) Time Period changes with the increase of document size in each update Fig. Comparison of Index Size and Time Period between DA and ICTCLAS when Index Changes with the Document Size

Fig. 4 .

 4 Fig. 4. Time cost between Stream Search and BI Search with the document Size

Fig. 5 .

 5 Fig. 5. Comparison of Time Cost for OR and AND Operators with New Documents Added to the Text Stream

http://javasoze.github.io/zoie/

https://code.google.com/p/patricia-trie/

https://code.google.com/p/concurrent-trees/

http://lucene.apache.org

Acknowledgments

The work was financed by the National Program on Key Basic Research Project (973) (No. 2013CB329502), National Natural Science Foundation of China (No. 61035003, 61202212, 61072085), National High-tech R&D Program of China (863 Program) (No.2012AA011003), National Science and Technology Support Program (2012BA107B02).


Qingshan Li

Hua Chu
email: hchu@mail.xidian.edu.cn

Liang Diao
email: diaoliang@stu.xidian.edu.cn

Lu Wang
email: lu_wang@stu.xidian.edu.cn

Adaptive Mechanism Based on Shared Learning in Multi-agent System

Keywords: adaptive mechanism, shared learning, Multi-Agent System, system framework

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In the key application areas of software system, system environment is very complex, and the specific performance features are dynamic, changeable and difficult to control [START_REF] Szepesvá | Algorithms for reinforcement learning[END_REF]. Software systems with self-adaptive capacities can adapt to the changing environment better [START_REF] Meignan | Coalition-based metaheuristic: a selfadaptive metaheuristic using reinforcement learning and mimetism[END_REF]. In dynamic and uncertain environment, traditional techniques have been difficult to meet the development needs of self-adaptive systems [START_REF] Salehie | Self-Adaptive Software: Landscape and Research Challenges[END_REF]. In view of the above application requirements and technical challenges, this article uses the following two techniques to support the development of self-adaptive systems: Agent-based technology and reinforcement learning technology.

The second chapter of this paper introduces the self-adaptive system development framework; the third chapter focuses on the description of selfadaptive mechanisms based on shared learning, including self-adaptive processes and shared learning algorithm; the fourth chapter verifies the share learning-based self-adaptive mechanism proposed in this paper, combining case analysis; the fifth chapter summarizes the full text and discusses the further research.

Supporting framework for self-adaptive system development and running

By referencing FIPA specifications [START_REF] Kabysh | Influence Learning for Multi-Agent Systems Based on Reinforcement Learning[END_REF], we put forward the support framework of self-adaptive system for development and running as shown in figure 1. The entire frame consists of two core parts: supporting platform and development tools. The supporting platform provides communication services, event services, and capabilities of the agent lifecycle management, the interaction of distributed multiagent system and the perception of agent environmental.

Integrated control engine loads the user-specified integrated rules and distributes them to agents, so that the agents can collaborate independently under the guidance of integrated rules. Event registry maintains a list of all events in the system, which agent is interested in, and notifies the agent when the event occurs. Agent library management tool is a special agent in the platform. It is primarily responsible for the static management of local agent and the instantiation of agent.Sensor management module manages the different sensors, therefore the agent can dynamically load different sensors to active perception information of non-active in environmental.

Developers can develop needed configuration files for the system by using selfadaptive system development tools. User also can define collaborative relationships between agents by using a scripting language or graphical way. And user can abstract knowledge rules inside the appropriate agent, using scripting language describe knowledge rules to control the agent to process information automatically, so that the system can complete the decision-making process fast and accurately. Agent configuration tool mainly is used for defining simulation Agent basic information which is required.

Self-adaptive mechanism based on shared-learning

Reinforcement learning is considered to be one of the core technologies to design the intelligent agent [START_REF] Smarsly | Multiagent-based collaborative framework for a self-managing structural health monitoring system[END_REF]. To cope with unpredictable, dynamic environment in the process, self-adaptive system based on reinforcement learning will interact with the environment continually at runtime, and judge self-adaptive operations performed in a different state to formed knowledge.

Self-adaptive process based on shared-learning

In the self-adaptive system, agent is constantly monitoring the environment and sensing the current state of the environment, thus constantly triggering "perceptionselect-do-learning" process. At the same time, knowledge table is also constantly updated and maintained, which enables the agent to choose actions more responsive to environmental change according to knowledge table, improving effects that agent adapt to environment the gradually. Self-adaptive process based on shared-learning is shown in figure 3, the whole process can be divided into the following four steps:

Step1: (sensing stage) Agent interacts with the environment in real time to access the environmental information.

Step2: (decision-making stage) Agent sends the state of the environment (assume that the state is s) to behaviour selecting unit after perceiving environmental change; behaviour selecting unit selects a most appropriate behaviour (assume the action is b) from multiple behaviours which might be performed according to selecting policy and submitted to the execution units.

Step3: (implementation stage) Execution unit executes behaviour directly or executes by calling a number of external interfaces (such as communication interfaces, and so on). Implementation of behaviours may affect the state of the environment;

Step4: (learning stage) Learner is learning unit of self-adaptive agent, Learner has learning algorithm internal. Using state of environment and environment return value of action as entered, learner uses learning algorithm to learn optimal acts policy of self-adaptive agent in environment states, updates Q value that implement acts b at states. When the environment changes, self-adaptive agent calls actions or behaviours that are defined in the agent to adapt to the changes of environment according to knowledge exist in learner.

Algorithm of shared-learning

Multi-Agent Collaborative reinforcement learning algorithm proposed in this paper is combined with the rules of knowledge and experience sharing between tuples. The knowledge obtained from each Agent independently learning and convergence will have an appropriate similarity transformation to get a shared experience tuples, which will achieve the solving method sharing about the similar problem. Meanwhile the status and action of the shared experience tuples will be designed as the rules of knowledge and stored in the rule base. While the Multi-Agent system is running, each Agent first query the rule base, match the conditions of rules. If satisfied, then the corresponding actions of the rules matched will be taken. If not, the Agent will turn in the state of the self-learning, get the convergence of the pair of the state and action, then convert it into a shared experience tuples, design rules, finally store this rule into the rule base. A unified space of the behaviour states has achieved by this algorithm through the sharing of the tuples' experience and the rules of knowledge to improve the efficiency of self-learning Agent module. S: States set is which agent concern, S= {s1, s2 ...}; A: Actions set is defined in agent, A= {a1, a2 ...}; 1. Query the rules in the rule base, if the current state is satisfied with the conditions of rules, then the corresponding action will be executed, otherwise the intensive learning will be executed as (2); 2. Initialization: S = s, Q (s, a) = 0, in which∀s∈S,∀a∈A;

3. Choose an action "a" based on a ε-greedy strategy;

4. the Agent performs an action "a" to get the immediate return "r" and the next state "s'";

5. update Q: Q(s, a)≔ A(s, a)+α(r + γ max a, Q(s', a')-Q(s, a))

Where γ is the discount, α is learning rate.

6. s = s', if all of the Q (s, a) are convergent, executed (7), else (3); 7. reset Agent initial state, repeat 2-6 steps, the learning process will be executed several times until the Q (s, a) is convergent, then the study task could be considered as completed.

8. Each the pair of the state and action obtained by the Agent using the Q-learning will have a similarity transformation to get the shared experience tuple (s *, a *). And the tuple will be designed as rules in which the state is the condition and the behaviour is the action. The rules will be stored into the rule base, when the conditions of the rules are met, the corresponding action will be executed.

In the initialization part of the algorithm, we build the Q table and initialize the Q value of each state-behaviour to 0. Of course, Q can also be set into a more meaningful value for experienced designers to speed up the convergence of learning. When algorithm get into the loop part, it will execute the process "choice behaviourimplement behaviour-receive return value-watch the new state-update Q table-set up the next loop starting state-choice behaviour ...-update Q table ..." repetitively. When all the values in the table of sharing-experience tuple become convergence, the loop is end.

Self-adaptive mechanism based on shared-learning

In this chapter, we implement an air defence command and control system to intercept intrusion target. As shown in Figure 3, our three UVAs are flying in the area near the border and decide flight behaviour according to the current location of the intrusion target. Learning trail of shared learning algorithm is the return value from the simulated environment of simulation system and three aircraft shares experience tuple what they have learned.

Figure 3. Situation maps of UAV formation intercept invasion target

System running

When agent initialization is completed, each agent receives information from the outside and works in terms of internal knowledge rule file. The generated messages is sent out though collaborative relationship. Agents finish the blocking process through collaborative interaction. Agent communication processes is shown in Figure 4.

Results and analysis

Set the appropriate parameters for the problem of interception of UAVs to make shared learning algorithm meet the required conditions. Experimental basic conditions are as follows, a series of successor experiments have been conducted on the basis of change different basic conditions.

(1)The UAV and intrusion target selecting one walking behaviour randomly, behaviour collections are represented as {eastbound, westbound, northbound, southbound, stationary}; [START_REF] Meignan | Coalition-based metaheuristic: a selfadaptive metaheuristic using reinforcement learning and mimetism[END_REF]The UAV has the ability to learn and make independent decisions respectively, by receiving feedback information of environment to improve its policy; (3)Do not have shared experiences tuple; (4)Assume that initial Q value of each state-behaviour to 0;(5)Instantaneous return functions which environment feedbacks to the UAV are as follows: This section verifies the effectiveness of shared learning and different return values impact of the system learning though two contrast experiment. The result is shown in Figure 6. In the figure, horizontal represents the number of experimental group, each group represents l0 flight simulation, and ordinate represents the moving times of unmanned plane in each set of experiment.

Global perception and experience sharing Effects of feedback on learning

Figure 6. The effect of different feedback value to learning

Setting return value of increase distance between ion task and target location with a step to-50 make the algorithm get a faster convergence effect. Through these two experiments, the following conclusions can be obtained: shared-learning algorithm is effective for multi-agent team and come to convergence under certain conditions; Collaborative learning between agents can improve the learning efficiency of multi-agent team. The return value which acts as the only clue of learning, different set of return values can bring to different effect of the system's learning.

Conclusion

Adaptive mechanism based on shared learning in Multi-Agent System This paper proposes an operation mechanism and learning algorithm for selfadaptive multi-agent system, which makes the self-adaptive agent have the learning capacity and can use the learning algorithm to learn related knowledge of environment online, can develop out effective self-adaptive policy according to the change of environment. All of these enhances the self-adaptive capacity of the system in dynamic and uncertain environment greatly.

This major work of this paper can be summarized in several areas:  This paper introduces the reinforcement learning technology and agent technology in the area of self-adaptive systems research, proposes self-adaptive mechanism of self-adaptive system under uncertainty environment, and the corresponding learning algorithm for selfadaptive agent to support the learning process.

 This paper develops a specific application, presented the development process of the case, showing the actual performance of the selfadaptive agent with learning ability, verify the legitimacy and effectiveness of the methods described in this paper.

Figure 1 .

 1 Figure 1. Supporting framework of self-adaptive system for development and running

Figure 2 .

 2 Figure 2. Self-adaptive process based on shared-learning

Figure 4 .

 4 Figure 4. Interface of explain and distribute integrated script

Comparative experiment 1 Figure 5 .Table 2 .

 152 Figure 5. Verification for effectiveness of shared-learningIn the case of all area perceptions, UAVs can reach agreement on how to intercept invasion targets as soon as possible; learning between the UAVs is the synchronization. After a running process of learning, agent is able to achieve the effect of convergence of expectations. This experiment will change the basic conditions (3) form not shared experiences tuple to share experiences tuple, each UVA uses a shared learning algorithm for learning. Seen from the experimental results, compared with does not use shared experiences, agent uses shared experiences can convergence to stable values faster, this indicates that the shared learning algorithm to significantly improve the efficiency of collaboration.Comparative experiment 2 UAVs execute task of blocked, comparison curve of moving times between before change return values and after change return values.On basis of experiment 1, we change return values set to try to observe the influence of return value on learning. We change return value set of basic condition[START_REF] Smarsly | Multiagent-based collaborative framework for a self-managing structural health monitoring system[END_REF] to:

Table 1 .

 1 Return value which environment feedbacks to the UAV

		arrive at the target	the distance to target reduce one step	the distance to target is decreasing	the distance to target keep unchanged	the distance to target increase one step	the distance to target is increased
	r	300	100	100	0	-1	-10

Acknowledgment

This work is supported by the Projects (61173026, 61373045, 61202039) supported by the National Natural Science Foundation of China; Projects (BDY221411, K5051223008, K5051223002) supported by the Fundamental Research Funds for the Central Universities of China; Project (513***103E) supported by the Pre-Research Project of the "Twelfth Five-Year-Plan" of China; Project (2012AA02A603) supported by the National High Technology Research and Development Program of China.


Fu Hou

Xinjun Mao
email: mao.xinjun@gmail.com

Junwen Yin

Wei Wu

An Agent-Based Autonomous Management Approach to Dynamic Services

Keywords: dynamic services, software agent, autonomous management, service situation

published or not. The documents may come

Introduction

Service-Oriented Computing (SOC) paradigm has gained popularity today for supporting the development of rapid, low-cost, interoperable, evolvable, and massively distributed applications. It is promised to easily assemble application components into a loosely coupled network of services that span organizations and computing platforms etc. [START_REF] Papazoglou | Service-oriented computing: a research roadmap[END_REF]. Web services are currently the most promising SOC based technology. Several technologies and standards have been proposed to manage the web services, e.g. WSDL to describe the services, SOAP to access service etc., for service-based applications development and invocation. Based on the technologies and standards, service provider registers web service in registry with some basic information e.g. operations, binding port, etc., if application intends to invoke some service, it will look up the registry to get the required service information, and then access the service in term of SOAP.

However, the services over Internet are dynamic, evolving and growing due to the changes of the requirements and operating contexts. One typical case is the evolving changes of web service's QoS. Doubtlessly, to determine the service to be accessed at design-time or only by considering the functionality information of service seems unfeasible, because the expected service may be unavailable or more suitable services for applications may arise due to the dynamic of services at runtime. This leads to the requirements of managing the dynamics of services in an autonomous and transparent way. Obviously, the autonomous management of services requires to perceive, organize, acquire the dynamic of services, and to decide which service should be accessed and invoked to satisfy the application requirements according to the dynamic information. There are several ways to tackle the issues: one is to re-construct web services and provide them with the capabilities of managing dynamics and providing autonomous decision. The other is to enrich the applications with the capabilities of monitoring the dynamics of services and of autonomy on the access of the expected services. However, both of these methods are complex because they need to modify the existing services or applications.

Software agent technology gives us inspirations about how to manage and organize the dynamic services. First, agent is context-aware, which means it can sense the situated environment. If we provide the monitoring capabilities for agents, they can perceive the dynamic information of services. Second, agent is autonomous on behaviours, which means agent can decide which behaviours should be performed according to its internal state and external requests. Therefore, we can access services by agent in an autonomous and flexible way. Third, agent is expected to be social, which means multiple agent can interact and cooperate with each other in order to achieve global objectives. Therefore, the complex management or organization can be achieved in term of the interaction of agents. Moreover, software agent technology enable legacy systems to be incorporated with new functions and capabilities.

The remainder of this paper is structured as follows. Section 2 discusses the related works about service management methods and the utilization of agent technology into service-oriented computing. Section 3 overviews the technical framework to manage dynamics of services. Section 4 details the management model and situation model of dynamic services, and presents the implementation architecture and the autonomous management process of dynamic services. Section 5 introduces a prototype platform -ServiceAutoManager that implements the above technologies and supports the autonomous management of dynamic services, and a web service application of travel searching is discussed to show the effectiveness of our proposed approach. Conclusions and future works are made in section 6.

Related Work

As more and more evolving and dynamic services are deployed on Internet, how to manage the dynamic of services has obtained great attentions from both industry and academic fields. Several attempts have been made in the past years, most of them focus on the service operation management. A typical work is to establish the registry management pattern based on SOA [START_REF] Papazoglou | Web Services Management: A Survey[END_REF], e.g. ESB, and there are also some researchers propose web service distributed management which essentially defines a protocol for interoperability of management information and capabilities in a distributed environment via Web services [START_REF] Kreger | Management Using Web Services: A Proposed Architecture and Roadmap[END_REF]. Recently seeding autonomic capabilities for service level management is an evolutionary service level management approach where autonomic computing capabilities anticipate IT system requirements and resolve problems with minimal human intervention [START_REF] Papazoglou | Service-oriented computing: a research roadmap[END_REF]. E.g. Yu Cheng et al. propose a prototype architecture and discuss related implementation issues for an autonomic service management framework [START_REF] Cheng | Toward an autonomic service management framework: A holistic vision of SOA, AON, and autonomic computing[END_REF]. Bhakti et al. present the idea of adapting the autonomic computing paradigm into SOA to dynamically (re)organizing its topologies of interactions between the services with little human intervention [START_REF] Bhakti | Autonomic, self-organizing service-Oriented Architecture in service ecosystem[END_REF].

Software agent techniques have been extensively exploited to solve issues occurring in several areas. They use software agent to implement the adaptive process, service composition, service selection and even a broker. E.g. Yu Fei Ma et al. present a lightweight autonomous agent fabric for Web service [START_REF] Ma | A lightweight agent fabric for service autonomy[END_REF]. Lopes and Botelho present a framework to enable the execution of semantic Web services using a context-aware broker agent [START_REF] Lopes | Executing semantic Web services with a contextaware service execution agent[END_REF]. Sreenath and Singh proposes a new agentbased approach in which agents cooperate to evaluate service providers [START_REF] Oyenan | Design and evaluation of a multi-agent autonomic information system[END_REF]. Chainbi et al present an agent-based framework for autonomic web services which is based on two agent-based systems collaborating to enrich web services and registries with self-* capabilities [START_REF] Chainbi | AFAWS: An Agent based Framework for Autonomic Web Services, Multi agent and Grid Systems[END_REF].

Agent-based Technical Framework of Managing Dynamics of Services

In order to manage the dynamic of services and support applications to flexibly access services, we propose an agent-base technical framework (see Fig. 1). In this framework, services are to be managed by a number of managers that are actually software agents. Each service manager can manage one or more services, and each service corresponds to at most one manager. Developer should explicitly describe the management relationship between the service and service manager at deploy-time. Such relationship can be dynamically adjusted at runtime in term of self-organizing of multiple service managers in order to achieve the re-organization and optimization of the management relationships. When the relationship is established, the infrastructure of services is responsible for monitoring the dynamics of the managed services and sending the dynamic information to the service managers. The managed services together with their dynamic information consist of the internal resources and states of service manager. The service managers should register at the service manager center. The registered information includes the agent ID and address of manager, the managed services, etc. Therefore, service manager center knows what the functions services provide, and who are responsible for managing these services. Applications that intend to access some service should first look up service manager center to obtain the information about which agent is responsible for managing the service that satisfies the expected functions. Then applications send request that describes the expected functions, constraints and corresponding parameters to the service manager. According to the requests and the dynamics of the managed services, service manager decides which service is more suitable for providing the function, and then access the service and return the service results.

4 Approaches to Autonomous Management of Services Before service manager begins to manage services, developers should deploy the service into service container and explicitly define service's configuration file. There are two types information in configuration file: service access information and the monitored dynamic aspects of the service. When the services are deployed in the container, container is responsible for enrolling the configuration information into the service manager. b) Service Monitoring. According to the monitored aspects of dynamics, service manager is responsible for monitoring the dynamics of services and maintaining the dynamic information. In this paper, we provide a situation model of service that covers several aspects of dynamics, including satiated context, quality status, and business capability. When service manager gets the configuration information of service, it will monitor the services and obtain the dynamic information of services based on the infrastructure. c) Services Invocation. Once the enrolment of management relationship and service monitoring are established, service manager can autonomously manage and invoke the services. When receiving service requests from applications, service manager will find and access the proper services that satisfy the request.

Implementation Architecture of Service Manager

In the above abstract model, service manager is the core to achieve the objective of service's autonomous management. Based on the reactive agent architecture we propose the implementation architecture of service manager (see Fig. 3). In Fig. 3 we can see that service manager is comprised of six basic modules: c) Collaboration Unit. Collaboration unit is to perform the interactions among service managers in order to achieve the collaborations. The purpose of collaboration may be querying services managed by other managers or selforganizing among managers to reorganize the managed services in different managers. d) Decision Unit. Decision unit is the component to decide which service managed by the manager is more suitable for the service request. The decision process is based on the composite considerations on the service request and the service dynamics and triggered by the service request. e) Request Analyst. Request analyst is responsible for analysing the service request from application, interacting with the decision unit to obtain the expected service, and returning the service results to the applications. f) Situation Sensor. Situation sensor is in charge of monitoring the managed services and obtain their dynamic information. It is also responsible for interacting with the service pool to store the perceived information.

Autonomous Management Process of Services

The autonomous management process for services consists of several phases in which different components and agents are involved and cooperated (see Fig. 4). First services are to be deployed into service container that supports the running of services and maintains the meta information of services. Then service container sends enrolment request to manager in order to establish the management relationship between the service and the manager. b) Service Monitoring Phase. First services are to be deployed into service container that supports the running of services and maintains the meta information of services. Then service container sends enrolment request to manager in order to establish the management relationship between the service and the manager. c) Service Access Phase. Request from application will trigger the process of accessing service. Typically, such request will be pre-processed by the request analyst, and request analyst will interact with the decision unit to find the proper service. Then service analyst will invoke the service and return result to application. d) Autonomous Decision Phase. Once an application request trigger the decision unit, the autonomous decision process will begin. First decision unit will look up the service pool and perceive the service situation if there exist the suitable service that satisfies the request, decision unit will return the service. If there is no proper service, the decision unit will collaborate with other managers to obtain the proper service.

Service Situation Model

With the proliferation of services as a business solution to enterprise application integration, the QoS is becoming increasingly important to service providers [START_REF] Lee | QoS for Web Services: Requirements and Possible Approaches[END_REF]. However, various applications with different QoS requirements will compete for network and system resources e.g. bandwidth and processing time, so QoS is not enough to describe the dynamics of service. In this paper we propose a situation model of service to describe and define the service dynamic aspects covering situated context, quality status and business capabilities (see Fig. 5). Situated context describes the utilization status of network and system resource (e.g. bandwidth etc.). Quality status describes the service qualities aspects status information, including performance (e.g. throughput, response time etc.), capacity (e.g. the limit of the number of simultaneous requests), accuracy (e.g. the number of errors), and availability. Business capability describes business capability status information of service. For example, the current positioning precision of GPS's position service.

ServiceAutoManager Platform and Case Study

In order to support the autonomous management of services and corresponding development tasks, we have developed a prototype platform called ServiceAu-toManager. ServiceAutoManager integrates Jade and Tomcat together, and provides the autonomous management functions for services. The implementation framework of ServiceAutoManager consists of four layers (see Fig. 6). In the following we give a case study to illustrate the above technologies and platform. The case is about travel searching problem, namely from A position to B position to find a path which satisfies user requirement with cellphone map searching application. In this paper we assume that the searching process needs three types of services: position service, path information service and taxi service. To reach B with the shortest time we need a position service to locate the position of B, and based on the path information service we will get some paths, and depending on the path status we need select one path and take taxi to B. This process is an artificial process, we hope this process can be implemented on the cellphone application, we assume that at the time there are three position services, four path information services and six taxi services, where the positioning precision P 1 of position service PS 1 satisfies P 1 ≥ 30m, position service PS 2 satisfies P 2 ≥ 10m and position service PS 3 satisfies P 3 ≥ 25m; the current ratio of traffic jam respectively is: R P IS1 = 6%, R P IS2 = 3%, R P IS3 = 8%, R P IS4 = 7%, and the ratio of traffic jam is dynamic ; the response time of taxi respectively is: T = 2min, T 2 = 4min, T 3 = 6min, T 4 = 5min, T 5 = 3min, T 6 = 10min, the services and their managers relationship diagram sees Fig. 7. We design the travel searching application under above hypothesis, the application accesses services process is: Firstly, find a Service Manager namely SManager5 from service manager centre. Secondly, define the service requirements of application, the requirements just are the service situation constraints: 1).The requirement of position service: the positioning precision P of position service satisfies P ≤ 20m; 2).The requirement of path information service: the current ratio R of traffic jam satisfies R ≤ 5%; 3).The requirement of taxi service: the response time T satisfies T < 3min. Thirdly, access the services based on requirements, in this process service manager will autonomously and transparently return the service results, in this case the results are PositionService2, PathInformationService4 and TaxiService1.

Conclusions and Future Work

This paper researches the autonomous management technologies of services due to the dynamic of services and the requirements of flexible and transparent service access. Different from related works, we adopt agent as technical solution and design service managers to perceive, organize and maintain the dynamics of services, and to further decide which service should be invoked according to the service request and situation. Service managers are actually agents that encapsulate services, manage their dynamic and provide autonomous service access. Developer only needs to explicitly claim the management relationship between service managers and the managed services. Therefore, our approach enables us to manage services promote the reuse and re-organization of legacy service systems. In order to support service's autonomous management based on the agent-based technical framework, we have presented situation model of service and implementation architecture of service manager that answer what the dynamic information should be managed and how to manage the dynamic service in an autonomous way respectively. We have developed a prototype platform called ServiceAutoManager based on Jade and Tomcat, and studied a travel searching case to illustrate the proposed approach.

The future works include: (1) the self-organization and collaboration among service managers to re-organize the managed services; (2) self-adaptation technologies for accessing web services in term of the changes of both requests, situated contexts and the dynamic of service itself; (3) more experiments to analyse the richness and weakness of our proposed approach.

Fig. 1 .

 1 Fig. 1. Agent-based Technical Framework of Managing Dynamics of Services

4. 1

 1 Fig.2depicts the abstract model of service management respecting the above technical framework, in which service managers are designed to manage the dynamics of services, decide and invoke the services to satisfy the applications requests. The whole management consists of three aspects: service enrolment, service monitoring and service invocation.

Fig. 2 .

 2 Fig. 2. Model of Services Management

Fig. 3 .

 3 Fig. 3. Implementation Architecture of Service manager

Fig. 4 .

 4 Fig. 4. Autonomous Management Process Sequence Diagram of Services

Fig. 5 .

 5 Fig. 5. Situation Model of Dynamic Service

Fig. 6 .

 6 Fig. 6. Implementation Framework of SAutManager Platform

Fig. 7 .

 7 Fig. 7. Diagram of Travel Searching Case Services and Service Managers Relationship

Acknowledgments. The research leading to these results has received funding from National Nature and Science Foundation of China under Granted Nos.61379051 and 61133001, Program for New Century Excellent Talents in University under Granted No. NCET-10-0898 and Open Fund State Key Laboratory of Software Development Environment under Granted No. SKLSDE-2012KF-0X.


Meiying Sun
email: sunmeiying07@mails.ucas.ac.cn

Shaobo Deng

Yuefei Sui

The Correspondence between Propositional Modal Logic with Axiom φ ↔ φ and the Propositional Logic

Keywords: propositional modal logic, propositional logic, disjunctive normal form, pseudo-atomic formula, pseudo-atom-complete, completeness

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Van Benthem gave the standard translation [START_REF] Van Benthem | Modal correspondence theory[END_REF][START_REF] Blackburn | Handbook of Modal Logic[END_REF] from the propositional modal logic into the first-order logic. The necessity operator □ corresponds to the universial quantifier ∀ via the standard translation and every modal formula corresponds to a first-order formula. Benthem discussed connections between modal axioms and first-order properties of the accessibility relation among worlds in the paper [START_REF] Van Benthem | Correspondence Theory[END_REF]. For example, the formula □p → p is valid on all reflexive frames. In order to solve the classical problems arising from the interplay between propositional attitudes, quantifiers and the notion of identity, Aloni proposed the conceptual covers semantics of the first-order modal logic [START_REF] Aloni | Quantification under Conceptual Covers[END_REF][START_REF] Aloni | Individual Concepts in Modal Predicate Logic[END_REF].

There are a number of systems of propositional modal logic, like K, D, T, S5, Triv and Ver. Trivially, K is a subsystem of all the others, and every normal 1 modal system1 is contained either in Triv or in Ver. We also have that every consistent system which contains D is contained in Triv [START_REF] Hughes | A New introduction to Modal Logic[END_REF]. Each formula in S5 can be equivalent to a formula in the modal conjunctive normal form [START_REF] Hughes | A New introduction to Modal Logic[END_REF], and each conjunct is the disjunction of φ or □φ or ♢φ, where φ is a formula of the propositional logic. This makes the proof of the completeness of S5 much easier and provides an effective procedure for determining whether or not a formula is a theorem of S5 and S5-valid [START_REF] Hughes | A New introduction to Modal Logic[END_REF]. Similarly, Triv can collapse into the propositional logic and Ver provides a different form of collapsing into the propositional logic [START_REF] Hughes | A New introduction to Modal Logic[END_REF].

In the propositional logic, any formula is equivalent to a formula in the disjunctive normal form and each disjunct is the conjunction of atomic formula or its negation [START_REF] Hamilton | Logic for Mathematicians[END_REF]. If there is a modal system S such that each formula can also be equivalent to a formula in the disjunctive normal form, then we can easily get a correspendence between S and the propositional logic. In K necessity can only be distributed over conjunction and possibility can only be distributed over disjunction. In order to distribute necessity over disjunction, we add the axiom □φ ↔ ♢φ to K and construct a new normal modal system K + .

In K + necessity can be distributed over conjunction and disjunction. And it is easy to prove that the formula □¬φ ↔ ¬□φ is a theorem of K + . Therefore the system K + has a remarkable property that any formula can be equivalent to a formula in the disjunctive normal form and each disjunct is the conjunction of pseudo-atomic formulas □ k p(k ≥ 0) or the negation of a pseudo-atomic formula. Then discussions of logical properties of K + reduce to discussions of logical properties of the propositional logic.

We have the concept of atom-completeness in the propositional logic, and in K + we correspondingly give the definition of pseudo-atom-completeness. In K + for any pseudo-atom-complete set A of formulas, if we delete one □ from each φ in A then the new set □ -A is also pseudo-atom-complete. Each atom-complete set of formulas in the propositional logic determines a maximally consistent set in a unique way. Similarly, each pseudo-atom-complete set of formulas in K + uniquely determines a maximally consistent set. So the accessibility relation in the canonical model [START_REF] Hughes | A New introduction to Modal Logic[END_REF] of K + can be simply given by eliminating one □ from each pseudo-atomic formula in a possible world.

Assume that P + = {q ki : k, i ≥ 0} is a language of the propositional logic. When a pseudo-atomic formula □ k p i (k, i ≥ 0) is corresponding to a propositional variable q ki , each formula in K + then can be corresponding to a formula in P + . Then we can prove that any theorem of K + can be corresponding to a theorem of P + , and vice versa. The semantics of K + is the possible world semantics, which is a set of models of P + . For any model M of K + and any possible world w in M we can construct an assignement v w of P + such that for any formula φ of K + , M, w |= φ if and only if v w |= φ ′ , where φ ′ is the cor-responding formula of φ. Then we can prove that any valid formula of K + can be corresponding to a valid formula of P + , and vice versa. So, the soundness theorem and the completeness theorem of K + follow directly from those of P + .

This paper is organized as follows: the next section gives the basic definition of the propositional modal logic K; the third section defines the propositional modal logic K + and gives the disjunctive normal form of formulas in K + ; the fourth section defines pseudo-atom-complete, and proves that each maximally consistent set of formulas is uniquely generated by a pseudo-atom-complete set of formulas; the fifth section gives correspondences between K + and the propositional logic P + , and get the soundness and completeness of K + ; and the last section concludes the whole paper.

2

The propositional modal logic K

This section gives the basic definitions of the propositional modal logic K, including the language, the syntax and the semantics, where the syntax gives the definitions of formulas, axioms and inference rules; and the semantics defines the models, satisfaction and validity. K is sound and complete, and proofs can be found in [START_REF] Hughes | A New introduction to Modal Logic[END_REF][START_REF] Fitting | First-order Modal Logic[END_REF]. Let the logical language L of the propositional modal logic contain the following symbols:

• propositional variables: p 0 , p 1 , ...;

• logical connectives: ¬, →;

• the necessary modality: □;

• auxiliary symbols: (, ).

A formula of the propositional modal logic is defined as follows2 :

φ ::= p|¬φ 1 |φ 1 → φ 2 |□φ 1 .
The possible modality ♢ and the necessary modality □ are dual. For any formula φ, ♢φ = df ¬□¬φ.

Definition 1 A frame F of the propositional modal logic is an ordered pair ⟨W, R⟩, where W is a non-empty set of possible worlds, and R ⊆ W 2 is a dyadic relation defined over the members of W .

For any possible worlds w, w ′ ∈ W , (w, w ′ ) ∈ R is usually denoted by wRw ′ . Frames can be classified by the relation R, and details of the classification can be found in [START_REF] Hughes | A New introduction to Modal Logic[END_REF][START_REF] Fitting | First-order Modal Logic[END_REF]. Definition 2 A model M is an ordered triple ⟨W, R, I⟩, where ⟨W, R⟩ is a frame; and I is an interpretation such that for any propositional variable p, I(p) ⊆ W.

A model ⟨W, R, I⟩ is said to be based on the frame ⟨W, R⟩. A model we define here is called a standard model, which is different from a Kripke model [START_REF] Kripke | Semantical analysis of modal logic I: Normal modal propositional calculi[END_REF]. You can see the difference between them in [START_REF] Hazen | Actuality in Propositional Modal Logic[END_REF] and any standard model can be transformed into a Kripke model [START_REF] Hazen | Actuality in Propositional Modal Logic[END_REF].

Definition 3 Given a model M , for any possible world w, M, w |= φ if and only if

       w ∈ I(p) if φ = p, M, w ̸ |= φ 1 if φ = ¬φ 1 , M, w |= φ 1 ⇒ M, w |= φ 2 if φ = φ 1 → φ 2 , Aw ′ ((w, w ′ ) ∈ R ⇒ M, w ′ |= φ 1 ) if φ = □φ 1 ,
where Aw ′ means "for any possible world w ′ ". We will give definitions of validity of formulas in a model, a frame and a class of frames. Given a set Γ of formulas and a formula φ, and C is a class of frames, φ is a logical consequence of Γ in C, denoted by

Γ |= C φ, if for any frame F ∈ C and model M based on F , M |= Γ implies M |= φ.
In this section we mainly talk about the system K, which is characterized by all frames. So we will use Γ |= φ to denote Γ |= C φ.

In the following we will give the axiom system of the propositional modal logic K.

Axioms:

φ 1 → (φ 2 → φ 1 ), (φ 1 → (φ 2 → φ 3 )) → ((φ 1 → φ 2 ) → (φ 1 → φ 3 )), (φ 1 → φ 2 ) → (¬φ 2 → ¬φ 1 ), □(φ 1 → φ 2 ) → (□φ 1 → □φ 2 ).
Inference rules:

(MP) φ 1 , φ 1 → φ 2 φ 2 , (N) φ 1 □φ 1 .
The last axiom is called the axiom K. The system we given above is called the system K of the propositional modal logic. It is sound and complete. We will only give the soundness theorem and the completeness theorem here, and the details of their proofs can be found in [START_REF] Hughes | A New introduction to Modal Logic[END_REF] and [START_REF] Fitting | First-order Modal Logic[END_REF].

3

The new system K + and the disjunctive normal form

Let K + be the propositional modal system obtained by adding to K the following axiom:

K + □φ ↔ ♢φ.
Then the necessary modality □ is equivalent to the possible modality ♢. In K we have the theorems about the distributivity of □ over ∧ and the distributivity of ♢ over ∨ [START_REF] Hughes | A New introduction to Modal Logic[END_REF]. So in K + we can easily get the following theorems about the distributivity of □ over ∧ and ∨. Proposition 1.

(i) ⊢ □(φ ∧ ψ) ↔ (□φ ∧ □ψ); (ii) ⊢ □(φ ∨ ψ) ↔ (□φ ∨ □ψ).
□ Each formula in the propositional logic is equivalent to a formula in the disjunctive normal form [START_REF] Hamilton | Logic for Mathematicians[END_REF]. Similarly, each formula in the system K + can also be equivalent to a formula in the disjunctive normal form, where □ i (i ≥ 0) only occurs before an atomic formula, and ¬ only occurs before a pseudoatomic formula of form □ i p, where p is an atomic formula. In the following we will first give the definitions of pseudo-atomic formula and the disjunctive normal form, and then prove that each formula in K + is equivalent to a formula in the disjunctive normal form.

Definition 5. A formula φ is pseudo-atomic if φ = □ k p, where k ≥ 0 and p is a propositional variable. Definition 6. A formula φ is in the disjunctive normal form if

φ = φ 1 ∨ φ 2 ∨ • • • ∨ φ n ,
where for each 1 ≤ i ≤ n,

φ i = ψ i1 ∧ • • • ∧ ψ imi ,
where for each 1 ≤ j ≤ m i ,

ψ ij =∼ lij □ kij p ij ,
where

□ kij = k ij -many □s □ • • • □ ; ∼ lij = { ¬ if l ij = 1, λ if l ij = 0,
and p ij is a propositional variable, where λ is the empty string. Similarly, we can define the conjunctive normal form. In this paper we will use the disjunctive normal form only. For simplicity, we call it the normal form. Since the propositional modal logic is obtained by adding □ to the propositional logic, and □ can be distributed over ∧ and ∨ in K + , we can get the conclusion that for any formula ψ of K + , we have a formula φ in the normal form which is equivalent to ψ.

Proposition 2. For any formula ψ, there is a formula φ in the normal form such that ⊢ ψ ↔ φ.

Proof. By induction on the construction of the formula ψ. □

Pseudo-atom-complete set of formulas

In this section we give the definition of pseudo-atom-complete. In the propositional logic an atom-complete set determines a maximally consistent set in a unique way. Similarly, in K + a pseudo-atom-complete set determines a maximally consistent set in a unique way. In K + for any pseudo-atom-complete set A of formulas, if we delete one □ from each φ in A then the new set □ -A is also pseudo-atom-complete. And the accessibility relation in the canonical model of K + can be simply given by eliminating one □ from each pseudo-atomic formula in a possible world.

Let A be a maximally consistent set of formulas in the propositional logic. For any propositional variable p, exactly one member of {p, ¬p} is in A. Definition 7. A set A of atomic formulas or the negation of atomic formulas is atom-complete if for any atomic formula p, exactly one member of {p, ¬p} is in A.

Proposition 3. An atom-complete set A determines a maximally consistent set in a unique way.

Let B be a maximally consistent set of formulas of K + . For any pseudoatomic formula □ k p, exactly one member of {□ k p, ¬□ k p} is in B. Definition 8. A set A of pseudo-atomic formulas or the negation of pseudoatomic formulas is pseudo-atom-complete if for any pseudo-atomic formula □ k p, exactly one member of {□ k p, ¬□ k p} is in A.

For any maximally consistent set B of formulas, let

σ(B) = {∼ l □ k p :∼ l □ k p ∈ B}.
Then, σ(B) is pseudo-atom-complete. Proposition 4. For any pseudo-atom-complete set B of formulas, there is a unique maximally consistent set C of formulas such that

σ(C) = B.
Proof. It is easy to see that B is consistent. So by the theorem of Lindenbaum we can extend B to a maximally consistent set C of formulas and it satisfies the condition that σ(C) = B. Then we can prove that C is unique by contraposition.

□ Theorem 3. For any pseudo-atom-complete set A,

□ -A = {∼ l □ n-1 p :∼ l □ n p ∈ A and n ≥ 1} is pseudo-atom-complete.
Proof. By the definition of pseudo-atom-complete. □ For any set B of formulas, let

□ -(B) = {φ : □φ ∈ B}.
Let W be the set of all maximally consistent sets, and R □ be the binary relation on W. For any possible worlds w, w ′ ∈ W, (w,

w ′ ) ∈ R □ if and only if □ -(w) ⊆ w ′ .
Corollary 1. Given a pseudo-atom-complete set A, let τ (A) be the unique maximally consistent set such that σ(τ (A)) = A. Then,

{τ (A), τ (□ -A), ..., τ (□ -n A), ...} is a set of possible worlds such that (i) (τ (A), τ (□ -A)) ∈ R □ , and (ii) for any n ≥ 1, (τ (□ -n+1 A), τ (□ -n A)) ∈ R □ .
Proof. We can prove (i) by contraposition. From the theorem 3 and the proposition 4 we can also prove (ii) with the same method of (i). □

Correspondences between K + and the propositional logic

In this section we build correspondences between K + and the propositional logic P + . When a pseudo-atomic formula □ k p i (k, i ≥ 0) is corresponding to a propositional variable q ki , each formula in K + then can be corresponding to a formula in the propositional logic P + . We also get the correspondence of models between K + and P + . Then we get correspondences of theorems and valid formulas between them. So, the soundness theorem and the completeness theorem of K + follow directly from those of P + . Suppose that P + = {q ki : k, i ≥ 0} is a language of the propositional logic. In order to give the correspondence between K + and P + , we firstly redefine a formula φ in the normal form of K + .

θ ::= □ k p i |¬□ k p i ; ψ ::= θ|ψ 1 ∧ ψ 2 ; φ ::= ψ|φ 1 ∨ φ 2 .
where k, i ≥ 0 and p i is a propositional variable of K + .

Then we define a mapping σ of formulas from K + to P + . And σ is defined as follows:

σ(θ) = { q ki if θ = □ k p i ¬q ki if θ = ¬□ k p i σ(ψ) = { σ(θ) if ψ = θ σ(ψ 1 ) ∧ σ(ψ 2 ) if ψ = ψ 1 ∧ ψ 2 σ(φ) = { σ(ψ) if φ = ψ σ(φ 1 ) ∨ σ(φ 2 ) if φ = φ 1 ∨ φ 2
It is easy to see that each formula φ in the normal form in K + can be corresponding to a formula σ(φ) in the normal form in P + . Since each formula φ in K + can be equivalent to a formula in the normal form in K + , each formula φ in K + can be corresponding to a formula in the normal form in P + . For simplicity, we will only consider formulas in the normal form in K + and formulas in the normal form in P + . Then it is easy to prove that σ is a bijective function. And we can also get that for any formula φ of K + , σ(¬φ) = ¬σ(φ).

By induction on the number of formulas in the sequence forming the deduction of φ from K + , we can get that if φ is a theorem of K + then σ(φ) is a theorem of P + . For example, if φ is a theorem of K + and we get it by an application of the N rule from the theorem φ 1 (p 0 , p 1 , ..., p n ), then σ(φ) is also a theorem of the propositional logic. Since we can distribute □ over ∧ and ∨, we get that φ = φ 1 (□p 0 , □p 1 , ..., □p n ). By induction hypothesis we know that σ(φ 1 ) = φ ′ 1 (q k00 , q k11 , ..., q knn )(0 ≤ i ≤ n, k i ≥ 0) is a theorem of P + , when we use q (ki+1)i to substitute for q kii we get a formula φ ′ 1 (q (k0+1)0 , q (k1+1)1 , ..., q (kn+1)n )(0 ≤ i ≤ n, k i ≥ 0) of P + , which is σ(φ) and also a theorem of P + . We know that each axiom of the propositional logic is an axiom of K + , by using the rule MP each theorem of P + we get is also a theorem of K + . So we get the following proposition.

Proposition 5. For any formula φ of K + , φ is a theorem of K + if and only if σ(φ) is a theorem of P + . □ Suppose that A is a set of formulas in K + , and A ′ = {σ(φ) : φ ∈ A} is a set of formulas of P + . Then we have the following propositions. Proposition 6. A is consistent if and only if A ′ is consistent. □ Proposition 7. A is maximally consistent if and only if A ′ is maximally consistent. □ For any model M = ⟨W, R, I⟩ of K + and any possible world w ∈ W , there is an assignment v w of P + such that for any pseudo-atomic formula

□ k p i , M, w |= □ k p i if and only if v w |= q ki .
Then we have the following proposition.

Proposition 8. For any formula φ of K + , M, w |= φ if and only if v w |= σ(φ).

Proof. Suppose that φ is in the normal form, and

φ = φ 1 ∨ • • • ∨ φ n = (ψ 11 ∧ • • • ∧ ψ 1m1 ) ∨ • • • ∨ (ψ n1 ∧ • • • ∧ ψ nmn ),
where

ψ ij =∼ lij □ kij p ij , 1 ≤ i ≤ n, 1 ≤ j ≤ m i and k ij ≥ 0. Then σ(φ) = σ(φ 1 ) ∨ • • • ∨ σ(φ n ) = (σ(ψ 11 ) ∧ • • • ∧ σ(ψ 1m1 )) ∨ • • • ∨ (σ(ψ n1 ) ∧ • • • ∧ σ(ψ nmn )).
Obviously Proof. The proof is by contraposition. □ Let C be the class of frames in which each world can only see one world, itself or another. We should prove that K + is sound and complete with respect to C. And theorems of K + are also theorems of P + , and vice versa; valid formulas of K + are also valid formulas of P + , and vice versa. So we can easily get the following theorems from the soundness and completeness of P + . Theorem 4.(Soundness of K + ) For any formula φ of K + , if ⊢ φ then |= C φ. Theorem 5.(Completeness of K + ) For any formula φ of K + , if |= C φ then ⊢ φ.

(i ≥ 0) of K + , v 0 (p i ) = 1 if and only if v(q 0i ) = 1; v 1 (p i ) = 1 if and only if v(q 1i ) = 1; • • • v k (p i ) = 1 if and only if v(q ki ) = 1; • • • Let M = ⟨W, R, I⟩, where R = {(v n , v n+1 ) : n ≥ 0}; for any propositional variable p i (i ≥ 0) and any k ≥ 0, v k ∈ I(p i ) if and only if v k (p i ) = 1.

Conclusions

In this paper we construct a new propositional modal system K + , in which maximally consistent sets have a property holding in the propositional logic: a maximally consistent set is uniquely determined by a set of pseudo-atomcomplete formulas. Each formula in such a logic is equivalent to a formula in the disjunctive normal form, where each disjunct is the conjunction of pseudoatomic formula or the negation of pseudo-atomic formula. The accessibility relation in the canonical model of K + can be simply given by eliminating one □ from each pseudo-atomic formula or its negation in a possible world. We also build correspondences of formulas, theorems and valid formulas between K + and the propositional logic P + . So, the soundness theorem and the completeness theorem of K + follow directly from those of P + .

Theorem 1 .

 1 (Soundness theorem of K) For any formula φ, if ⊢ φ then |= φ. Theorem 2. (Completeness theorem of K) For any formula φ, if |= φ then ⊢ φ.

9 .

 9 Then we have the following proposition. Proposition For any formula φ of K + , M, v 0 |= φ if and only if v |= σ(φ). □ It is easy to get the following proposition. Proposition 10. For any formula φ of K + , |= φ if and only if |= σ(φ).

  is true at every world in M . A formula φ is valid on a frame F, denoted by F |= φ, if φ is valid in every model based on F . Given a class of frames C, a formula φ is valid with respect to C, if φ is valid on every frame in C.

Definition 4 A formula φ is valid in a model M, denoted by M |= φ, if φ

  , M, w |= ψ ij if and only if v w |= σ(ψ ij ). v w |= σ(φ) if and only if there is an i such that v w |= σ(φ i ); if and only if there is an i and for any j, v w |= σ(ψ ij ); if and only if there is an i and for any j, M, w |= ψ ij ; if and only if there is an i such that M, w |= φ i ; if and only if M, w |= φ. □ For any assignment v of P + we can construct a model of K + . Let W = {v 0 , v 1 , v 2 , ...} be a set of assignments such that for any propositional variable p i

A normal modal system is a consistent extension of the system K which retains the rules MP and N. And the definition can be found in[START_REF] Hazen | Actuality in Propositional Modal Logic[END_REF][START_REF] Hughes | A New introduction to Modal Logic[END_REF].

The logical connectives ∧, ∨ and ↔ can be defined by ¬ and →. For example, φ ∧ ψ = df ¬(φ → ¬ψ), where= df is read as "be defined as".

Acknowledgements

This work is supported by National Natural Science Foundation of China under grant No. 60573064, 91224006, 61203284, and 61173063.


Shaobo Deng

Meiying Sun

Cungen Cao

Yuefei Sui

A Sound And Complete Axiomatic System For Modality ϕ ≡ 1 ϕ ∧ 2 ϕ

Keywords: Modal logic, Axiomatic system S5, Soundness, Completeness, Canonical model

An axiomatic system is presented in this paper, which has a modal operator such that ϕ ≡ 1 ϕ ∧ 2 ϕ, where 1 and 2 are the modal operators of the language for the axiom system S5. The axiomatic system for is proved to be sound and complete.

Introduction

The modal logic has many axiomatic systems, such as K, T, D, B, S4 and S5 ( [START_REF] Sui | A new introduction to modal logic[END_REF]). The axiom system S5 is characterized by all equivalence frames( [START_REF] Sui | A new introduction to modal logic[END_REF]). The approximation spaces for Rough sets can be used as the possible-world semantics for S5. Let an approximate space (U, R) be an equivalence frame W, R for S5, i.e., U = W . Then for any formula ϕ, if the interpretation of ϕ corresponds to a subset X of U, then the lower and upper approximations of X correspond to the interpretations of ϕ and ♦ϕ, respectively, and the equivalence relation R corresponds to the accessibility relation for ( [START_REF] Young | First-order rough logic i: approximate reasoning via rough sets[END_REF]).

Given two approximation spaces (U, R 1 ) and (U, R 2 ), R 1 ∪ R 2 may not be an equivalence relation. Given two modal operators 1 and 2 , let R 1 and R 2 be the accessibility relations for 1 and 2 , respectively. Let be a modal operator such that R 1 ∪R 2 is the accessibility relation for , that is, M, w ϕ iff for any w ∈ W if (w, w ) ∈ R 1 ∪ R 2 then M, w ϕ, which implies and is implied by that for any w ∈ W if (w, w ) ∈ R 1 then M, w ϕ and for any w ∈ W if (w, w ) ∈ R 2 then M, w ϕ, i.e., M, w 1 ϕ and M, w 2 ϕ if and only if M, w ϕ.

1 Let be a modal operator such that for any possible world w, M, w ϕ iff M, w 1 ϕ and M, w 2 ϕ, i.e., for any formula ϕ, ϕ ≡ 1 ϕ ∧ 2 ϕ. In this paper, we consider the modal operator ϕ ≡ 1 ϕ ∧ 2 ϕ. We shall give the language, the syntax and the semantics for the modal logic with modal operator ϕ ≡ 1 ϕ ∧ 2 ϕ. The axiomatic system for will be given and proved to be sound and complete.

The main contribution of this paper is that a propositional modal logic with a modal operator ϕ ≡ 1 ϕ ∧ 2 ϕ. The axiomatic system for is sound, and complete with respect to the class of all reflective and symmetric frames, where the accessibility relation R for is equivalent to R 1 ∪ R 2 , where R i is the equivalence relation for i and i = 1, 2.

If R 1 = R 2 , then the axiomatic system for turns out to be S5. This paper is organized as follows: the propositional modal logic with modal operator ϕ ≡ 1 ϕ ∧ 2 ϕ is described in section 2, including the language, the syntax and the semantics for the logic. Then we shall give the axiomatic system for and prove the soundness theorem and the completeness theorem. Section 3 summaries results of the paper and discusses some possible extension of the logic.

The propositional modal logic with modal operator

ϕ ≡ 1 ϕ ∧ 2 ϕ
In this section, we shall give the language, the syntax and the semantics for the propositional modal logic with the modality ϕ ≡ 1 ϕ ∧ 2 ϕ. The axiomatic system for is denoted by S51 ∧ S52 , then we prove that S51 ∧ S52 is sound and complete.

The language, syntax and semantics for the logic

The language for S51 ∧ S52 contains the following symbols: • propositional variables: p 0 , p 1 , ...;

• logical connectives: ¬, →; • modalities: , 1 , 2 ;

• auxiliary symbols: (,). Formulas:

ϕ := p|ϕ 1 → ϕ 2 |¬ϕ 1 | ϕ 1 ; ϕ := 1 ϕ 1 ∧ 2 ϕ 1 .
Other operators:

(α ∨ β) = def (¬α → β); (α ∧ β) = def ¬(α → ¬β); (α ↔ β) = def ((α → β) ∧ (β → α)); (♦α) = def (¬ ¬α). Definition 2.1. A frame F is a triple W, R 1 , R 2 ,
where W is a non-empty set of possible worlds, and R 1 ⊆ W 2 and R 2 ⊆ W 2 are the equivalence relations defined over the members of W and the accessibility relations for 1 and 2 , respectively.

Definition 2.2. A model M is a quadruple W, R 1 , R 2 , I , where W, R 1 , R 2 is a frame and I is an interpretation such that for any propositional variable p I(p) ⊆ W and for any w ∈ I(p) p is true in w.

A satisfaction relation , between any formula ϕ and any possible world w, is defined as follows:

Definition 2.3. Given any model M , any possible world w ∈ W and any formula ϕ, M, w ϕ iff

           w ∈ I(p) if ϕ = p M, w ϕ 1 if ϕ = ¬ϕ 1 M, w ϕ 1 ⇒ M, w |= ϕ 2 if ϕ = ϕ 1 → ϕ 2 for all w ∈ W if wR 1 w then M, w ϕ 1 , and for all w ∈ W if wR 2 w then M, w ϕ 1 if ϕ = ϕ 1
By the definition of the satisfaction relation, we can give the following definition:

Definition 2.4. A formula ϕ is valid in a model M , dented by M ϕ, iff for any w ∈ W M, w ϕ; a formula ϕ is valid in a frame F , denoted by F ϕ, iff for any model M based on F M ϕ; let C be a class of frames. A formula ϕ is valid in C iff for any

F ∈ C F ϕ; Σ C ϕ iff for any frame F ∈ C if F Σ then F ϕ. If Σ = ∅ then C ϕ.
Now we give the following axiom schemas and inference rules for S51 ∧ S52 :

• Axiom schemes:

L1 ϕ → (ψ → ϕ) L2 (ϕ → (ψ → µ)) → ((ϕ → ψ) → (ϕ → µ)) L3 (¬ψ → ¬ϕ) → (ϕ → ψ) L4 (ϕ → ψ) → ( ϕ → ψ) L5 ϕ → ϕ L6 ϕ → ♦ϕ L7 1 1 ϕ → 1 1 ϕ L7 2 2 ϕ → 2 2 ϕ
• Inference rules:

(M P ) ϕ, ϕ → ψ ψ (N ) ϕ ϕ
Definition 2.5. A formula ϕ is provable from Γ, denoted by Γ ϕ, if there is a sequence of formulas ϕ 1 , ..., ϕ n such that ϕ = ϕ n , and for each 1 ≤ i ≤ n, either ϕ i is an axiom or a formula in Γ, or is deduced from the previous formulas via one of the deduction rules.

The Soundness Theorem

This section is to prove the soundness theorem by induction on the length of proofs. Before giving the proof, we give the following lemmas:

Lemma2.1. Each axiom schema is valid. P roof . As for the axiom schema L1, L2, L3, we do not check their validity and two references are [START_REF] Sui | A new introduction to modal logic[END_REF] and [START_REF] Ebbinghaus | Mathematical logic[END_REF].

(L5) By the definition 2.3, it is easy to prove it. (L6) By the definition 2.3, it is easy to prove it. (L7 1 ) Since the accessibility relation R 1 for 1 is an equivalence relation, it follows that

1 ϕ → 1 1 ϕ is valid. (L7 2 ) Since the accessibility relation R 2 for 2 is an equivalence relation, it follows that 2 ϕ → 2 2 ϕ is valid.
Lemma2.2. The deduction rules preserve validity. P roof. We prove that (N ) preserves the validity. Since for any model W, R 1 , R 2 , I based on any frame W, R 1 , R 2 and any w ∈ W , M, w |= ϕ.

Let w 1 be any possible world. Since R 1 and R 2 are the equivalence relations on W , we can obtain that for any w 1 ∈ W if w 1 R 1 w 1 then M, w 1 |= ϕ, and for any w 1 ∈ W if w 1 R 2 w 1 then M, w 1 ϕ. It follows that M, w 1 ϕ. Since for any w 1 ∈ W M, w 1 ϕ, it follows that ϕ.

Theorem 2.1(The Soundness Theorem). For any set of formulas Γ and formula ϕ, if Γ ϕ, then Γ ϕ. P roof. For any set of formulas Γ and formula ϕ, since Γ ϕ, ϕ is the last member of a sequence which is a deduction from Γ. So we can use induction on the number of the sequence to prove this theorem as follows:

For the base step, the sequence has only one formula, namely ϕ. Then ϕ must be an axiom of S51 ∧ S52 or a member of Γ, and then Γ |= ϕ. Now suppose that the sequence contains n formulas,where n>1,and suppose as induction hypothesis that Γ |= α follows from Γ α ,which sequence is fewer than n members. There are the following cases:

Case a. ϕ is an axiom of S51 ∧ S52 or a member of Γ, then we have Γ |= ϕ Case b. ϕ is obtained by modus ponens rule from a formula ψ and a formula ψ → ϕ in the sequence. So by induction hypothesis, it obtains that Γ |= ψ and Γ |= ψ → ϕ, then it follows that Γ |= ϕ.

Case c. ϕ = ψ is obtained by the inference rule N from ψ. So by induction hypothesis, it follows that Γ |= ψ. Since if for any model W, R 1 , R 2 , I based on any frame W, R 1 , R 2 and any w ∈ W M, w ψ then for any model W, R 1 , R 2 , I based on any frame W, R 1 , R 2 and any w ∈ W M, w ψ, it follows that Γ |= ψ.

The completeness theorem

The completeness theorem is to be proved in this section. The proof method of the complete theorem is similar to the classical canonical model method ( [START_REF] Sui | A new introduction to modal logic[END_REF]). We shall construct two relations on W and prove whether the two relations are equivalence relations or not. And one relation corresponds to the accessibility relation for 1 , while the other corresponds to the accessibility relation for 2 .

Definition 2.6. Γ is consistent iff there is no finite set {ϕ 1 ,...,ϕ n } ⊆ Γ such that:

¬(ϕ 1 ∧ ... ∧ ϕ n ).
By definition 2.6, we can prove that Γ is inconsistent iff there is some formula ϕ such that Γ ϕ and Γ ¬ϕ.

Lemma 2.3. Suppose that Σ is a consistent set of formulas. Then there is a maximal consistent set of formulas Σ * such that Σ ⊆ Σ * .

In constructing a model in which the possible worlds are maximal consistent sets of formulas we will have to specify when one world is accessible from another(that model, in this paper, is also called canonical model). Thereby, the accessibility relation R 1 and R 2 , in the canonical model, is defined as follows:

Definition 2.7. For any two distinct maximal consistent sets Σ * 1 ,Σ * 2 , we define two binary relations R 1 and R 2 on W as follows:

(1) We shall say that Σ * 1 R 1 Σ * 2 iff Σ * 1 and Σ * 2 satisfy the following condition: For any formula

ϕ if ϕ ∈ Σ * 1 then ϕ ∈ Σ * 2 (written:S -(Σ * 1 ) = {ϕ : ϕ ∈ Σ * 1 }).
(2) We shall say that Σ * 1 R 2 Σ * 2 iff Σ * 1 and Σ * 2 satisfy the following condition: For any formula

ϕ if ϕ ∈ Σ * 1 then ϕ ∈ Σ * 2 (written: S(Σ * 1 ) = { ϕ : ϕ ∈ Σ * 1 }). Lemma 2.4. Let Γ * = {Σ * 0 , Σ * 1 , .
..} be the set of all maximal consistent sets. If for any i, j ∈ N we define Σ

* i R 1 Σ * j iff S -(Σ * i ) ⊆ Σ * j , and Σ * i R 2 Σ * j iff S(Σ * i ) ⊆ Σ * j
, then both the relation R 1 and R 2 are equivalence relations on W . P roof. (1) In order to prove that R 1 is an equivalence relation, we shall prove the following three conditions:

1) For any i ∈ N , if Σ * i ∈ Γ * then Σ * i R 1 Σ * i . 2) For any Σ * i , Σ * j ∈ Γ * , if Σ * i R 1 Σ * j then Σ * j R 1 Σ * i . 3) For any Σ * 1 , Σ * 2 , Σ * 3 ∈ Γ * , if Σ * 1 R 1 Σ * 2 and Σ * 2 R 1 Σ * 3 then Σ * 1 R 1 Σ * 3 . 1). For any i ∈ N , we shall prove S -(Σ * i ) ⊆ Σ * i . For any formula ϕ, if ϕ ∈ Σ * i then ϕ ∈ S -(Σ * i ). Since ϕ → ϕ(L5) and ϕ ∈ Σ * i , ϕ ∈ Σ * i . It follows that S -(Σ * i ) ⊆ Σ * i .
2). We shall prove that if

S -(Σ * i ) ⊆ Σ * j then S -(Σ * j ) ⊆ Σ * i
, that is to say, we shall prove that for any formula

β if β ∈ Σ * j then β ∈ Σ * i . Suppose β / ∈ Σ * i . ¬β ∈ Σ * i . By L6 and ¬β ∈ Σ * i it follows that ♦¬β ∈ Σ * i . Since S -(Σ * i ) ⊆ Σ * j , it follows that ♦¬β ∈ Σ * j , that is, ¬ β ∈ Σ * j . Since ¬ β ∈ Σ * j and β ∈ Σ * j , Σ * j is not consistent
, which is a contradiction to the hypothesis of this lemma.

3). We need to prove that if

S -(Σ * 1 ) ⊆ Σ * 2 and S -(Σ * 2 ) ⊆ Σ * 3 then S -(Σ * 1 ) ⊆ Σ * 3 , that is to say, for any formula β, if β ∈ Σ * 1 then β ∈ Σ * 3 .
We can prove it by L5 and L7 1 .

What we need to explain is that R 1 is the accessibility relation for 1 and in this case for any formula ϕ ϕ ≡ 1 ϕ. Thereby, we can use the axiom schema L7 1 .

(2) Now, we prove that the relation R 2 is an equivalence relation. the following conditions shall be proved:

1) For any i ∈ N , if Σ * i ∈ Γ * then Σ * i R 2 Σ * i . 2) For any Σ * i , Σ * j ∈ Γ * , if Σ * i R 2 Σ * j then Σ * j R 2 Σ * i . 3) For any Σ * 1 , Σ * 2 , Σ * 3 ∈ Γ * , if Σ * 1 R 2 Σ * 2 and Σ * 2 R 2 Σ * 3 then Σ * 1 R 2 Σ * 3 .
It is easy to prove the item 1)-3). We omit the proof procedures. Then

(ϕ 1 ∧ ... ∧ ϕ n ) → ¬ψ iff (ϕ 1 ∧ ... ∧ ϕ n ) → ψ iff (ϕ 1 ∧ ... ∧ ϕ n ) → ψ iff ( ϕ 1 ∧ ... ∧ ϕ n ) → ψ iff ¬( ϕ 1 ∧ ... ∧ ϕ n ∧ ¬ ψ)
Thereby, { ϕ 1 , ..., ϕ n } ∪ {¬ ψ} is not consistent. By the definition of S -(Γ) it follows that { ϕ 1 , ..., ϕ n } ∪ {¬ ψ} is a subset of Γ. Thereby, Γ is not consistent, which is a contradiction to the hypothesis of this lemma.

(2) We shall prove that S(Γ) ∪ {¬ψ} is consistent as follows. Suppose that S(Γ) ∪ {¬ψ} is not consistent. Then there exists some finite subset

{ ϕ 1 , ..., ϕ n } ∪ {¬ψ} of S(Γ) ∪ {¬ψ} such that ¬( ϕ 1 ∧ ... ∧ ϕ n ∧ ¬ψ). Then ( ϕ 1 ∧ ... ∧ ϕ n ) → ¬ψ iff ( ϕ 1 ∧ ... ∧ ϕ n ) → ψ iff ( ϕ 1 ∧ ... ∧ ϕ n ) → ψ iff ( ϕ 1 ∧ ... ∧ ϕ n ) → ψ iff ¬( ϕ 1 ∧ ... ∧ ϕ n ∧ ¬ ψ)
Thereby, { ϕ 1 , ..., ϕ n } ∪ {¬ ψ} is not consistent. For any ϕ i , by L7 2 ( ϕ ≡ 2 ϕ) it follows that ϕ ∈ Γ, where i=1,...,n. Thereby, { ϕ 1 , ..., ϕ n } ∪ {¬ ψ} is a subset of Γ. Then Γ is not consistent, which is a contradiction to the hypothesis of this lemma.

What we need to explain is that R 2 is the accessibility relation for 2 and in this case for any formula ϕ ϕ ≡ 2 ϕ. Thereby, we can use the axiom schema L7 2 .

The canonical model for S51 ∧ S52 , M , is like any other model, a quadruple W, R 1 , R 2 , I . W is the set of all sets of maximal consistent sets of formulas. I.e. w ∈ W iff w is a maximal consistent set of formulas. If w and w are both in W , then wR 1 w iff S -(w) ⊆ w . And if w and w are both in W , then wR 2 w iff S(w) ⊆ w . For any propositional variable p I(p) ⊆ W , and for any w ∈ I(p) p is true in w iff p ∈ w. For any other formula this has to be proved as follows:

Lemma 2.6. Let M = W, R 1 , R 2 , I be the canonical model for S51 ∧ S52 . Then for any formula ϕ and any world w, M, w ϕ iff ϕ ∈ w. P roof. We prove the lemma by induction on the structure of formulas. (1) For any w ∈ W , if wR 1 w then α ∈ w . α ∈ w iff M, w α by induction hypothesis. Then M, w α because for any w if wR 1 w and M, w α.

(2) For any w ∈ W , if wR 2 w then α ∈ w . Since α ∈ w and α → α, α ∈ w . α ∈ w iff M, w α by induction hypothesis. Then M, w α because for any w if wR 2 w and M, w α.

Subcase d.2. ¬ α ∈ w: By the lemma 2.5 , both S -(w) ∪ {¬α} and S(w)∪{¬α} are consistent. By the lemma 2.3, we can enlarge S -(w)∪{¬α} and S(w) ∪ {¬α} into maximal consistent sets of formulas w 1 and w 2 , respectively. Thereby, there exist w 1 , w 2 such that S -(w) ⊆ w 1 and S(w) ⊆ w 2 .

Conclusion

In this paper, we present an axiomatic system for a modality ϕ ≡ 1 ϕ ∧ 2 ϕ, and prove that the axiomatic system for is sound and complete. The axiomatic system for is different from S5. What we need to point out is that L7 1 and L7 2 are not the axiom schemas for , which is needed when proving the completeness theorem. An interesting problem is to give a sound and complete axiomatic system for the modality corresponding to the accessibility relation R = R 1 ∩ R 2 , where the equivalence relation R i is the accessibility relation for i , i = 1, 2.

Lemma 2 . 5 .

 25 Let Γ be any consistent set of formulas containing ¬ ψ, thenS -(Γ) ∪ {¬ψ} is consistent and S(Γ) ∪ {¬ψ} is consistent, where S -(Γ) = {ϕ : ϕ ∈ Γ } and S(Γ) = { ϕ : ϕ ∈ Γ }. P roof. (1)We shall prove that S -(Γ) ∪ {¬ψ} is consistent as follows: Suppose that S -(Γ) ∪ {¬ψ} is not consistent. Then there exists some finite subset {ϕ 1 , ..., ϕ n } ∪ {¬ψ} of S -(Γ) ∪ {¬ψ} such that ¬(ϕ 1 ∧ ... ∧ ϕ n ∧ ¬ψ).

  Case a. ϕ := p: By definition, this lemma holds. Case b. ϕ := ¬α: M, w ¬α iff M, w α iff α / ∈ w iff ¬α ∈ w Case c. ϕ := α → β: α → β / ∈ w iff ¬(α → β) ∈ w iff α ∈ w and ¬β ∈ w iff M, w α and M, w β iff M, w α → β Case d. ϕ := α: (⇐) Subcase d.1. α ∈ w: By the definition of R 1 , R 2 , we have the following two cases:

Acknowledgement:

This work is supported by National Natural Science Foundation of China under grant No. 91224006,61035004,61173063,61203284,61363047, and the ministry of science and technology project under grant No. 201303107.

Since S -(w) ⊆ w 1 and S(w) ⊆ w 2 , by the definition of R 1 and R 2 , it follows that wR 1 w 1 and wR 2 w 2 . For ¬α ∈ w 1 and ¬α ∈ w 2 , it follows that M, w 1 |= ¬α and M, w 2 |= ¬α by induction hypothesis. So there exist w 1 , w 2 such that wR 1 w 1 and wR 2 w 2 and M, w (2) For any w ∈ W , if wR 2 w then M, w α. From (1), we have:

(3) For any w ∈ W , if wR 1 w then α ∈ w by induction hypothesis. From (2),we have: (4) For any w ∈ W , if wR 2 w then α ∈ w by induction hypothesis. Assume ¬ α ∈ w. Since w is a maximal consistent set of formulas, it follows that there exists w 1 , w 2 ∈ W such that wR 1 w 1 and wR 2 w 2 and ¬α ∈ w 1 and¬α ∈ w 2 by the lemma 2.5. So ¬α ∈ w 1 is a contradiction to (3), and ¬α ∈ w 1 and ¬α ∈ w 2 is also a contradiction to (4). Thereby, α ∈ w for w is a maximal consistent set of formulas.

Subcase d.4. M, w α: By the definition 2.3, we have: (1) There exists w 1 ∈ W such that wR 1 w 1 and M, w 1 α; or (2) There exists w 2 ∈ W such that wR 2 w 2 and M, w 2 α. From (1), by induction hypothesis, ¬α ∈ w 1 ; and from (2), ¬α ∈ w 2 . Suppose α ∈ w, by the definition of R 1 and R 2 , it follows that:

(3) For any w ∈ W if wR 1 w then α ∈ w ; and (4) For any w ∈ W if wR 2 w then α ∈ w . From (4) and L5, we have:

(5) For any w ∈ W if wR 2 w then α ∈ w . It follows that ( 3) is in contradiction with wR 1 w 1 and ¬α ∈ w 1 . And (5) also is in contradiction with wR 2 w 2 and α ∈ w 2 . Thereby, ¬ α ∈ w for that w is a maximal consistent set of formulas.

Theorem 2.2(The Completeness Theorem): For any set of formulas Γ and formula ϕ, if Γ ϕ, then Γ ϕ. P roof. Suppose Γ ϕ, so Γ ∪ {¬ϕ} is consistent. Then there is a maximal consistent set of formulas w such that Γ ∪ {¬ϕ} ⊆ w by the lemma 2.3.

Let M = W, R 1 , R 2 , I be a canonical model, where W is the set of all sets of maximal consistent sets of formulas. I.e. w ∈ W iff w is a maximal consistent set of formulas. If w and w are both in W , then wR 1 w iff S -(w) ⊆ w . And if w and w are both in W , then wR 2 w iff S(w) ⊆ w . By the lemma 2.4 it follows that R 1 and R 2 are the equivalence relations on W .

For any formula α ∈ Γ ∪ {¬ϕ}, α ∈ w. By the theorem 2.6, M, w α. So M, w Σ and v ¬ϕ, which is a contradiction to Σ ϕ.

So for any set of formulas Γ and formula ϕ, if Γ ϕ, then Γ ϕ.