Fengying Li

Tianlong Gu

Yaoguang Wang
email: wangyguang@qq.com

Liang Chang
email: changl@guet.edu.cn

Verification of Branch-Time Property Based on Dynamic Description Logic

Keywords: dynamic description logic, verification, temporal description logic, action theory

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

Introduction

Model checking [START_REF] Clarke | Model Checking[END_REF] is a formal verification method widely used in recent years, which is based on state transition system. However, the traditional model checking has some limitations. Firstly, it does not consider what makes state change. Secondly, it just uses temporal logic based on proposition logic to specify the property, which limits the scope of specifying properties. So, researchers begin to combine the action theory [START_REF] Reiter | Knowledge in action: logical foundations for describingand implementing dynamical systems[END_REF] to verification problem and consider the action make the state change.

Verification problem with action theory has been addressed by some researchers. In [START_REF] Giacomo | Non-terminating processes in the situation calculus[END_REF], the author puts forward a method of verifying temporal properties based on infinite sequence of Golog program and checks whether the execution of program sequence can satisfy temporal properties. In [START_REF] Claβen | A Logic for non-terminating Golog programs[END_REF], the author aims at the fully automated verification of non-terminating Golog programs and uses an extension of situation calculus by constructing the first-order temporal logic CTL * . However, the problems both of them consider are all undecidable. For this reason, [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF] begins to use the action theory based on decidable description logic to check whether there is an execution sequence of action can satisfy the temporal property specified in linear temporal description logic DL-LTL [START_REF] Baader | LTL over description logic axioms[END_REF].

However, [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF] just considers the atom action and only the linear-time properties can be verified. Based on this limitation, we consider the action in dynamic description logic that contains action constructors like sequence, choice, iterator or test action. For the reason that the action in DDL contains choice action constructor, it becomes possible that the action can make the state change in branch structure. The verification problem becomes whether there is a model generated by an execution complex action that meets temporal formula specified in branch temporal description logic DL-CTL. Instead of considering the actual execution sequences of actions, we consider execution complex action sequences accepted by a given non-deterministic finite automaton NFA. If a NFA is an abstraction of the action, i.e. all possible execution sequences of the action are accepted by NFA, then any property that holds in all the actions accepted by NFA is also a property that is satisfied by any execution of the actions. Therefore, we not only add the action in dynamic description logic to verification problem, but also can verify the branch-time properties.

Preliminaries

Temporal Description Logic DL-CTL

Description logics [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF][START_REF] Baader | LTL over description logic axioms[END_REF][START_REF] Baader | Integrating description logics and action formalisms: First results[END_REF] are a well-known family of formalisms to represent the knowledge, which offers the considerable expressive power going far beyond the propositional logic and the reasoning is still decidable. DL-CTL is the temporal extension to description logics, which extends the propositional branch-time logic (CTL) by allowing for the use of axioms of the basic description logic in place of propositional letters. The properties in this paper will be expressed in DL-CTL.

The concepts in DL-CTL is similar with DL, which are inductively defined a set N C of concept name, a set N R of role name, and a set N I of individual name. The concept construction is the same as those do in DL and the formula is constructed with the temporal operators in CTL. At the same time, the propositional letters in CTL are replaced by ABox assertions of description logic. Definition 1. DL-CTL formula is defined as follows: ϕ, ψ:

:= C⊑D|C(p)|R(p, q)|ϕ| ϕ ψ|EX ϕ | AF ϕ |E(ϕUψ)
where p, qN I , RN R , C,D are concept name. We can also introduce the formula such as false, true, ϕψ, ϕψ, AX ϕ, EF ϕ, EG ϕ, AG ϕ, A(ϕUψ), E(ϕRψ), A(ϕRψ).

The semantic of DL-CTL is similar with CTL and it is based on the structure, in which their states are organized by branch structure. However, the different from CTL is that the state in DL-CTL is not mapped to a set of propositional letters but mapped to DL interpretations. Thus, the state change in state transition system can be viewed as an interpretation change in DL-CTL. Definition 2. DL-CTL structure is a tetrad M = (S, T, ∆, I):

(1) S is a set of all states;

(2) T S S is binary relation of state which means the transition between two states;

(3) ∆ is the interpretation domain; (4) For every state s  S, the function I gives s a DL interpretation I(s) = (Δ,  I(s) ) and the interpretation function  I(s) must meet the following conditions:

(i) For every concept C i  N C, there is C i I(s)  Δ; (ii) For every role name R i  N R , there is R i I(s)  Δ×Δ; (iii) For every individual name p i  N I there is p i I(s)  Δ, and for every state s '  S there is p i I(s) = p i I(s') .

Definition 3. A DL-CTL structure is M=(S, T, , I), the semantic of concept and formula in DL-CTL are inductively defined as follows.

Firstly, for every states sS, a concept C is interpreted C I(s) , which is a subset of Δ.

(1) (C) I(s) :=Δ\C I(s) ;

(2) (C⊔D) I(s) := C I(s) D I(s) ; (3) (R.C) I(s) :={x |for every y  Δ: if(x, y)  R I(s) ,then y  C I(s) }. Secondly, for every states s S, M, s⊨ ϕ means ϕ holds at state s of the structure M.

(4) (M, s) ⊨ C⊑D iff C I(s)  D I(s) ; (5) (M, s) ⊨ C(p) iff p I(s)  C I(s) ; (6) (M, s) ⊨ R(p, q) iff (p I(s) , q I(s) )  R I(s) ; (7) (M, s) ⊨ ϕ iff (M, s) ⊭ ϕ; (8) (M, s) ⊨ ϕ ψ iff (M, s) ⊨ ϕ and (M, s) ⊨ ψ; (9) (M, s) ⊨ EX ϕ iff
there is a state s' and (s, s') T and (M, s') ⊨ϕ; (10) (M, s) ⊨ AF ϕ iff for every path starting with s, there is always a state s' so that sT*s' and (M, s') ⊨ ϕ;

(11) (M, s) ⊨ E(ϕUψ) iff there exists a path starting with s, and there exists an integer k 0 so that (M, s+k) ⊨ ψ and for every 0i<k, (M, s+i) ⊨ ϕ.

In this paper, we consider that the state transition is caused by the application of action. For the reason that every state in DL-CTL structure is mapped to a DL interpretation, we can say that the change of the interpretation of one state to the next is also caused by action.

Dynamic Description Logic DDL

The action theory based on description logic is inherited the advantage of the action theory and the description logic, which not only has the more expressive power but also makes the reasoning tasks decidable. Dynamic description logic (DDL) is a kind of action theory based on description logic, which is proposed by Chang. L et al [START_REF] Chang | A family of dynamic description logics for representing and reasoning about actions[END_REF], who has introduced complex action to the action theory based on description logic.

In this paper, we consider the action theory based on dynamic description logic and the basic definitions of action will be given below. Definition 4. Let T is an acyclic TBox. An action for T is generated below.

π, π =α|φ?|π π |π,π |π * where α is an atom action and φ is an assertion. φ?, π π , π,π , π* are respectively called test action, choice action, sequential action and iterated action.

The complex action is composed by these actions sequence. For example, (φ?), a b, (c, d)* is the complex action and a, b, c, d are respectively the atom action and φ is an assertion.

An atom action is a triple (pre, occ, post), and the detail description of atom action can be found in [START_REF] Baader | Integrating description logics and action formalisms: First results[END_REF]. In this paper, we just consider the action without occ for convenience.

We say that α is executable in an interpretation I if I is a model of pre. If the execution of action can change the interpretation I to I , we can say that α makes I⇒I .

In the existing researches, action is considered as the cause of the state transition, which also means that action is the binary relation between states. For the reason that the action in dynamic description logic contains choice constructor with which the action can make the state change in branch-time state transition system, it becomes possible to verify the branch-time property based on dynamic description logic. Next, some necessary definitions corresponding to this case will be given below. Definition 5. For every complex action π, let be the set of the atom action or test action in π. Every element in can be view as a word and let L(π) be the minimal set of string that defined by the following rules:

(1) If π is an atom action or test action then, L (π) = π;

(2) L (π π ) =L (π) L(π );

(3) L (π, π ) = {l 1 l 2 |l 1 π and l 2 π }; (4) L(π * )=L(π 0 ) L(π 1 ) L(π 2 )…,where L(π 0 ) is an empty string and for every i 1,there is L(π i )=L(π i-1 ,π).

So, each string in L(π) corresponds one of the action execution sequence of π. Definition 6. For a complex action π and one of its action execution sequence l i , where l i L(π), we use |l i | to denote the length of action execution sequence, l i (j) to denote the j-th atom or test action in i-th action execution sequence.

For example, for a complex action π=a,b,c,d, L(π)={l 1 }.That is to say, l 1 is the only action execution sequence and l 1 =abcd; For another complex actionπ=(a,b) (c,d,e), L(π)={l 1 ,l 2 }, l 1 and l 2 are the two action execution sequences of π and l 1 =ab, l 2 =cde, l 1 (1)=a, 2 (2)=d. Definition 7. Let T be an acyclic TBox, A an ABox, and π a complex action for T. For the interpretation of a state s 0, there is I(s 0 )⊨A, then for an execution action sequence l i of π and a path starting from s 0 , if is executable in I(s j ) and it makes I(s j )⟹ I(s j+1 ), then, we call this path is a path generated by l i . A DL-CTL structure generated by π is a tree structure where s 0 is the root and it contains all paths generated by each corresponding execution action sequence of π.

In this paper, for verification problem based on action, we consider whether there is a model M generated by an execution complex action that meets the property specified in DL-CTL. According to automaton theory, every action π can be constructed to a non-deterministic finite automaton (NFA). Instead of considering the actual execution sequences of actions, we abstract the complex action to non-deterministic finite state automaton (NFA) and just consider the action accepted by a NFA. Definition 8. A= (Q, , δ, q 0 , F) is a non-deterministic finite automaton and Q is a set of state, is the alphabet, δ: Q 2 Q is a transition function, q 0 Q is initial state and F Q is the final state set. We can say that A is a NFA for and is the set of the atom action or test action. The language accepted by A is L (A), which also can be treated as L (π).

According to the theory of formalism, the verification problem can be considered as satisfiability problem, which asks whether there is a complex action π accepted by NFA that satisfies the property specified in DL-CTL. The formal definition of this problem is shown in Definition 9 and an actual example will be given to this problem in the following section. Definition 9. Let T be an acyclic TBox, A an ABox, and a finite set of action for T. B is a NFA for the alphabet , and φ a DL-CTL formula. φ is satisfiable w.r.t T, A, and B if there is a DL-CTL structure M generated by π from A w.r.t T such that M, s 0 ⊨φ.

An example

An example of buying a book will be given to show the problem we have discussed above. Assume the fact is: Jim wants to buy book A and B in bookstore, if the bookstore does not have the two books, it has to order them and then Jim can buy the two books at the same time.

According to the fact, the property can be described like this: though the bookstore does not have the two books, Jim can eventually get them. Obviously, if Jim wants to buy the two books, the bookstores must have the two books; if not, the bookstore must order the two books. If the bookstores just order one of them, Jim still can't buy the two books. Based on these facts, we give a formal definition of this case.

Firstly, we give a basic definition and symbol in this case, where the concept set N C ={student, book, instore}, the role set N R ={bought, has}, the individual name set N I ={Jim,book_a,book_b},The action set:{buyBook_a,buyBook_b,order_a,order_b}.

Based on these definitions, the background knowledge can be described below.

student ≡ person⊓∃has.books

Then, we define the actions given above.

buyBook_a ≡({student (Jim), book (book_a), instore (book_a)}, { instore (book_a), bought (Jim, book_a)}); buyBook_a ≡({student (Jim), book (book_b), instore (book_b)}, { instore(book_b), bought (Jim, book_b)}); order_a ≡({book (book_a), instore (book_a)}, {instore (book_a)}); order_b ≡({book (book_b), instore (book_b)}, {instore (book_b)});

The property described in this example can be specified in following DL-CTL formula φ. bb From the fact we know that if Jim want to buy the two books, the bookstore must have the two books; if not, the bookstore must order them, and Jim can go to buy the book and the get the book. That is to say, as long as the action order_a, order_b, buyBook_a, buyBook_b exists in complex action π, the property will be satisfied.

EF( instore(book_a) instore(book_b) EF(bought(Jim,book_a) bought(Jim,book_b)))

Fig. 1. a non-deterministic finite automaton B buyBook

The NFA B buyBook is depicted in Figure 1. The alphabet of B buyBook is , which consists of the actions defined above. For the convenience of describing the actions, the actions instore (book)?, buyBook_a, buyBook_b, order_a, order_b are abbreviated with In(b)?, ba ,bb ,oa ,ob.

For action π=In(b)?(((oa ob)(oa) * ,(ob),(ba) * ,(bb) * , it is easy to check that one of its action execution sequence In(b)oa,oa(oa…)ob,ba,(bb…) L(B buyBook ) can generate a branch structure that can satisfy the property that Jim eventually get the two books described above.

Verification algorithm based on DDL

In this paper, we consider a restricted situation that action contains cyclic sequence of action, which is similar to the case given in [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF]. We solve this problem defined above by the reduction from the satisfiability problem of DL-CTL formula to the consistency problem introduced in [START_REF] Baader | Integrating description logics and action formalisms: First results[END_REF]. The detail algorithm is given in Algorithm 1 and the detail construction of each step will be given in the following section.

Algorithm 1. Given an ABox A, a TBox T, an action and a formula , whether there is a model M generated by that meets can be decided by the following steps:

Step 1. Construct an acyclic TBox T red , and an ABox A red from A, T, and ;

Step 2. Construct an ABox A pre from ;

Step 3. Using tableau rules to compute an ABox Aϕ from ϕ;

Step 4. Using the reasoning services provided by description logic to decide whether A red A pre Aϕ is consistent w.r.t T red , if A red A pre Aϕ is consistent w.r.t T red , return 'yes', else return 'no'.

3.1

Construction of T red

Firstly, we assume that there are no DL-CTL negation signs in φ, which is similar with the method in [START_REF] Baader | Intergrate Action Formalisms into Linear Temporal Description Logic[END_REF] when dealing with LTL negation signs. It allows DL-CTL signs occur only in front of ABox assertion rather than temporal operator.

Secondly, we refer to the method for solving the projection problem in [START_REF] Baader | Intergrate Action Formalisms into Linear Temporal Description Logic[END_REF] to the finite sequence of atom action to construct T red and A red .

In order to define T red , we define T N , which contains all individual names in the input.

T N = {N≡ {a}, for all a I } (1)
Let Sub be the set of the subconcepts in the input. For every C Sub, if C is not a defined concept name of T, then there is a concept definition of and . Moreover, contains only those concept definitions. The concept definition of can be found in [START_REF] Baader | Intergrate Action Formalisms into Linear Temporal Description Logic[END_REF]. Now, according to the method given in [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF], we are ready to assemble T red :

T red =T N (⋃ ) { ≡ A≡E T, for i m+2n-1} (2)
TBox T N and can ensure that the interpretations of concept and role names remain unchanged by actions on the anonymous objects and the last part of T red is to make sure that T is satisfied no matter how actions change an interpretation. In order to meet the semantic of action, we need to get the pre-definitions of , , A ini ,which can be found in [START_REF] Baader | Intergrate Action Formalisms into Linear Temporal Description Logic[END_REF], and then we can get ABox A red :

Construction of A red and

A red =A ini (⋃ ) ⋃ (3)
In [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF], we know that from every model of A red and T red , we can construct the cruial part of a DL-CTL structure generated by π from A and T. We can also see that any finite sequence I(s 0 )....I(s m+2n-1 ) satisfy the property stated in the above items can be extended to an DL-CTL structure generated by

π=π 1 •••π m (π •••π ) π from A w.

r.t T by setting I(s m+kn+i )=I(s m+n+i ) for all k 2 and

i < n. To enforce the excitability of the execution action sequence l i , which l i (j) is the j-th atom or test action in l i (j), we define ABox A pre , which is similar with the method given in [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF] dealing with the atom actions.

A pre =⋃{ | j , for 0 j m+2n-1} (4)
where pre j is the set of pre-conditions of l i , the excution action sequence of π.

3.3

Construction of Aϕ

In order to ensure that the DL-CTL formula φ is satisfied, we generate additional ABox Aϕ by applying a non-deterministic tableau algorithm. We have time-stamped copied ϕ (i) for every subformula φ of ϕ, which means that ϕ holds at time point i. Different from the method for solving the semantic the temporal operator of LTL given in [START_REF] Baader | Intergrate Action Formalisms into Linear Temporal Description Logic[END_REF], we use the approach given below to solve the problem of DL-CTL with these tableau rules. The tableau algorithm starts with an initial set ={ϕ (0) }, and then modifies this set by tableau rules until there are no more rules to apply, part of the tableau rules are described below and other rules can be inferred by these rules.

(1) rule: If (ϕ) (i) and (ϕ) (i) , let (ϕ) (i) ; (2) rule: If (ϕ 1 ϕ 2 ) (i) and {(ϕ 1 ) (i) , (ϕ 2 ) (i) } , let {(ϕ 1 ) (i) , (ϕ 2 ) (i) } ; (3)  rule: If (ϕ 1 ϕ 2 ) (i) and (ϕ 1 ) (i) , let(ϕ 1 ) (i) ; If(ϕ 1 ϕ 2 ) (i) and (ϕ 2 ) (i) ,let (ϕ 2 ) (i) ; (4) EX rule: If (EXϕ 1 ) (i) and (AXϕ 1 ) (i)  ,let (AXϕ 1 ) (i) , and let (ϕ 1 ) (i+1) in all possible branches at the next time point ,then remove (AXϕ 1 ) (i) , (EXϕ 1 ) (i) ;

(5) AX rule: If (AXϕ 1 ) (i) and (EXϕ 1 ) (i)  , let (EXϕ 1 ) (i) , and let (ϕ 1 ) (i) in next time point in all branches at i+1, and all the branches are respectively recorded by l 1 ,l 2 ... ( 6) EG rule: If (EGϕ) (i) and (ϕ) (i) and use (ϕ) (i) , (ϕ) (i+1) •••to lable all the states aftertimeiandlet{(ϕ) (i) ,(ϕ) (i+1) •••(ϕ) (j) } (j m+2n-1), then remove(EGϕ) (i) and all the possible branches are recorded by l 1 ,l 2 ... [START_REF] Baader | Integrating description logics and action formalisms: First results[END_REF] AG rule: If (AGφ) (i) and (φ) (i) , use (ϕ) (i) , (ϕ) (i+1) • • • to lable all the states after time i and let {(ϕ) (i) ,(ϕ) (i+1) •••(ϕ) (j) } (j m+2n-1),then remove(EGϕ) (i) . ( 8) EU rule: If (E(ϕ 1 Uϕ 2 )) (i) ,for i there are two conditions: i m+n and i>m+n. When i>m+n, use (ϕ) (i) ,•••(ϕ) (k-1) ,(ϕ) (k) to lable all the states after time i and make {(ϕ) (i) ...(ϕ) (k-1) (ϕ) (k) } , then remove (E(ϕ 1 Uϕ 2 )) (i) , when i m+n,use (ϕ 1) ,(ϕ) (m+n) ,••• (ϕ) (k-1) ,(ϕ) (k) to lable all the states after time i and make{(ϕ) (i) ,•••(ϕ) (m+2n-1) ,(ϕ) (m+n) ,•••(ϕ) (k-1) ,(ϕ) (k) } , then remove (E(ϕ 1 Uϕ 2 )) (i) . For the two conditions, use l 1 ,l 2 ...to record the existing branches. (9) AU rule: If (A(ϕ 1 Uϕ 2 )) (i) ,for i there are two conditions: i m+n and i>m+n. When i>m+n, use (ϕ) (i) ,•••(ϕ) (k-1) ,(ϕ) (k) to lable all the states after time i and make {(ϕ

) (i) ,••• (ϕ) (m+2n-
) (i) •• (ϕ) (k-1) (ϕ) (k) }
, then remove (A(ϕ 1 Uϕ 2 )) (i) ,when i m+n, use (ϕ) (i) ,•••(ϕ) (m+2n-1) ,(ϕ) (m+n) ,•••(ϕ) (k-1) ,(ϕ) (k) to lable all the states after time i and make{(ϕ

) (i) ,•••(ϕ) (m+2n-1) ,(ϕ) (m+n) ,•••(ϕ) (k-1) ,(ϕ) (k) }
,then remove (A(ϕ 1 Uϕ 2 )) (i) . ( 10) EU rule: If (E(ϕ 1 Uϕ 2 )) (i) and at the same time (ϕ 1 ) (i) ,(ϕ 2 ) (i) , let {(ϕ 2 ) (i) ,(ϕ 2 ) (i) ϕ 1 } ; If(E(ϕ 1 Uϕ 2 )) (i) and (ϕ 2 ) (i) ,at the same time, (AXE(ϕ 1 Uϕ 2 )) (i) , let {(ϕ 2 ) (i) ,(AXE(ϕ 1 Uϕ 2 )) (i) } ,then,use the rule AX and EU defined above. (11) AU rule: If (A(ϕ 1 Uϕ 2 )) (i) and (ϕ 1 ) (i) ,(ϕ 2 ) (i) ,let {(ϕ 2 ) (i) , (ϕ 2 ) (i) ϕ 1 } ; If (A(ϕ 1 Uϕ 2 )) (i) and (ϕ 2 ) (i) ,(EXA(ϕ 1 Uϕ 2 )) (i) , let {(ϕ 2 ) (i) , (EXA(ϕ 1 Uϕ 2 )) (i) } , then,use the rule EX and AU defined above . (12) EG rule: If (EGϕ 1 ) (i) and (ϕ 1 ) (i) ,let (ϕ 1 ) (i) ; If (EGϕ 1 ) (i) and (AXEGϕ 1 ) (i) ,let (AXEGϕ 1 ) (i) , then,use the rule AX and EG defined above and use l 1 ,l 2 ...to record the existing branches.. (13) AG rule: If (AGϕ 1 ) (i) and (ϕ 1 ) (i) ,let (ϕ 1 ) (i) ; If (AGϕ 1 ) (i) and (EXAGϕ 1 ) (i) , let(EXAGϕ 1 ) (i) , then use the rule EX and AG defined above. It can be shown that the tableau rules always terminate with a finite set , which contains only time-stamped DL-assersions and the final is an ABox. Since there exists the branch time operator, it will generate not only one ABox, depending by the choices made in the rules. We say that A is induced by w.r.t π if it is one of the ABoxes produced by applying the above rules to { }. In this case, we introduce the verification problem based on dynamic description logic and conisder its dual, the satisfiability problem ,which is introduced in Definition 7. Finally, we reduce this problem to consistency of an ABox w.r.t an acyclic Tbox. This theorem can be proved with a similar process presented in [START_REF] Baader | Intergrate Action Formalisms into Linear Temporal Description Logic[END_REF]. Due to space limitations, we omitted the proof here.

Conclusions

Traditional verification technology is based on transition system and the property is specified in propositional logic, which limits the scope of describing the property. So, the temporal description logic DL-LTL is put forward to specify the temporal property in [START_REF] Baader | LTL over description logic axioms[END_REF]. Based on DL-LTL, F.Baader considers runtime verification problem in [START_REF] Baader | Runtime verification using a temporal description logic[END_REF], which observes changes to the state without knowing how they are caused.

In order to explore the cause of state transition, [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF] assumes the action can make the state change and then combine the decidable action theory based on description logic to decide whether there is an infinite execution atom actions that can satisfy the linear property specified in DL-LTL. At last, a specific approach is given for solving this problem.

However, [START_REF] Baader | Verifying properties of infinite sequences of description logic actions[END_REF] just considers the atom actions and just can verify the liner property. For such limitations, we consider complex action based on dynamic description logic and use the temporal description logic DL-CTL to specify the properties. For the verification problem whether the property specified in DL-CTL holds in a model generated by a complex action, we consider its dual, the satisfiability problem whether there is an execution of complex action that can satisfy the property. For the convenience of this problem, we abstract complex action to a non-deterministic finite state automaton (NFA) and consider whether there is a complex action accepted by NFA that satisfy the temporal property. Finally, we reduce this verification problem to consistency problem in description logic and give an approach to it.

In this paper, we abstract the action to a non-deterministic finite state automaton and every possible execution actions are accepted by this NFA. A future work will consider the actual action rather than its abstraction.

  A pre A red is an ABox which record the changes by actions on the named objects. For every ABox assertion ϕ, we define . If =C(a), = and if =r(a,b), = (a,b).

Theorem 1 .

 1 The DL-CTL formula is satisfiable w.r.t T, A and an NFA B iff there is an ABox A induced by w.r.t π such that A red A pre A is consisitent with T red .

Acknowledgements. This work is supported by the National Natural Science Foundation of China (Nos. 61363030, 61262030), the Natural Science Foundation of Guangxi Province (No.2012GXNSFBA053169, 2012GXNSFAA053220) and the Science Foundation of Guangxi Key Laboratory of Trusted Software.


Zuqiang Meng
email: mengzuqiang@163.com

Liang Jiang

Hongyan Chang

Yuansheng Zhang

A Heuristic Approach to Acquisition of Minimum Decision Rule Sets in Decision Systems

Keywords: Heuristic approach, minimum decision rule set, rule acquisition, classifier, data classification

In rough set theory, not too much work pays attention to the acquisition of decision rules and to the uses of the obtained rule set as classifier to predict data. In fact, rough set theory also can be applied to train data and create classifiers and then complete data prediction. This paper systematically studies the problem of acquisition of decision rules in decision systems. The main outcomes of this research are as follows: (1) the specific definition of minimum rule set is given, and such a minimum rule set can be used as a classifier to predict new data; (2) a new approach to finding out all minimum rule sets for a decision system, Algorithm 1, is proposed based on discrimination function, but with relatively low execution efficiency; (3) By improving Algorithm 1, a heuristic approach to computing a special minimum rule set, Algorithm 3, is proposed, which works far more efficiently than Algorithm 1. The outcomes can form the foundation for applying rough set theory to data classification and offer a new resolution to data classification.

Introduction

Rough set theory [START_REF] Pawlak | Rough Sets[END_REF] is a powerful mathematical tool to deal with insufficient, incomplete or vague information. Nowadays the majority of work in rough set theory focuses on attribute reduction [START_REF] Li | Quick Attribute Reduction in Inconsistent Decision Tables[END_REF] . Attribute reduction is in fact feature selection and has been applied to address many practical problems [START_REF] Liu | A Weighted Rough Set Based Method Developed for Class Imbalance Learning[END_REF][START_REF] Meng | A Fast Approach to Attribute Reduction in Incomplete Decision Systems with Tolerance Relation-based Rough Sets[END_REF][START_REF] Meng | Extended Rough Set-based Attribute Reduction in Inconsistent Incomplete Decision Systems[END_REF][START_REF] Yang | Applying rough sets to prevent customer complaints for IC packaging foundry[END_REF] . After attribute reduction, data sets can be used for a variety of applications and data classification is an important application. However, not too much work pays attention to data classification with rough set theory. In rough set theory, most methods of data classification are to use rough set theory to select features and then use other tools to train data and create classifier [START_REF] Hu | Mixed Feature Selection Based on Granulation and Approximation[END_REF] . In fact, rough set theory also can be used to extract decision rules from decision systems. Although some scholars have made contribution to this work [START_REF] Chang | An Approach for Attribute Reduction and Rule Generation Based on Rough Set Theory[END_REF][START_REF] Shao | Method of Rule Extraction Based on Rough Set Theory[END_REF][START_REF] Du | Rule Learning for Classification Based on Neighborhood Covering Reduction[END_REF] , there is still a lack of systematic foundation for rule acquisition in rough set theory. This paper systematically studies the problem of acquisition of decision rules in decision systems. First, the specific definition of minimum rule sets is given, and then a new approach to finding out all minimum rule sets for a decision system is proposed based on discrimination function, and finally a heuristic approach to computing a special minimum rule set is proposed. Each of the two proposed approaches has its own advantages and disadvantages. The work provides a relatively complete solution for extracting decision rules from decision systems and using rough set theory to classify data.

The rest of the paper is organized as follows. Section 2 reviews some basic concepts linked to Information system and decision logic. Section 3 gives the definition of minimum rule set. Section 4 proposes a general approach to the acquisition of all minimum rule sets in a given decision system. Section 5 then proposes a heuristic approach to the acquisition of a minimum rule set. Section 6 gives an example to show how to use the heuristic approach. Section 7 finally concludes the paper.

Information system and decision logic

An information system is usually expressed in the following form: IS = (U, A, {V a }, f a ) aA , where U is a nonempty finite set of objects, standing for a given universe; A is a nonempty finite set of attributes; V a is a value set(domain) of attribute a; f a is called information function, i.e., f a :U→V a , which denotes the value of function f on attribute a; If V a and f a are obvious, then (U, A, {V a }, f a ) aA can be denoted as (U, A) for short.

For any BA, subset B determines a binary relation, denoted as TR(B), which is defined as follows: TR(B) = {(x,y) | f a (x)= f a (y) for any aB and any x,yU}.

It is easy to prove that TR(B) is reflexive, symmetric, transitive, and thereby is an equivalence relation on U. Thus, equivalence relation TR(B) can divide the universe U into several disjoint subsets, which are known as equivalence classes. Suppose that X 1 , X 2 , …, X n are all equivalence classes induced by attribute set

B, then {X 1 , X 2 , …, X n } is a partition U/TR(B) of the universe U, denoted by U/TR(B) = {X 1 , X 2 , …, X n }.
Extraction of decision rules is in fact the problem of extracting description of granules (equivalence classes), which are expressed with decision logic.

Let IS(B) = <U, B, {Va}, fa>a ∈B, B ⊆A. Then decision logic language DL(B) with respect to B is defined as following:

(1) (a, v) is an atomic formula, where a ∈B, v ∈Va, (2) an atomic formula is a formula in DL(B);

(3) if φ is a formula, then ~φ is also a formula in DL(B); (4) if both φ and ψ are formulae, then φ∨ψ, φ∧ψ, φ→ψ, φ≡ψ are all 3 formulae;

(5) only the formulae obtained according to the above Steps (1) to (4) are formulae in DL(B).

If φ is a simple conjunction, which consists only of atomic formulae and connectives ∧, thenφis called a basic formula.

The following definition gives the relationship between formulae in DL(B) and granules IS(B):

For any s∈U, the relationship between s and formulae in DL(B) is defined as following:

(

(φ) = { s | s |= φ}, that is, m(φ)
is the set of all those objects that satisfy formula φ; For subset g⊆U, if m(φ) = g, then g is said to be descriptive and φ is a description of g, denoted by DES(g). It is easy to find that for the same subset g⊆U, there are possibly many different descriptions:

φ 1 , φ 2 , …, φ m , such that m(φ 1 ) = m(φ 2 ) =…= m(φ m ) = g
. This is one of the reasons why extracting all decision rules from a decision system is a NP-hard problem.

Minimum rule set in decision system

We note that some principles of attribute reduction can also be applied to extracting decision rules from decision systems and then to acquiring minimum rule set, which can be used as a classifier.

Decision system is a special case of information system, which can be regarded to be generated by partitioning attribute set A into two disjoint subsets, or by adding some attributes to A.

A decision system is usually denoted by DS = (U, C∪D, {V a }, f a ) aA=C∪D ,where U, V a and f a have the same meanings as that in the above section; C is a nonempty finite set of attributes, called condition attribute set; D is a nonempty finite set of attributes, called decision attribute set, and C∩D=; The 4-triple (U, C∪D, {V a }, f a ) aA=C∪D is usually denoted as (U, C∪D) for short, namely, DS=(U, C∪D).

As mentioned above, we can consider that decision system (U, C∪D) consists of two information systems: (U, C) and (U, D).

Suppose thatφDL(C) andψDL(D). Implication form φ→ψ is said to be a decision rule in decision system (U, C∪D). If bothφ andψ are basic formula, then φ→ψ is called basic decision rule.

Decision rule has two important measuring indices, confidence and support, which are defined as following:

conf(  → )= | ) ( | | ) ( ) ( |    m m m  [11] [1] sup(  → ) = | | | ) ( ) ( | U m m    [2]
where conf(  → ) and sup(  → ) are confidence and support of decision rule  → , respectively.

In general, we usually find those decision rules whose confidence is equal to 1.

Obviously, if m(  ) ⊆ m( ), then conf(  → ) = 1.
Of course, it is not enough to guarantee that confidence is equal to 1. In fact, the larger the confidence, the better it is, although it is small than 1 with certainty. That is, extracting decision rules is the procedure of finding those rules whose confidence is equal to 1 and whose support is as large as possible. In order to illustrate this procedure, we further introduce some related concepts. Proof. It is straightforward.

Property 1 shows that with the decrease of attribute subset, corresponding equivalence classes become larger and larger, thus increase corresponding rule's support. That is, by deleting some attributes from C, we can increase rule's support according to formula (2), which is the foundation of finding decision rules in this paper.

In fact, by deleting some attributes from condition attribute set, every object in the universe U can induce at least one decision rule. Thus, all objects from U can induce a lot of decision rules and then form a very large decision rule set. Obviously, many rules are redundant and should be removed from rule set. Therefore, one basic problem is that what is the criterion of a minimum rule set? Definition 2. For decision system DS = (U, C∪D), if ruleφ→ψ is true in DL(C∪D), i.e., for any xU x|=φ→ψ, then ruleφ→ψ is said to be consistent in DS, denoted by |= DS φ→ψ; if there exists at least object xU such that x |=φ∧ ψ,then ruleφ→ψ is said to be satisfiable in DS.

5

Consistency and satisfiability are the basic properties that must be satisfied by decision rules. In addition, an efficient and effective decision rule set should be as small as possible, that is, it should be minimized. Definition 3. For decision system (U, C∪D), object xU and decision rule r: φ →ψ, if x|=r, then it is said that rule r covers object x, or object x is covered by rule r; let coverage(r) denote the set of all objects that are covered by rule r and coverage -1 (x) the set of all rules that cover object x, that is:

coverage(r) = {xU | x|= r}, coverage -1 (x) = {r′ | r′ cover x, i.e.
, xcoverage(r′)}. Definition 4. For decision system (U, C ∪ D), decision rules r 1 and r 2 , if coverage(r 1 )⊆coverage(r 2 ), then it is said that r 2 functionally cover r 1 , denoted by

r 1  r 2 .
Obviously, those rules that are functionally covered by other rules should be removed out from rule set.

Definition 5. For decision system (U, C ∪ D) and xU, [x] B is said to be maximized if [x] B  [x] C and for any B′B [x] B  [x] D , where B  C; rule DES([s] B ) → DES([s] D ) is said to be reduced if [x] B is maximized.
A decision rule set  is said to be minimal if it satisfies the following properties:

(1) any rule from  should be consistent;

(2) any rule from  should be satisfiable;

(3) any rule from  should be reduced; (4) for any two rules r 1 , r 2  , neither r 1  r 2 nor r 2  r 1 .

When a decision rule set satisfies all the four properties, each rule is effective and the whole rule set is minimal and then matching efficiency can be improved greatly.

A general approach to acquisition of all minimum rule sets

Suppose thatφ be a formula and B = {a 1 , a 2 , …, a m } be a condition attribute subset. Let set(φ) be the set of all attributes that appear in formula φ ,and  B and  B respectively be the simple conjunction and the simple disjunction that consists of all the attributes appear in B with  as connective, i.e.,

 B = a 1  a 2  …  a m . For example, letφ= a  b  c then set(φ)={a, b, c}; let B = {a, b, c} then  B = a  b  c and  B = a  b  c. Definition 6. For decision system (U, C∪D), let ([x] C , x′) =  {aC | x′  [x] {a} }, where x, x′  U; suppose that U -[x] D = {x′ 1 , x′ 2 , …, x′ m },

then the discrimination function of [x]

C is defined as following:

f([x] C ) = ([x] C , x′ 1 )  ([x] C , x′ 2 )  …  ([x] C , x′ m ).
The discrimination function is a conjunctive normal form. By using absorption law and distribution law, it can be converted to be a disjunctive normal form, which consists of several simple conjunctions. Each simple conjunction corresponds to a decision rule. Without loss of generality, suppose that f(

[x] C ) is converted to disjunctive normal form  1   2  …   m′ ,
where  i is a simple conjunction, i=1,2,…, m′. Then all the rules that induced by equivalence class [x] C are as follows: r 1 : DES(

) ( 1 ] [  set x ) → DES([x] D ), r 2 : DES( ) ( 2 ] [  set x ) → DES([x] D ), r m′ : DES( ) ( ] [ m set x   ) → DES([x] D ).
Let R([x] C ) be the set of all rules that induced by [x] C , i.e., R([x]C) = {r 1 , r 2 , ..., r m′ }. Suppose that decision class [x] D is an union of several equivalence classes:

[x 1 ] C , [x 2 ] C , ..., [x p ] C , i.e., [x] D = [x 1 ] C ∪[x 2 ] C ∪... ∪[x p ] C . Let R([x]D) = R([x 1 ] C )∪R([x 2 ] C ) ∪...∪R([x p ] C ).
Obviously, some induced rules in R([x] D ) are redundant and should be removed from rule set. Or in other words, R([x] D ) needs to be further reduced.

Definition 7. For decision system (U, C∪D) and decision class

[x] D , suppose  is a subset of rule set R([x] D ), i.e.,   R([x] D ), then  is a reduct of R([x] D ) if
any rule in  is consistent, satisfiable, reduced and for any two rules r 1 , r 2  , neither r 1  r 2 nor r 2  r 1 .

Similar to attribute reduction, R([x] D

) possibly has more than one reduct. We can also use discrimination function to find all reducts of R([x] D ).

Suppose [x]

D = {x 1 , x 2 , ..., x h }. Let f([x] D ) = [  coverage -1 (x 1 )]  [  coverage - 1 (x 2 )]  …  [  coverage -1 (x h )]. Obviously, f([x] D ) is a conjunctive normal form.
Similarly, it can be converted to a disjunctive normal form by using absorption law and distribution law, in which each simple conjunction corresponds to a reduct of

R([x] D ). Assume that f([x] D ) is converted to disjunctive normal form

 1   2  …   h′ . Then all reducts of R([x] D ) are as follows: set( 1 ), set( 2 ), …, set( h′ ).
It is not difficult to prove that for any r  set( i ), r is consistent, satisfiable, reduced and for any two rules r 1 ,

r 2  set( i ), neither r 1  r 2 nor r 2  r 1 , i  {1, 2, …, h′}. Therefore, set( i ) is a reduct of R([x] D ). Again, we know that that if [x 1 ] D ≠[x 2 ] D then [x 1 ] D ∩[x 2 ] D = and then R([x 1 ] D )∩R([x 2 ] D ) =.
([x i ] D ); (3) for each [x′] C EC([x i ] D ), compute R([x′] C ) using discrimination function and then obtain R([x i ] D )=∪{R([x′] C ) | [x′] C EC([x i ] D )}; (4
) find all reducts of R([x i ] D ) using discrimination function, and suppose the set of all reducts of R(

[x i ] D ) is RED[R([x i ] D )];
(5) compute the set of all minimum rule sets: { 

n i i 1   | i   RED[R([x i ] D )],
where i{1,2,…,n}}.

Steps ( 2)-( 4) can be performed concurrently, with which we can improve the efficiency of the approach. The biggest advantage of this approach lies in that it can find out all minimum rule sets for a decision system. However, we know that in steps ( 3) and ( 4) discrimination function is used, where a conjunctive normal form is converted to be a disjunctive normal form using absorption law and distribution law. This conversion involves problem of combination explosion and is a NP-hard problem. Therefore, the approach is suitable for large data set. Furthermore, it is unnecessary to find all minimum rule sets for a decision system in real applications. In fact, a special minimum rule set is more desired in most cases. Therefore, the time-consuming steps, conversion of conjunctive normal form to disjunctive normal form, should be abandoned in real applications.

A heuristic approach to acquisition of a minimum rule set

Suppose that f(t 1 , t 2 , …, t r ) is a conjunctive normal form, where t 1 , t 2 , …, t r are r different items that occur in the formula. They can stand for attributes or rules. Further, suppose that after using absorption law:

f(t 1 , t 2 , …, t r ) = 1   2   …  k  ,
where i  is a simple disjunction, and for any different simple disjunctions i  and j  , neither set( i  )  set( j  ) nor set( j  )  set( i  ), i,j{1,2,…,k}. Now we introduce how to obtain a special simple conjunction of f(t 1 , t 2 , …, t r ), which corresponds to a reduct of attribute set or rule set.

Let us sort items t 1 , t 2 , …, t r in an ascending order by their occurring frequencies in formula f(t 1 , t 2 , …, t r ) and suppose the ascending order is <t′ 1 , t′ 2 , …, t′ r >, where t′ r occurs most frequently in formula f(t 1 , t 2 , …, t r ) and therefore it is viewed as the most important item. That is, the finally obtained simple conjunction should contain some important items like …, t r-1 , t r and remove some unimportant items like t 1 , t 2 , … as possible. The approach to obtaining a special simple conjunction of f(t 1 , t 2 , …, t r ) is called Algorithm 2, which is described as follows. 9

Table 1. A decision system U a 1 a 2 a 3 d x 1 2 3 2 1 x 2 1 1 1 2 x 3 3 3 3 3 x 4 2 2 2 3 x 5 2 2 1 2 x 6 2 3 3 1
According to Algorithm 3, steps to obtain a special minimum rule set are as follows:

(1) by computing, DC(DS) = {{x 1 , x 6 },{x 2 , x 5 }, {x 3 ,

x 4 }} = {[x 1 ] D , [x 2 ] D , [x 3 ] D }; (2) for decision class [x 3 ] D DC(DS), EC([x 3 ] D ) = {{x 3 }, {x 4 }} = {[x 3 ] C , [x 4 ] C }; f([x 3 ] C ) = (a 1  a 3 )  (a 1  a 2  a 3 )  (a 1  a 2  a 3 )  a 1 ,
] C ) = {(a 2 , 2)  (a 3 , 2)→(d, 3)}; finally, R′′([x 3 ] D ) = R′′([x 3 ] C )∪R′′([x 4 ] C ) = {(a 1 , 3)→(d, 3), (a 1 , 2)  (a 1 , 2)→(d, 3)}; (3)
by the similar way, we can compute R′′([x 1 ] D ) and R′′([x 2 ] D ). All the results are as follows: That is, {r 1 , r 2 , r 4 , r 5 , r 6 } is a special minimum rule set that obtained by Algorithm 3. We can prove that any rule in the rule set is consistent, satisfiable, reduced and for any two rules r 1 , r 2 in the rule set, neither r 1  r 2 nor r 2  r 1 . So it is a minimum rule set.

R′′([x 1 ] D ) = {r 1 : (a 2 , 3)  (a 3 , 2)→(d, 1), r 2 : (a 1 , 2)  (a 3 , 3)→(d, 1)} R′′([x 2 ] D ) = {r 3 : (a 3 , 1)→(d, 2),

Conclusion

In rough set theory, many scholars pay more attention to attribute reduction, and not too much work pays attention to the acquisition of decision rules with rough set theory. Most methods use rough set theory to reduce data in the first place, and then use other algorithms, such as CART, SVM [START_REF] Hu | Mixed Feature Selection Based on Granulation and Approximation[END_REF] , to create classifier based on the reduced data and use it to classify or predict new data. In fact, rough set theory can also be used to extract decision rules from data sets. By creating minimum rule sets, which is used as classifiers, we can also achieve better data prediction. In this paper, we propose two important algorithms, Algorithm 1 and Algorithm 3. Algorithm 1 can find out all minimum rule sets for a given data set theoretically. But it applies discrimination function to complete its computing, which is a time-consuming operation, so its disadvantage is low efficiency, especially for large data sets. By improving Algorithm 1, a heuristic approach to computing a special minimum rule set, Algorithm 3, is proposed. Using occurring frequency of attributes or rules as heuristic information, Algorithm 3 can rapidly obtain a special minimum rule set. It works far more efficiently than Algorithm 1 and has high application value.

Definition 1 . 1 .

 11 For decision system (U, C∪D), B ⊆C and x∈U, let [x] B = {y ∈U | (x, y) ∈TR(B)}, then [x] B is said to be an equivalence class with respect to attribute subset B. Property For decision system (U, C∪D), B 1 ⊆B 2 ⊆C and any x∈U, [x] B2 ⊆ [x] B1 .

1 .Algorithm 1 . 7 ( 1 )

 1171 Hence for any two different decision classes [x 1 ] D and [x 2 ] D , we may concurrently calculate all reducts of [x 1 ] D and [x 2 ] D . According to analysis above, we can give a complete solution to acquisition of all minimum rule sets in decision system DS = (U, C ∪ D), which is called Algorithm For calculating all minimum rule sets. compute all different equivalence classes: [x 1 ] D , [x 2 ] D , ..., [x n ] D , and let DC(DS) = {[x 1 ] D , [x 2 ] D , ..., [x n ] D }; (2) for decision class [x i ] D DC(DS), find out all equivalence classes whose union is equal to [x i ] D , and suppose the set of all such equivalence classes is EC

r 4 :

 4 (a 3 , 1)→(d, 2)} R′′([x 3 ] D ) = {r 5 : (a 1 , 3)→(d, 3), r 6 : (a 2 , 2)  (a 3 , 2)→(d, 3)} (4) by computing, we have: coverage -1 (x 1 ) = {r 1 }, coverage -1 (x 2 ) = {r 3 , r 4 }, coverage -1 (x 3 ) = {r 5 }, coverage -1 (x 4 ) = {r 6 }, coverage -1 (x 5 ) = {r 3 , r 4 }, coverage -1 (x 6 ) = {r 2 }. Take RED′′[R′′([x 2 ] D )] for example. Because f([x 2 ] D ) = (r 3  r 4 )  (r 3  r 4 ) and the ascending order is <r 3 , r 4 >, so it can be found that {r 4 } is a reduct of f([x 2 ] D ) and therefore RED′′[R′′([x 2 ] D )] = {r 4 }; by the same way, RED′′[R′′([x 1 ] D )] = {r 1 , r 2 }, RED′′[R′′([x 3 ] D )] = {r 5 , r 6 }; (5) the finally obtained minimum rule set is RED′′[R′′([x 1 ] D )]∪RED′′[R′′([x 2 ] D )] ∪RED′′[R′′([x 3 ] D )] = {r 1 , r 2 }∪{r 4 }∪{r 5 , r 6 } = {r 1 , r 2 , r 4 , r 5 , r 6 }.

  |= φ∧ψ iff s |= φ and s |= ψ (4) s |= φ∨ψ iff s |= φ or s |= ψ (5) s |= φ→ψ iff s |= ~φ∨ψ (6) s |= φ≡ψ iff s |= φ→ψ and s |=ψ→φ.For formula φ, if s |= φ, then we say that the object s satisfies formula φ. Let m

	1) s |= (a, v) iff fa(s) = v
	(2) s |= ~φ iff not s |= φ
	(3) s

  and through the statistics the ascending order is <a 2 , a 3 , a 1 >, and then by using Algorithm 2, the obtained reduct of f([x 3 ] C ) is {a 1 }; so we have R′′([x 3 ] C ) = {(a 1 , 3)→(d, 3)}, and similarly, we have R′′([x 4

Acknowledgement. This work is supported by the National Natural Science Foundation of China (No. 61363027) and the Natural Science Foundation of Guangxi Province, China (No. 2012GXNSFAA053225).

Algorithm 2. For calculating a special simple conjunction (called a reduct of f(t 1 , t 2 , …, t r ) for simplicity).

(1) let f′ = f(t 1 , t 2 , …, t r ) (2) for i = 1 to r do { (3) for each j  in f′, if there is no such j  in f′ that set( j  ) = {t′ i } then remove item t i from j  for each j  , denoted by j  = j  -{t i };

(4) apply absorption law to f′;

) for example. It can be observed that the occurring frequencies of a 1 , a 2 , a 5 , a 3 , a 4 are 2, 2, 2, 3, 3, respectively. According to Algorithm 2, the reduction steps are as follows:

(3) after applying absorption law: f′ = (a 3 )  ( a 2  a 4 )  (a 4  a 5 ); (4) remove a 2 from f′: f′ = (a 3 )  (a 4 )  (a 4  a 5 );

(5) after applying absorption law: f′ = (a 3 )  (a 4 ); (6) as a result set(f′) = {a 3 , a 4 }. By using Algorithm 2, we can modify Algorithm 1 to a heuristic approach, which is used to acquire a special minimum rule set and is described as follows:

Example analysis

Consider decision system DS = (U, C∪D), where U = {x 1 , x 2 , …, x 6 }, C = {a 1 , a 2 , a 3 } and D = {d}, presented in Table 1.


Wenjun Cheng

Yuhui Gao

Using PDDL to Solve Vehicle Routing Problems

Keywords: Artificial Intelligence Planning, Vehicle Scheduling, PDDL, Vehicle Routing

In this paper, we describe a search method based on the language PDDL for solving vehicle routing problems. The Vehicle Routing Problem (VRP) is a classical problem in Operations Research, and there are many different variants of the VRP. This paper describes a new approach to model standard VRP and some variants based on PDDL language, explains how the method constructs model and solves the problem using several PDDL planners, and analyses the planning results of these planners.

Introduction

The vehicle routing problem is a well-known combinatorial optimization problem in the field of service operations management and logistics [START_REF] Laporte | Fifty Years of Vehicle Routing[END_REF]. It is described as finding the minimum distance or cost of the combined routes of a number of vehicles that must service a number of customers. The number of feasible solutions for the VRP increases exponentially with the number of customers to be serviced, and almost each of VRP's variants is more complicated than standard VRP. Since there is no known polynomial algorithm that will find the optimal solution, the VRPs is considered NPhard. For finding solutions of such problems, the use of problem-specific solvers with heuristics is considered a reasonable approach that most of VRP research is based on. However it is realistic to solve VRPs that are structured in the same way using universal planners. This paper describes the methods to model some of the variants of VRP in PDDL. The planners for PDDL are automated, which means that they solve the problem by using heuristics that are pre-developed, meaning that the heuristics do not change depending on the type of problem. So it provides attempt to solve the VRPs through a uniform method. The remainder of this paper is organized as follows. Section 2 introduces the VRP and its multiple variants; Section 3 describes the features of PDDL language and the main versions of PDDL; Section 4 gives the models of several VRPs based on PDDL; Section 5 provides some efficient PDDL planners to solve the models and compares the planning results. Section 6 concludes with a brief discussion and perspectives.

The standard VRP and its Variants

The standard VRP can be described as a weighted graph G=(V, A, d) where V={v 1 ,v 2 ,…,v n } is a set of vertices representing locations with the depot located at v1 and A is the set of arcs. With every arc(v i , v j ) (i ≠ j) is associated a non-negative distance d which can be interpreted as a travel cost or as a travel time. The standard VRP consists of designing a set of least-cost vehicle routes in such a way that  Each customer is visited only once by a single vehicle, and is served according to their demand.  Each vehicle must start and end its route at the depot v1, and it is not allowed to visit the depot in between.

The standard VRP can be extended in multiple ways which add some constraints to be satisfied. The most common constraints include:

 Capacity restrictions: each vehicle has finite capacity and each location has a finite demand. So the sum of the demands for the vehicle's tour does not exceed its capacity. Capacity-constrained VRPs will be referred to as CVRPs.  Total time restrictions: the length of any route may not exceed a prescribed bound.

Time-constrained or distance-constrained VRPs will be referred to as DVRPs.  Time windows restrictions: the service at each customer must start within an associate time window and the vehicle must remain at the customer location during service. The VRP with time windows will be referred to as VRPTW.  Other restrictions including multiple depots, multiple goods, multiple service modes, multiple transport modes, or different optimization goals. So there are a variety of VRP variants such as multiple depot vehicle routing problem (MDVRP), the vehicle routing problem with backhauls (VRPB), the vehicle routing problem with backhauls and time windows (VRPBTW), and VRP with pickup and delivery (VRPPD).

These VRPs were made by industrial requirements and have been studied since 1995.

With the simpler variants of the VRP being solved, the VRP research community pays more attention to rich VRP models and larger size problems recently. We prefer to construct some common models to descript most of VRP variants from simple to complex, and choose a uniform way to solve these models. In the field of artificial intelligence (AI), PDDL is an expressive language which offers to represent many planning knowledge while freeing from the plan search algorithms, and PDDL can satisfy the demand of modelling various kinds of VRP.

PDDL and its Versions

PDDL, the "Planning Domain Definition Language", is a standard language for expressing planning problems and domains is widely used in the planning community [START_REF] Mcdermott | PDDL-The Planning Domain Definition Language[END_REF]. This enables us to effortlessly select the best suited planner for describing the technical and epistemological requirements of planning domains and the capabilities of planners in a uniform way. A planning problem is made of an initial state, a final state and a set of operators; a state is a set of predicates and operators can be seen as a couple of states: preconditions which must be true to allow execution and effects which are true after execution. In PDDL, the specification of the predicates and the operator schemas is separated from the specification of the initial state and the goal condition. The former is typically referred to as the planning domain and the latter as the planning problem, so a number of planning problems can be defined for the same planning domain.

There are dozens of different versions of PDDL and its extension. Every version of PDDL specifies new requirements that should be supported and increases the flexibility and functionality of PDDL language. PDDL1.2 states the basics of the language, such as how the domain and problem file should be composed. One of the most important PDDL versions is 2.1, which specifies the possibility to use numerical variables, plan-metrics, and durative actions which make planning with conditions such as fuel consumption, time constraints and capacity constraints possible [START_REF] Fox | PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains[END_REF]. In PDDL versions 2.2, derived predicates and timed initial literals which are useful in modelling VRPs are specified [START_REF] Edelkamp | PDDL2.2: The Language for the Classical Part of the 4th International planning Competition[END_REF]. However, for higher PDDL versions, only a few planners provide effective support, and we cannot use the specifications of these PDDL versions.

PDDL Models

PDDL Model for CVRP

In the problem there are three different types: freights, vehicles, and locations. Planning problems predicates are objects that are described using Boolean representation. The following predicates represent facts related to the types.  (at freight ?f, location ?l): the freight ?f is currently at the location ?l.  (at2 vehicle ?v, location ?l): the vehicle ?v is currently at the location ?l.  (adjacent location ?l1, location ?l2): the location ?l1 is adjacent to ?l2.  (in freight ?f, vehicle ?v): the freight ?f is currently loaded by the vehicle ?v.  (using vehicle ?v): the vehicle ?v is not at the depot.  (destination freight ?f location ?l): the location ?l is the destination of the freight ?f. Planning problems functions are objects with states that can be represented numerically (also called numerical fluents). The following predicates represent facts related to the types.  (totalCost): this descripts the variable that keeps track of the total cost of the solution. It is the key function to solve Multi-criterion and multi-objective optimal problems.  (weight freight ?f): this descripts the weight of the freight ?f.  (maxLoad): this descripts the maximum load limit of all vehicles.

 (load vehicle ?v): this descripts how much weight the vehicle ?v is carrying.  (distance location ?l1 location ?l2): this descripts the distance between ?l1 and ?l2.

This function is only available for adjacent locations.

Actions are events that change the state of the problem. The available actions in the domain are defined in terms of their preconditions and effects using the available predicated and the functions of the domain. For example, the follow PDDL statement is an action schema as it appears in the CVRP PDDL domain that represents the actions of the vehicle loading the freight.

(:action load :parameters (?f -freight ?v -vehicle ?l -location) :precondition ( and (using ?v) (at ?f ?l) (at2 ?v ?l) (>= (maxLoad) (+(load ?v) (weight ?f)))) :effect ( and (in ?f ?v) (not (at ?f ?l)) (increase (cargo ?v) (weight ?f)))) )

In this problem there are four actions possible:  useVehicle(vehicle ?v): set the vehicle ?t as available for use.

precondition: the vehicle ?v is not in use. effect: the vehicle ?v is in use.  load(freight ?f, vehicle ?v, location ?l): loads the freight ?f into the vehicle ?v at the location ?l. precondition: the vehicle ?v is in use; it and the freight ?f are both at the tion ?l; maxLoad >= load v + weight f . effect: the freight ?f is in the vehicle ?v and is not at the location ?l; load v =load v +weight f .  unload(freight ?f, vehicle ?v, location ?l): unloads the freight ?f from the vehicle ?v at the location ?l. precondition: the vehicle ?v is in use and at the location ?l where is the destination of the freight ?f; ?f is in the vehicle ?v. effect: the freight ?f is at the location ?l and is not in the vehicle ?v; load v =load vweight f .  move(vehicle ?v, location ?l 1 , location ?l 2 ): moves the vehicle ?v from ?l 1 to ?l 2 .

precondition: the vehicle ?v is in use and at the location ?l 1 ; ?l 1 is adjacent to ?l 2 . effect: the vehicle ?v is at ?l 2 and not at ?l 1 .

Inside the problem file, all types of planning objects are defined and initialized, and the planning goal is set. The domain that is described above can have many VRP problem files, which might differ by the number of objects, initial values and goal.

For CVRP PDDL domain, all freights should be at their respective goal location and all vehicles should have returned to their respective origin. The function "totalCost" should be minimized which is the metric of the problem and always equal to the objective function. Some PDDL features need to be supported in constructing PDDL models for CVRP: typing, fluents, plan metrics. These features are specified before PDDL version 2.1, so the models can be solved by any planner which supports PDDL2.1.

PDDL Models for DVRP and VRPTW

In the PDDL model for DVRP, it is necessary to convert the transport of vehicles to durative actions. So the PDDL feature "durative actions" is added to the feature list which is must be supported in the PDDL model. Some correspond changes must be applied to the former PDDL model for CVRP. For example, the follow PDDL statement is a durative action schema that represents the actions of the vehicle loading the freight.

(:durative-action load :parameters (?f -freight ?v -vehicle ?l -location) :duration(= ?duration (loadTime ?f)) :condition ( and (over all(using ?v)) (at start(at ?f ?l)) (at start(at2 ?v ?l)) (at start(>= (maxLoad) (+ (load ?v)(weight ?f))))) :effect ( and (at end(in ?f ?v)) (at start(not (at ?f ?l))) (at end(increase (load ?v) (weight ?f))))) ) (loadTime freight ?f): this function descripts how long the freight ?f is loaded or unloaded by vehicles.

In VRPTW, there are individual time windows for each customer, and possibly also on the depot. The PDDL feature "timed initial literals" has the possibility to make predicates available according to predetermined times and consequently to make actions feasible at special time. This feature is specified in PDDL 2.2 and only a few planners support it. Only one predicate wants to be added to the domain file of DVRP model to support time windows.

(available ?f -freight) : descripts the freight ?f available(depend on time windows).

The PDDL planning problem generated for above modes is the following (most of the predicates should be self-explanatory): (and (at f1 l1) (at f2 l1) (at2 v1 l1) (at2 v2 l1)) ) (:metric minimize (totalCost)) )

PDDL Models for Other VRPs

For other VRPs, such as MDVRP, VRPB, VRPBTW and VRPPD, the different from above VRPs is focused on multiple vehicle types, multiple service types, route restrictions, and freight constraints. It doesn't need more PDDL features to describe the PDDL model for these VRPs. All we need to do is providing more predicates, functions and actions.

Performance of PDDL Planners

The PDDL planners are automated and the heuristics search algorithms embedded in them does not change depending on the type of problem. There are many PDDL planners available on the internet, with certain characteristics that may make them more or less suitable for different kinds of planning problems. The planners we tried were SAPA [START_REF] Do | SAPA: A multi-objective metric temporal planner[END_REF], LPG-TD [START_REF] Gerevini | LPG: A planner based on a local search for planning graphs with action costs[END_REF][START_REF] Gerevini | I: Integrating Planning and Temporal Reasoning for Domains with Durations and Time Windows[END_REF][START_REF] Gerevini | An approach to temporal planning and scheduling in domains with predictable exogenous events[END_REF], SGPlan6 [START_REF] Chen | Temporal planning using subgoal partitioning and resolution in SGPlan[END_REF], TFD [START_REF] Eyerich | Using the context enhanced additive heuristic for temporal and numeric planning[END_REF], POPF2 [START_REF] Coles | Forward chaining partial-order planning[END_REF] and DaeYa [START_REF] Dréo | Divide-and-Evolve: The marriage of Descartes and Darwin[END_REF]. All of these planners can solve the DVRP problems because they have the ability to satisfy the "durative-action" feature of PDDL 2.1 and process the problems which contain durative actions. But only SAPA, LPG-TD, POPF2 and SGPlan support the "timed-initial-literals" feature of PDDL 2.2 and can solve the VRPTW problems. Figure 1 shows the performance of planners on DVRP benchmark instances. 20 DVRP instances used range from between 10 to 30 locations, 10 to 50 freights, and from 10 to 20 vehicles which are auto-generated using the code in Matlab.

Figure 2 shows the performance of planners on VRPTW benchmark instances. 12 VRPTW instances used range from between 10 to 20 locations, 10 to 30 freights, and from 10 to 20 vehicles which are auto-generated using the code in Matlab.

DaeYa planner performs the best of the planners in the DVRP case and LPG-td planner performs the best of the planners in the VRPTW case. We only consider the small-scale VRP problems because the performances of most PDDL planners are not the same level as problem-specific solvers.

Conclusions

This paper describes a new approach to model standard VRP and some variants based on PDDL language, explains how the method constructs model and solves the problem using several PDDL planners, and analyses the planning results of these planners.

Comparing to problem-specific solvers, this method provides common models to describe VRP problems and uniform solving mode by using different planners. Although the performances of multiple PDDL planners are not the same level as problem-specific solvers, it is realistic to expect planners to solve problems that are structured in the same way as real-world problems.

  f1 -freight f2 -freight v1-vehicle v2-vehicle l1 -location l2 -location l3 -location) (:init (adjacent l1 l2) (adjacent l2 l1) (adjacent l1 l3) (adjacent l3 l1) (= (distance l1 l2) 22) (= (distance l2 l1) 22) (= (distance l1 l3) 25) (= (distance l3 l1) 25) (= (weight f1) 8) (= (weight f2) 9) (= (load v1) 0) (= (load v2)0) (at 0 (available f1)) (at 100 (not (available f1))) (at 0 (available f2)) (at 100 (not (available f2))) (= (maxLoad) 10) (= (totalCost) 0) (at f1 l2) (at f2 l3) (at2 v1 l1) (at2 v2 l1) (destination f1 l1) (destination f2 l1) ) (:goal

Fig. 1 .

 1 Fig. 1. DVRP Benchmark

Fig. 2 .

 2 Fig. 2. VRTTW Benchmark


Ruo Shu
email: shuruo@upc.edu.cn

Shibao Li
email: lishibao@upc.edu.cn

Xin Pan

An Optimization Scheme for SVAC Audio Encoder

Keywords: SVAC audio encoder, MEL-frequency ceptral coefficients, bandwidth expansion, linear predictive coding coefficients, quality evaluation

Both audio signals and MEL-frequency cepstral coefficients are encoded in SVAC audio encoder. These two independent processing leads to structural redundancies for the encoder design. This paper proposes an optimization scheme using MEL-frequency cepstral coefficients to realize high-frequency reconstruction and removes Bandwidth Extension module of the original encoder. Simulation results prove that the new encoder has considerable improvement on structure, reconstructed high-frequency precision and coding quality.

Introduction

Surveillance video and audio coding is designed for application in the field of national security and defense, and is important for maintaining public security and fighting and preventing criminal activities. Chinese government started to establish the national standard of surveillance video and audio coding (SVAC) in 2008, and the standard was approved and published in 2010. At present, the corresponding products are in promotion and have wide application future.

Different from conventional audio encoders mainly used in multi-media fields, SVAC audio encoder has some special technical characteristics for the particularity of applications, such as providing a high recognition rate for voiceprint recognition in back-end after signals are decoded and real-time responses when special events occur, etc. These new techniques lead to complex algorithms, and in addition, combining them with conventional coding technologies simply and directly result in many structural redundancies in SAVC audio encoder. Therefore structure optimization for the encoder needs further research. This paper proposes an optimization scheme for SVAC audio encoder. The new method reconstructs high-frequency content of signal based on decoded MELfrequency cepstral coefficients (MFCCs) extracted and coded in front-end, and removes the Bandwidth Extension (BWE) module in original encoder.

SVAC audio encoder

The overall framework of SVAC audio encoder is shown in Figure1. The coding processing can be divided into two parallel parts: audio coding and characteristic parameters coding. After sampling rate conversion, input PCM signal in one road is transferred to audio coding module, and can be encoded in different bitrates controlled by the levels of events detected in abnormal events detector. The other road signal is sent to characteristic parameters coding module in which the wellknown MFCCs are extracted, quantified and coded in order to prevent the influence of speech coding distortion on voiceprint recognition in back-end.

In audio coding module, input signal is divided into low-frequency band and high-frequency band. Based on the signal type, low-frequency signal is encoded in two switch modes: Algebraic Code Excited Linear Prediction (ACELP) and Transform Audio Coding (TAC), and high-frequency signal is encoded through BWE technology which consumes little bitrates. In characteristic parameters extracting module, MFCCs are extracted, and then quantified and coded in subsequent modules. Here two coding modes are offered for MFCCs: direct coding mode and predictive coding mode (dotted line in Figure 1). The latter one firstly decodes bit stream of the audio encoder and acquires reconstructed signal, then MFCCs of reconstructed signal and original signal are extracted respectively. At last, residual MFCCs are quantified and coded.

It can be seen that the connection between these two road modules lies only in MFCCs' predictive coding mode. From the perspective of encoder design, these two road signal processing (only at different sampling frequencies,) perhaps cause structural redundancies. In view of this, the structure of SVAC audio encoder has potential to be further optimized.

SVAC bandwidth expansion

As an enhancement technique for audio coding, even under the conditions of limited bit-rates, BWE can present high-frequency content with a very small amount of side information coded in front-end, and use part of low-frequency data combined with the side information to realize high-frequency reconstruction of signal, which further broadens the signal bandwidth of low bit-rate coding, and improves coding quality. BWE technology now has been employed in a variety of audio encoders. BWE in SVAC audio encoder transmits energy gain factors and 8-order linear predictive coding (LPC) coefficients, and they occupy 16 bits only in one frame after quantization. In audio decoding, high-frequency excitation signal is obtained by gain adjustment of low-frequency excitation signal, and then synthesis filter is designed based on the decoded 8-order LPC coefficients. At last, high-frequency signal is reconstructed and then full-band signal is obtained.

It can be seen that BWE in SVAC audio encoder is based on LPC coefficients, however the encoder also chooses MFCCs as its characteristic parameters. Both of them are widely used speech signal characteristic parameters. Recent studies have shown that the MFCCs have stronger correlation than LPC coefficients between high and low frequency of speech signals and the BWE technology based on MFCCs is superior to the current implementation scheme based on LPC coefficients.

Bandwidth expansion based on MFCCs

Firstly, we analyze the extraction steps of MFCCs. In order to be unified with SVAC audio encoder, we select speech signals whose frequency spectrums are in the range of 0 kHz ~ 8 kHz. Low-frequency is in 0 kHz ~ 4 kHz range, and highfrequency is in 4 kHz ~ 8 kHz range. Extraction steps are summarized briefly as follows:

a) Pre-emphasis: A single-pole high-pass filter is used to emphasize the highfrequency content. b) Windowing: A Hamming window is used to mitigate the edge effect of discontinuities between frames. c) Power spectrum estimation: Fast Fourier Transform(FFT) is applied to obtain the power spectrum; d) Mel-scale filters bank binning: MEL scale triangular filters are applied.

Record the number of low-pass filter with M, and the number of high-pass filter is denoted by N. The output energy of each MEL filter for lowfrequency is , and the output energy of each MEL filters

  0 1 k X k M    for high-frequency is ;   0 1 k Y k N   
e) Log operation: The outputs of MEL filters log-energies are obtained. f) Discrete Cosine Transform(DCT): DCT of the log-energies is applied to obtain the MFCCs as follows:

[1]         -1 0 -1 0 2 1 2 : log cos , 0 1 2 2 1 2 : log cos , 0 1 2 M n k k N n k k k n LF c X n M M M k n HF c Y n N N N                            
Where is the nth MFCC. Seen from the MFCCs extraction process above, two steps involve noninvertible loss of information; discarding phase information in step c) and the manyto-one mapping of the MEL filters in step d). And in the practical application of step f), such as speech recognition, also involves potential loss of information depending on whether the MFCCs vectors are truncated.

Assume that the MFCCs of high-frequency are under well preservation, so by Inverse DCT (IDCT) we can get the complete reconstruction of the energy k Y of MEL filters. However the evaluation for k Y in step d) is a many-to-one mapping, so the MEL scale power spectrum cannot be reconstructed precisely through k Y . Finer cepstral detail can, however, be obtained by interpolating from these log-energies of MFCCs by increasing the resolution of the IDCT as follows:

  -1 0 2 1 2 log cos , 0 1 2 N k n k k n Y c k iN N iN                  [2]
Where i is an interpolation factor, which is decided by the resolution of MEL-scale. For example, when N=6 and the MEL-scale resolution is 1, for the high-frequency ranges in 4 ~ 8 kHz, the calculation for i is:

    8 4 100 1 mel mel f kHz f kHz i N     [3] Where   mel f
is the conversion formula between MEL frequency and the actual linear frequency:

    10 2595log 1 700 mel Hz Hz f f f   [4]
Through exponential transformation of ˆk Y  from Mel frequency to linear frequency, we can acquire high-frequency power spectrum, and then with Inverse Fast Fourier Transform (IFFT) we get the autocorrelation coefficients of highfrequency sequence. Furthermore we use Levinson-Durbin iterative algorithm to obtain the solution of Yule-Walker equation, finally, the LPC coefficients are achieved. The generation of high-frequency excitation signal will not be discussed in this paper, and we use the technology defined in SVAC.

Improvement on BWE

SVAC audio encoder codes audio signals and MFCCs simultaneously. So obviously MFCCs-based BWE mentioned above can be adopted to replace the original BWE based on LPC coefficients.

For the sampling frequency converter in Figure 1, the output signal transferred to MFCCs coding module is sampled in 16 kHz, and the output signal transferred to audio coding module is sampled in 12.8kHz~38.4kHz range. So bandwidth of encoded audio signal is in 6.4 kHz ~19.2 kHz range, and the bandwidth of BWE is half of encoded signals. In SVAC audio coder, there are many coding levels, and Table 1 lists three levels from 1.0 to 1.2. Each level has two internal sampling frequencies. For example, when internal sampling frequency is 12.8kHz at level 1.0, high-frequency content of signal in 3.2 kHz ~6.4 kHz range is reconstructed by BWE and the maximal frequency is 6.4 kHz. At the same time, the signal sent to modules to extract and code MFCCs is sampled in 16 kHz, so its MFCCs extracted from high-frequency band can be used for high-frequency reconstruction. In this case, the maximal frequency reconstructed is 8 kHz higher than 6.4 kHz in the previous coder. So our optimization scheme is that the original BWE module can be removed completely when internal sampling frequency is lower than or equal to 16 kHz at low coding level because highfrequency reconstruction can be achieved from MFCCs.

Figure 2 is the framework of improved audio encoder for SVAC based on the above-mentioned idea. In this framework, sample frequency converter converts audio signal to a fixed 16 kHz sampling frequency. The converted signal is output to a low-pass filter (LP) and a high-pass filter (HP). The lowfrequency signal is encoded by audio coding module and MFCCs are extracted and coded from full band signal. At last, SVAC bit streams are multiplexed.

Figure 2. New block diagram for SVAC audio encoder

In decoder, the MFCCs of high-frequency signal decoded are converted to LPC coefficients to design the synthesis filter which is used to reconstruct the high-frequency content of original signal.

In this new SVAC audio encoder, BWE module is removed completely and the structure of encoder is simplified.

Simulation results

We compare our new encoder with SVAC audio encoder in simulation. 30 mono audio sequences are selected as experimental materials, including 18 male and female speech samples, 5 music samples and 7 abnormal events samples standardized in SVAC. Coding level is 1.0 with 3 different bit rates which are 10.8kbps, 17.2kbps and 24.4kbps respectively. Simulation concerns complexity and bit consumption, comparison of reconstructed LPC Coefficients, contrast of accuracy of reconstructed high-frequency band, and quality evaluation.

Analysis of complexity and bit consumption

Our encoder removes BWE module in SVAC and avoids calculation and quantization for gain factors and LPC coefficients, without introducing additional operations. So the computational complexity is reduced. The original encoder rebuilds LPC coefficients gained from inverse quantization and interpolation, and also decodes gain factors. However, the new decoder rebuilds LPC coefficients based on MFCCs. Their computational complexities are approximately equal. From the point of view of bit consumption, our encoder saves 16 bits consumption of BWE module in original SVAC, and the saved bits can be used for MFCCs coding or audio coding, which can increase the corresponding quantization accuracy and coding quality. The new encoder does not have to encode energy gain factors due to the energy information contained in MFCCs which namely are log-energies described above, so the new encoder saves bits again.

Here comes to the conclusion that our encoder achieves gains both on complexity and bit consumption.

Comparison of reconstructed LPC coefficients

In SVAC audio encoder, 8-order LPC coefficients of high band (4 kHz~8 kHz) are obtained and quantified. The dimensions of MFCCs in the new encoder is DIM (10, 6) which means 6 MFCCs are extracted from high band and quantified. The LPC coefficients are rebuilt based on these quantified MFCCs following the above method.

We compare these two sets of LPC coefficients with their real values and choose standard variance to describe error estimation. The definition is:

        2 1 , , M n lpc i n lpc i n i M       [5] In the formula above,   , lpc i n  is distorted value of LPC coefficient and   , lpc i n is its real value. Also, i (1 8 i  
) is the index of LPC coefficient, and n represents the frame index. M is the number of frames. 2000 frames of different samples are chosen in our simulation. Table 2 It can be seen from the table that compared to the original LPC coefficients, the error of reconstructed LPC coefficients in the new encoder is less than that in SVAC audio encoder. The main reason is that bit rates consumed by LPC coefficients in SVAC audio encoder are relatively less.

presents average   i  ( 1 8 i   ) in comparison. σ[1] σ[3] σ[5] σ[7] σ[2] σ[4] σ[6] σ[
Here comes to the conclusion that reconstruction of LPC coefficients has higher accuracy in the new encoder.

Comparison of accuracy of reconstructed high-frequency spectrum

Fig. 3 is an English female speech signal which is coded by both encoders. One frame is picked up to do comparison on high-frequency spectrum. In Figure 3, picture above is the frequency spectrum of original signal. The intermediate picture is spectrum of signals coded at level 1.0 when the internal sampling frequency is 12.8 kHz. In order to compare effectively, low-frequency part less than 4 kHz uses ACELP to encode, and frequency spectrum in 4 kHz~6.4 kHz range is reconstructed by BWE. Picture below is the reconstructed spectrum in our encoder in which low-frequency part under 4 KHz uses ACELP to encode and frequency spectrum in 4 kHz~8 kHz range is rebuilt based on MFCCs. We can see that two encoders have same performances at low-frequency band, but the new encoder broadens spectrum from 6.4 kHz to 8 kHz, especially this broadening is realized without increasing coding bit rates.

Here comes to the conclusion that the new encoder has higher precision in highfrequency reconstruction.

Quality evaluation

We performed MUSHRA experiments for the two encoders. Considering when the spectrum of music signals are below 8 kHz, human's hearing is affected significantly more than speech signals, we only select speech samples and some abnormal events samples in our subjective evaluation.

There are 7 listeners who have rich listening experiences. The experiment follows the MUSHRA method. In order to ensure the score at reasonable range, the original audio samples are hidden in all samples, and 3.5 kHz and 7.0 kHz low-pass filtered signals are added as hidden anchors.

Figure 4 presents score curves of two encoders at different bit rates. The original encoder reconstructs high-frequency below 6.4 kHz, and the new encoder below 8 kHz. Their curves are near the curve of 7.0 kHz anchor. But we can see that coding quality of the new encoder significantly exceeds the original one, and the average gain is about 3.63.

We can get the following conclusion that coding quality of the SVAC audio encoder is improved by the new scheme at same bit rates.

Conclusion

We propose an optimization scheme for SVAC audio encoder. We reconstruct high-frequency content of audio signal only dependent on those MFCCs extracted in front-end, and eliminate BWE module to simplify the encoder's structure, along with improvement on coding quality without increasing bit rates. Simulation results show that the new encoder achieves apparent gains in various aspects.

On the other hand, the optimization scheme only works effectively at coding level 1.0. When at higher level, BWE based on MFCCs cannot reconstruct spectrum higher than 8 kHz because the signal for MFCCs extracting is only sampled at 16 kHz. In fact, BWE module in original SVAC audio encoder cannot reconstruct highfrequency content with good quality also. For example, when audio signal is sampled at 19.2 kHz, high band from 9.6 kHz to 19.2 kHz is estimated dependent on 16 bits side information only, and the reconstruction quality is not satisfying. How to design BWE module more effectively at different coding levels for SAVC audio encoder is our future research direction.

Acknowledgment

The work is supported by 'the Fundamental Research Funds for the Central universities' of China (No.12CX04078A).

  Details of the derivation of MFCCs-based BWE are described as below.

Figure 3 .

 3 Figure 3. Reconstructed high-frequency spectrum in two encoders

Figure 4 .

 4 Figure 4. MUSHRA evaluation

Table 1 .

 1 Three coding levels in SVAC audio encoder

	Technical		Levels
	parameter	1.0	1.1	1.2
	internal sampling frequency(kHz)	12.8/16	24/25.6	32/38.4
	samples per frame	512	512	512
	maximum bitrates(bits/s)	24250	38800	58200

Table 2 .

 2 Error estimation of LPC coefficients

	8]

The authors would like to thank the anonymous reviewers for their constructive comments and corrections and the MUSHRA listening test participants for their effort.


Liying Lu

Xiaobo Lu

Saiping Ji

Chen Tong

A Traffic Camera Calibration Method Based On Multi-Rectangle Calibrating a camera using multi-rectangle constructed by mark lines in traffic road

Keywords: KEYW ORDS: distance detection, camera calibration, multi-rectangle, parameter modification

As distance detection is frequently needed in modern traffic management, camera calibration has a significant influence on the accuracy of distance detection. The traditional calibration methods usually need a calibration target, and the exact distance of calibration points has to be measured. In this paper, according to the camera imaging model, we put forward a calibration method based on multi-rectangle, which constructs several rectangles with the mark lines of the traffic road. Without measuring the internal or external parameters of the camera or the exact distance of calibration point, we only need the side lengths of rectangles and the image coordinates of the rectangular vertexes to establish the video image distance conversion model. For improving the accuracy of conversion, we use multiple rectangles to determine the coordinates of the vanishing points and modify the coordinates of the rectangular vertexes. Experimental results show that our method is more accurate when compared with the mainstream methods.

Introducti on

In modern traffic management, traffic video image processing is frequently used in the field of distance detection, speed detection and visibility detection. As an important part of traffic image processing, camera calibrat ion has a significant influence on the accuracy of detections which related to distance. Camera calibration means establishing the conversion model between the position of image pixel point and the position of actual point. According to the camera model, we get the camera parameters using some feature points of a real scene and these points' coordinates in the image. Finally, we build the conversion model between the image coordinates and the actual distance using the camera parameters [START_REF] Zheng | Computer Vision and Pattern Recognition[END_REF][START_REF] Hartley | Multiple view geometry in computer vision[END_REF] .

Traditional camera calibrat ion methods usually need some standard calibration targets, whose actual size has been accurately measured before calib rating. These methods use the corresponding relationship of image points and actual points to establish the constraint conditions of camera parameters, then calculate the parameters of camera by some nonlinear optimizat ion algorith m [START_REF] Zhang | A flexible new technique for camera calibration[END_REF][START_REF] Zhang | Camera calibration with one-dimensional objects[END_REF][START_REF] Ye | Study on the Camera Calibration Approach and Algorithm of Edge Detection and Contour Tracking[END_REF]. It is been proven that the calibration method based on vanishing point is effect ive and reliable, the position of vanishing point could b e determined by one-dimensional target of calibration targets [START_REF] Guillou | Using vanishing points for camera calibration and coarse 3D reconstruction from a single image[END_REF][START_REF] Yan | Camera Self-Calibration In Highway Dynamic Environment[END_REF]. Wei Geng and Yang Liu put forward a new algorith m based on single rectangle, which uses the mark lines in traffic road to calib rate the parameters of camera, then establish mutual conversion model between image coordinate system and the actual distance (Geng, 2012). The method uses the actual lengths of rectangular patterns and the corresponding informat ion of coordinates to establish detection model, without taking manual measurement to get camera internal and external parameters and the absolute distance of standard fixed points.

But under actual situation, as the mark lines may have been worn and the feature points are manual marked, that method may bring serious error. To solve this problem, a calibration algorith m based on mult i-rectangle is introduced in this paper, which constructs several rectangles with mark lines of the traffic road, then modif ies the Y-axis d irection vanishing point by fitting a straight line with mu ltiple points. In the X-axis d irect ion, n straight lines will generate intersection points, we choose the point with highest accuracy as the X-axis d irection vanishing point. To get mo re accurate calibration parameters, we use the position information of vanishing points and the accuracy of each rectangular vertex to mod ify the position of every rectangular vertex, then establish distance conversion model with these modified parameters. Through a lot of experiment, this method is more accurate than t he single-rectangle algorithm.

Calibration Method B ased On Multi-Rectangle

As the white mark lines and the gray road surface make the contrast ratio of the image not strong enough, and the mark lines may have been worn, it 's difficu lt to localize the position of feature points accurately and the calibration method based on single-rectangle is inclined to bring erro r. We study a parameter modification method in this paper to reduce the error. As shown in Figure 1, we can construct mu ltip le rectangles in a road surface image.

Modifying the coordinate of the vanishing point in Y-axis direction

The projection line of mark lines in image plane will intersect at point 2 Q , which is the vanishing point in Y-axis direction. Assume that we construct single rectangle with point 1 2 1 2

A A B B     , straight line 12 AA  and 12 BB  can be v iewed as the projection lines of mark lines, but error will be brought when any point is localized inaccurately. To reduce the error, we fit straight line A L with point 1 2 3 A A A   … using the least squares method, hence, A L can be viewed as the pro jection line in image plane of the left mark line. Then we fit the project ion line in image plane of the right mark line B L in the same way. Find the intersection point 2 Q of straight line A L and B L , so 2 Q is the vanishing point in Y-axis direct ion.

Modifying the coordinate of the vanishing point in X-axis direction

n ij k k ij d i j D ij            (1)

Modifying the coordinates of the rectangular vertex

Some feature points may have been inaccurately localized as we use mark lines to construct calibration target, so these coordinates must be modified.

To characterize the accuracy of point )

n kt t skq n kt t D E D      (2)
In the formu la, s could be a or b , 1 kn , 1 tn  , so sk represents a rectangular vertex, 1 max( )

n kt t D   is the largest value of accuracies on straight line ii AB  , 1
q means the current value is the accuracy in 1 Q direction. But

1 akq E equals 1 bkq E in 1
Q direction, wh ich means it's unable to distinguish the accuracy of i A and i B . So we have to find other straight lines in other direction, make As Figure 2(a) shows, every diagonal in the same direction parallels to each other, as an example, we choose a group of straight lines

1 (1 1) ii A B i n      , these
straight lines will intersect at a vanishing point 3 Q . The coordinate of 3 Q could be calculated in the same way as how we calculate the coordinate of 1 Q , then the

Figure 2. Feature point coordinate modification X Y 1 A 2 A 3 A 4 A 5 A n A 1 B 2 B 3 B 4 B 5 B n B ( ) a 3 Q 4 Q 1 Q k B A L B L k A 1 k A   1 k A        ( ) b k A  k B 
accuracy of i A and

1 i B   in 3 Q direction 3 skq E can
E E E E efc E efc E      (3)
In the formu la,

k ranges from 1 to n , 3 ( )=0 skq efc E when , s a k n  or ,1 s b k  ; 4 ( )=0 skq efc E when 1 s a k  , or s b k n  , , otherwise 3 ( )=1 skq efc E , 4 ( )=1
skq efc E .

After getting the accuracy of every feature point, we can modify the coordinate of feature points. We take point

Distance conversion model

Co mpared to the single-rectangle method, the mu lti-rectangle method make 1 Q , 2 Q and every rectangular vertexes modified, so we can get more accurate calibration parameters. O QQ . As y QQ parallels to X-axis, its projection line in image plane passes through 1 Q , so

y k k l d k k p    ,
where k d represents the distance between k P and 1 P , 2k p represents the reciprocal of the pixel-value differencing between point k P and 2 Q . As k ranges from 1 to n , we can get n equations, then we can establish a coordinate system with 1 () yk ld  -axis as vertical axis and 2k p -axis as horizontal axis, fit a straight line using the points we got in the equations, the slope of the straight line is 22 k . According to the relationship between 21 k and 22 k : 21

2 1 1 sin cos / d k k f    1 / (( ) ( ) ) x d x x y d y y l k p k f p u u v v l k p k f p u u v v                        (7)

Results And Analysis Of Experiment

Accuracy testing experiment

To evaluate the accuracy of the proposed method, we compare the effect of mu lti-rectangle method and the single-rectangle method through experiment. We mark six points in image that are corresponding to 21.00m to 214.13 m in actual road plane, then calcu late the distance of these points using the video image distance conversion model, and compare the results with the actual distance. As Table 1 shows, compared to the single-rectangle method, the proposed method has an improved measuring accuracy on each distance, and as the distance increases, the error of single -rectangle method increases fast, but the error of the proposed method remains in the range of 5%. In the study we found that the accuracy of vanishing point 1

Q and 2 Q have a major impact on the model parameters, for the proposed method, we use multip le rectangles to determine the position of vanishing point, so we could get more accurate vanishing point coordinate than the single-rectangle method.

Actual distance (m)

Single-rectangle method M ulti-rectangle method

Stability testing experiment

To evaluate the stability of the proposed method, we measure the maximu m error of the single-rectangle method and the multi-rectangle method in 10 different traffic images, the distance of each test point is less than 200 meters. 2 shows, the maximu m error of the mult i-rectangle method floats around 5%, while the maximu m error of the single-rectangle method floats around 10%. In addition, in the 4th and 7th image, the maximu m error of the singlerectangle method rise to 16.24% and 21.72% due to the mark line has been worn, while the maximu m error of the mu lti-rectangle is only 6.93% and 7.44%. Through this experiment, we can see the proposed method is more stable than the singlerectangle method.

Conclusion

This paper put forward a camera calibration algorithm based on multi -rectangle, which constructs mult iple rectangles with mark lines in actual traffic road, then modifies the calibration parameters and establish video image distance conversion model. We modify the coordinate of vanishing point in Y-axis d irection by fitting a straight line with mu ltip le rectangular vertexes, modify the coordinate of vanishing point in X-axis direction by choosing the point with highest accuracy among all intersection points, then we modify the position of every rectangular vertex, and establish the distance conversion model using the modified parameters. Co mpared to single-rectangle method, the proposed method provides more accurate calibrat ion parameters, and the distance conversion model we got has an imp rove accuracy. Experiment result shows that as distance increases, the detecting error increases too, but the effect of the proposed method is still better than the single-rectangle method.

However, this method still belong to the category of manual calibrat ion, the init ial feature points still needs to be manual marked, that would bring some unknown error and reduce the calibration accuracy. How to automatically localize the feature points, that's what we need to improve in further study.

Figure 1 .

 1 Figure 1. Construct multiple rectangles in a road surface image 1 A 2 A 3 A 4 A 5 A

  in P on straight line ii AB  , then calculate the normalized summation. Define the accuracy of any rectangular vertex in the 1 Q direction:

  straight lines, thus to separate the accuracy of i A and i B .

  examp le, the exact feature point k A , k B should be the intersection point of the straight lines which pass through 1 Q and straight line A L or B L , we mark them as square points in Figure 2(b) . The round dots in Figure 2(b) represents the manual marked feature points , we choose the point which has a smaller accuracy value as reference point, then connect it and 1 Q to construct the modified straight line kk AB   , so the intersection point of

Figure 3 .

 3 Figure 3. Calculating calibration parameters

Table 1 .

 1 Results for distance detection experimentA Traffic Camera Calibration M ethod Based On Multi-Rectangle 7

		Test value	relative	Test value	relative
		(m)	error	(m)	error
	21.00	20.25	3.55%	20.52	2.30%
	37.69	36.94	2.00%	36.97	1.91%
	62.41	59.59	4.52%	60.91	2.40%
	104.08	97.60	6.23%	100.82	3.13%
	160.47	147.83	7.88%	154.79	3.54%
	214.13	193.56	9.61%	205.52	4.02%

Table 2 .

 2 Results of stability testing experimentAs Table

	serial	M aximum error (single-	M aximum error (multi-
	number	rectangle method)	rectangle method)
	1	9.61%	4.02%
	2	12.37%	4.72%
	3	9.88%	5.14%
	4	16.24%	6.93%
	5	8.75%	4.12%
	6	10.03%	5.62%
	7	21.72%	7.44%
	8	10.94%	5.92%
	9	11.41%	5.37%
	10	9.18%	4.58%

Acknowledg ments

This work was supported by the National Natural Science Foundation of China (No.61374194) and Ch ina Postdoctoral Science Foundation Funded Project (No.2013M540405).