Nội dung

Vietnam J Comput Sci (2014) 1:29–37 DOI 10.1007/s40595-013-0002-5 REGULAR PAPER The paraconsistent process order control method Kazumi Nakamatsu · Jair M. Abe Received: 29 September 2013 / Accepted: 30 September 2013 / Published online: 9 November 2013 © The Author(s) 2013 Abstract We have already developed some kinds of paraconsistent annotated logic programs. In this paper we propose the paraconsistent process order control method based on a paraconsistent annotated logic program called before–after extended vector annotated logic program with strong negation (bf-EVALPSN) with a small example of pipeline process order verification. Bf-EVALPSN can deal with before–after relations between two processes (time intervals) in its annotations, and its reasoning system consists of two kinds of inference rules called the basic bf-inference rule and the transitive bf-inference rule. We introduce how the bf-EVALPSN-based reasoning system can be applied to the safety verification for process order. Keywords Paraconsistent annotated logic program · Before–after relation · Bf-EVALPSN · Process order control 1 Introduction A family of paraconsistent logic called annotated logics PT was proposed by da Costa et al. [4]. They can deal with inconsistency with many truth values called annotations, although the semantics of annotated logics is basically two valued. The K. Nakamatsu (B) School of Human Science and Environment, University of Hyogo, Shinzaike, Himeji 670-0092, Japan e-mail: nakamatu@shse.u-hyogo.ac.jp J. M. Abe ICET-Paulista University, São Paulo, SP, CEP 04026-022, Brazil J. M. Abe Institute of Advanced Studies, University of Sao Paulo, Cidade Universitaria, São Paulo, SP, CEP 05508-970, Brazil e-mail: jairabe@uol.com.br paraconsistent annotated logic has been developed from the viewpoint of logic programming [3], aiming at application to computer science. Furthermore, we have developed the paraconsistent annotated logic program to deal with inconsistency and some kinds of non-monotonic reasoning in a framework of annotated logic programming by using ontological (strong) negation and the stable model semantics [6], which is called annotated logic program with strong negation (ALPSN for short). Later, to deal with defeasible reasoning [14], we proposed a new version of ALPSN called vector annotated logic program with strong negation (VALPSN for short) and applied it to resolving conflicts [7]. Furthermore, we have extended VALPSN to deal with deontic notions (obligation, forbiddance, etc.) and named extended VALPSN (EVALPSN for short) [8,9]. We have shown that EVALPSN can deal with defeasible deontic reasoning and the safety verification for process control. Considering the safety verification for process control, there are many cases in which the safety verification for process order is significant. For example, suppose a pipeline network in which two kinds of liquids, nitric acid and caustic soda, are used for cleaning the pipelines. If those liquids are processed continuously and mixed in the same pipeline by accident, explosion by neutralization would be caused. To avoid such a dangerous accident, the safety for process order should be strictly verified in a formal way. However, it seems to be a little difficult to utilize EVALPSN for the safety verification of process order control different from that of process control. Therefore, we have developed EVALPSN toward treating before–after relations between time intervals and applied it to process order control [11], which has been named before–after (bf)-EVALPSN. The before–after relation reasoning system based on bf-EVALPSN consists of two groups of inference rules called the basic bf-inference rule and the transitive bf-inference rule. 123 30 The original ideas of treating such before–after relations in logic were proposed for developing practical planning and natural language understanding systems by Allen [1] and Allen and Ferguson [2]. In his logic, before–after relations between two time intervals are represented in some special predicates and treated in a framework of first-order temporal logic. On the other hands, in bf-EVALPSN, before–after relations between two time intervals are regarded as paraconsistency between before and after degrees, and they can be represented more minutely in vector annotations of a special literal R( pi , p j , t) representing the before–after relation between two processes (time intervals) at time t. Bf-EVALPSN-based before–after relation reasoning system consists of two kinds of efficient inference rules called the basic bf-inference rule and the transitive bf-inference rule that can be implemented as a bf-EVALPSN. This paper is organized as follows: in Sect. 2, EVALPSN is reviewed briefly; in Sect. 3, bf-EVALPSN is formally defined and its simple reasoning example is introduced; in Sect. 4, the bf-EVALPSN reasoning system consisting of two kinds of inference rules is defined and explained in detail with some examples; in Sect. 5, the paraconsistent process order control method based on bf-EVALPSN reasoning is introduced with a small example of pipeline process order control; lastly, we conclude this paper. Vietnam J Comput Sci (2014) 1:29–37 Fig. 1 Lattice Tv (2) and lattice Td The ordering (d ) of Td is described by the Hasse’s diagram in Fig. 1. The intuitive meaning of each member of Td is ⊥(unknown), α(fact), β(obligation), γ (non-obligation), ∗1 (fact and obligation), ∗2 (obligation and non-obligation) and ∗3 (fact and non-obligation), (inconsistency). Then, the complete lattice Te (n) of extended vector annotations is defined as the product, Tv (n) × Td . The ordering (e ) of Te (n) is defined: let [(i 1 , j1 ), μ1 ], [(i 2 , j2 ), μ2 ] ∈ Te , [(i 1 , j1 ), μ1 ] e [(i 2 , j2 ), μ2 ] iff (i 1 , j1 ) v (i 2 , j2 ) and μ1 d μ2 . There are two kinds of epistemic negations (¬1 and ¬2 ) in EVALPSN, both of which are defined as mappings over Tv (n) and Td , respectively. Definition 1 (epistemic negations ¬1 and ¬2 in EVALPSN) ¬1 ([(i, j), μ]) = [( j, i), μ], ∀μ ∈ Td , 2 Annotated logic program EVALPSN In this section, we review EVALPSN briefly [9]. Generally, a truth value called an annotation is explicitly attached to each literal in annotated logic programs [3]. For example, let p be a literal and μ an annotation, then p : μ is called an annotated literal. The set of annotations constitutes a complete lattice. An annotation in EVALPSN has a form of [(i, j), μ] called an extended vector annotation. The first component (i, j) is called a vector annotation and the set of vector annotations constitutes the complete lattice, Tv (n) = {(x, y) | 0 ≤ x ≤ n, 0 ≤ y ≤ n, x, y, n are integers} in Fig. 1. The ordering (v ) of Tv (n) is defined as: let (x1 , y1 ) , (x2 , y2 ) ∈ Tv (n), (x1 , y1 ) v (x2 , y2 ) iff x1 ≤ x2 and y1 ≤ y2 . For each extended vector annotated literal p : [(i, j), μ], the integer i denotes the amount of positive information to support the literal p and the integer j denotes that of negative one. The second component μ is an index of fact and deontic notions such as obligation, and the set of the second components constitutes the complete lattice, Td = {⊥, α, β, γ , ∗1 , ∗2 , ∗3 , }. 123 ¬2 ([(i, j), ⊥]) = [(i, j), ⊥], ¬2 ([(i, j), α]) = [(i, j), α], ¬2 ([(i, j), β]) = [(i, j), γ ], ¬2 ([(i, j), γ ]) = [(i, j), β], ¬2 ([(i, j), ∗1 ]) = [(i, j), ∗3 ], ¬2 ([(i, j), ∗2 ]) = [(i, j), ∗2 ], ¬2 ([(i, j), ∗3 ]) = [(i, j), ∗1 ], ¬2 ([(i, j), ]) = [(i, j), ]. If we regard the epistemic negations as syntactical operations, the epistemic negations followed by literals can be eliminated by the syntactical operations. For example, ¬1 ( p : [(2, 0), α]) = p : [(0, 2), α] and ¬2 (q : [(1, 0), β]) = p : [(1, 0), γ ]. There is another negation called strong negation (∼) in EVALPSN, and it is treated as well as classical negation [4]. Definition 2 (strong negation ∼) Let F be any formula and ¬ be ¬1 or ¬2 . ∼ F =def F → ((F → F) ∧ ¬(F → F)). Definition 3 (well-extended vector annotated literal) Let p be a literal. p : [(i, 0), μ] and p : [(0, j), μ] are called well-extended vector annotated literals, where i, j are non-negative integers and μ ∈ {α, β, γ }. Definition 4 (EVALPSN) If L 0 , . . . , L n are weva-literals, L 1 ∧ . . . ∧ L i ∧ ∼ L i+1 ∧ . . . ∧ ∼ L n → L 0 Vietnam J Comput Sci (2014) 1:29–37 31 Fig. 2 Before (be)/after (af) and disjoint before (db)/after (da) is called an EVALPSN clause. An EVALPSN is a finite set of EVALPSN clauses. Here, we comment that if the annotations α and β represent fact and obligation, notions “fact”, “obligation”, “forbiddance” and “permission” can be represented by extended vector annotations, [(m, 0), α] , [(m, 0), β], [(0, m), β], and [(0, m), γ ], respectively, in EVALPSN, where m is a nonnegative integer. 3 Before–after EVALPSN In this section, we review bf-EVALPSN. The details are found in [12,13]. In bf-EVALPSN, a special annotated literal R( pm , pn , t) : [(i, j), μ] called bf-literal whose non-negative integer vector annotation (i, j) represents the before–after relation between processes Pr m and Pr n at time t is introduced. The integer components i and j of the vector annotation (i, j) represent the after and before degrees between processes Pr m ( pm ) and Pr n ( pn ), respectively, and before–after relations are represented paraconsistently in vector annotations. Definition 5 (bf-EVALPSN) An extended vector annotated literal, R( pi , p j , t) : [(i, j), μ] is called a bf-EVALP literal or a bf-literal for short, where (i, j) is a vector annotation and μ ∈ {α, β, γ }. If an EVALPSN clause contains bf-EVALP literals, it is called a bf-EVALPSN clause or just a bf-EVALP clause if it contains no strong negation. A bf-EVALPSN is a finite set of bf-EVALPSN clauses. We provide a paraconsistent before–after interpretation for vector annotations representing bf-relations in bfEVALPSN, and such a vector annotation is called a bfannotation. Exactly speaking, there are 15 kinds of bf-relation according to before–after order between four start/finish times of two processes. Before (be)/after (af) is defined according to the bfrelation between each start time of the two processes. If one process has started before/after another one starts, then the bfrelations between them are defined as “before/after”, which are represented in the left in Fig. 2. We introduce other kinds of bf-relations as well as before (be)/after (af). Disjoint before (db)/after (da) is defined as having a time lag between the earlier process finish time and the later one’s start time; this is described on the right in Fig. 2. Immediate before (mb)/after (ma) is defined as having no time lag between the earlier process finish time and the later one’s start time; it is described on the left in Fig. 3. Joint before (jb)/after (ja) is defined as two processes that overlap, where the earlier process had finished before the later one finished; it is described on the right in Fig. 3. S-included before (sb)/S-included after (sa) is defined as two processes, where one had started before the other started, but finished at the same time; it is described on the left in Fig. 4. Included before (ib)/after (ia) is defined as two processes, where one had started/finished before/after another one started/finished; it is described on the right in Fig. 4. F-included before (fb)/after (fa) is defined as two processes that started at the same time, but with one finishing before another one finished; it is described in the left in Fig. 5. Paraconsistent before–after (pba) is defined as having two processes that started at the same time and also finished at the same time; it is described on the right in Fig. 5. The epistemic negation over bf-annotations, be, af, db, da, mb, ma, jb, ja, ib, ia, sb, sa, fb, fa and pba is defined and the complete lattice of bf-annotations is shown in Fig. 6. Fig. 3 Immediate before (mb)/after (ma) and joint before (jb)/after (ja) Fig. 4 S-included before (sb)/after (sa) and included before (ib)/ after (ia) Fig. 5 F-included before (fb)/after (fa) and paraconsistent before– after (pba) 123 32 Vietnam J Comput Sci (2014) 1:29–37 First of all, we introduce a group of basic bf-inference rules to be applied at the initial stage (time t0 ), which are named (0, 0)-rules. (0,0)-rules Suppose that no process has started yet and the vector annotation of bf-literal R( pi , p j , t) is (0, 0), which shows that there is no knowledge in terms of the bf-relation between processes Pri and Pr j , then the following two basic bf-inference rules are applied at the initial stage. Fig. 6 The complete lattice Tv (12)bf for bf-annotations (0,0)-rule-1 If process Pri started before process Pr j starts, then the vector annotation (0, 0) of bf-literal R( pi , p j , t) should turn to be(0, 8), which is the greatest lower bound of the set, {db(0, 12), mb(1, 11), jb(2, 10), sb(3, 9), ib(4, 8)}. (0,0)-rule-2 If both processes Pri and Pr j have started at the same time, then it is reasonably anticipated that the bfrelation between processes Pri and Pr j will be one of the bf-annotations, {fb(5, 7), pba(6, 6), fa(7, 5)} whose greatest lower bound is (5, 5) (refer to Fig. 6). Therefore, the vector annotation (0, 0) of bf-literal R( pi , p j , t) should turn to (5, 5). Definition 6 (epistemic negation ¬1 for bf-annotations) The epistemic negation ¬1 over the bf-annotations is obviously defined as the following mappings: (0, 0)-rule-1 and (0, 0)-rule-2 are translated into the bfEVALPSN, ¬1 (af) = be, ¬1 (be) = af, ¬1 (da) = db, R( pi , p j , t) : [(0, 0), α] ∧ st( pi , t) : [t, α] ¬1 (db) = da, ¬1 (ma) = mb, ¬1 (mb) = ma, ¬1 (ja) = jb, ¬1 (jb) = ja, ¬1 (sa) = sb, ¬1 (sb) = sa, ¬1 (ia) = ib, ¬1 (ib) = ia, ¬1 (fa) = fb, ¬1 (fb) = fa, ¬1 (pba) = pba. Therefore, each bf-annotation can be translated into vector annotations as bf = (0, 8), db = (0, 12), mb = (1, 11), jb = (2, 10), sb = (3, 9), ib = (4, 8), fb = (5, 7) and pba = (6, 6). 4 Reasoning system in bf-EVALPSN To represent the basic bf-inference rule in bf-EVALPSN, we newly introduce two literals: st( pi , t), which is interpreted as process Pri starts at time t, and fi( pi , t), which is interpreted as process Pri finishes at time t. Those literals are used for expressing process start/finish information and may have one of the vector annotations, {⊥(0, 0), t(1, 0), f(0, 1), (1, 1)}, where annotations t(1, 0) and f(0, 1) can be intuitively interpreted as “true” and “false”, respectively. 123 ∧ ∼ st( p j , t) : [t, α] → R( pi , p j , t) : [(0, 8), α] (1) R( pi , p j , t) : [(0, 0), α] ∧ st( pi , t) : [t, α] ∧ st( p j , t) : [t, α] → R( pi , p j , t) : [(5, 5), α] (2) Suppose that (0, 0)-rule-1 or 2 has been applied, then the vector annotation of bf-literal R( pi , p j , t) should be one of (0, 8) or (5, 5). Therefore, we need to consider two groups of basic bf-inference rules to be applied for following (0, 0)rule-1 and 2, which are named (0,8)-rules and (5,5)-rules, respectively. (0,8)-rules Suppose that process Pri has started before process Pr j starts, then the vector annotation of bf-literal R( pi , p j , t) should be (0, 8). We have the following inference rules to be applied for following (0, 0)-rule-1. (0,8)-rule-1 If process Pri has finished before process Pr j starts, and process Pr j starts immediately after process Pri finished, then the vector annotation (0, 8) of bf-literal R( pi , p j , t) should turn to mb(1, 11). (0,8)-rule-2 If process Pri has finished before process Pr j starts, and process Pr j has not started immediately after process Pri finished, then the vector annotation (0, 8) of bf-literal R( pi , p j , t) should turn to db(0, 12). (0,8)-rule-3 If process Pr j starts before process Pri finishes, then the vector annotation (0, 8) of bf-literal R( pi , p j , t) should turn to (2, 8) that is the greatest lower bound of the set, {jb(2, 10), sb(3, 9), ib(4, 8)}. Vietnam J Comput Sci (2014) 1:29–37 33 (0, 8)-rule-1, 2 and 3 are translated into the bf-EVALPSN, R( pi , p j , t) : [(0, 8), α] ∧ fi( pi , t) : [t, α] ∧ st( p j , t) : [t, α] → R( pi , p j , t) : [(1, 11), α] (3) R( pi , p j , t) : [(0, 8), α] ∧ fi( pi , t) : [t, α] ∧ ∼ st( p j , t) : [t, α] → R( pi , p j , t) : [(0, 12), α] (4) R( pi , p j , t) : [(0, 8), α]∧ ∼ fi( pi , t) : [t, α] ∧ st( p j , t) : [t, α] → R( pi , p j , t) : [(2, 8), α] (5) has been applied, no bf-annotation could be derived. Therefore, a group of basic bf-inference rules named (2, 8)-rules should be considered for following (0, 8)-rule-3. (2,8)-rules Suppose that process Pri has started before process Pr j starts and process Pr j has started before process Pri finishes, then the vector annotation of bf-literal R( pi , p j , t) should be (2, 8) and the following three rules should be considered. (2,8)-rule-1 If process Pri finished before process Pr j finishes, then the vector annotation (2, 8) of bf-literal R( pi , p j , t) should turn to jb(2, 10). (2,8)-rule-2 If both processes Pri and Pr j have finished at the same time, then the vector annotation (2, 8) of bfliteral R( pi , p j , t) should turn to fb(3, 9). (2,8)-rule-3 If process Pr j has finished before Pri finishes, then the vector annotation (2, 8) of bf-literal R( pi , p j , t) should turn to ib(4, 8). (5,5)-rules Suppose that both processes Pri and Pr j have already started at the same time, then the vector annotation of bf-literal R( pi , p j , t) should be (5, 5). We have the following inference rules to be applied for following (0, 0)rule-2. (5,5)-rule-1 If process Pri has finished before process Pr j finishes, then the vector annotation (5, 5) of bf-literal R( pi , p j , t) should turn to sb(5, 7). (5,5)-rule-2 If both processes Pri and Pr j have finished at the same time, then the vector annotation (5, 5) of bfliteral R( pi , p j , t) should turn to pba(6, 6). (5,5)-rule-3 If process Pr j has finished before process Pri finishes, then the vector annotation (5, 5) of bf-literal R( pi , p j , t) should turn to sa(7, 5). Basic bf-inference rules (5, 5)-rule-1, 2 and 3 are translated into the bf-EVALPSN, Basic bf-inference rules (2, 8)-rule-1, 2 and 3 are translated into the bf-EVALPSN, R( pi , p j , t) : [(2, 8), α] ∧ fi( pi , t) : [t, α] ∧ ∼ fi( p j , t) : [t, α] → R( pi , p j , t) : [(2, 10), α] R( pi , p j , t) : [(2, 8), α] ∧ fi( pi , t) : [t, α] ∧ fi( p j , t) : [t, α] → R( pi , p j , t) : [(3, 9), α] ∧ fi( p j , t) : [t, α] → R( pi , p j , t) : [(4, 8), α] (6) R( pi , p j , t) : [(5, 5), α] ∧ fi( pi , t) : [t, α] ∧ fi( p j , t) : [t, α] → R( pi , p j , t) : [(6, 6), α] (7) R( pi , p j , t) : [(5, 5), α] ∧ ∼ fi( pi , t) : [t, α] ∧ fi( p j , t) : [t, α] → R( pi , p j , t) : [(7, 5), α] (8) If one of (0, 8)-rule-1,2, (5, 5)-rule-1,2 and 3 has been applied, a final bf-annotation such as jb(2, 10) between two processes should be derived. However, even if (0, 8)-rule-3 Table 1 Application orders of basic bf-inference rules Vector annotation (10) R( pi , p j , t) : [(2, 8), α] ∧ ∼ fi( pi , t) : [t, α] R( pi , p j , t) : [(5, 5), α] ∧ fi( pi , t) : [t, α] ∧ ∼ fi( p j , t) : [t, α] → R( pi , p j , t) : [(5, 7), α] Rule Rule-1 (11) The application orders of all basic bf-inference rules are summarized in Table 1. Now, we introduce the transitive bf-inference rule, which can reason a vector annotation of bf-literal transitively. Suppose that there are three processes Pri , Pr j and Pr k starting sequentially, then we consider deriving the vector annotation of bf-literal R( pi , pk , t) from those of bf-literals R( pi , p j , t) and R( p j , pk , t) transitively. We describe only the variation of vector annotations in the following rules. Vector annotation Rule Vector annotation Rule-1 (0, 12) Rule-2 (1, 11) Rule-3 (2, 8) Rule-1 (5, 7) (0, 8) (0, 0) Rule-2 (9) (5, 5) Rule-2 (6, 6) Rule-3 (7, 5) Rule Vector annotation Rule-1 (2, 10) Rule-2 (3, 9) Rule-3 (4, 8) 123 34 Vietnam J Comput Sci (2014) 1:29–37 of the rules TR1-1, TR1-2, . . . or TR1-5 should be applied at the following stage; and if the rule TR1-4 has been applied after the rule TR1, one of the rules TR1-4-1, TR1-4-2, . . . or TR1-4-7 should be applied at the following stage; on the other hand, if one of the rules TR1-1, TR1-2 or TR1-3 has been applied after the rule TR1, there should be no transitive bf-inference rule to be applied at the following stage because one of bf-relations db(0, 12), mb(1, 11) has been derived. Note (II) Transitive bf-inference rules, Transitive bf-inference rules TR0 (0, 0) ∧ (0, 0) → (0, 0) TR1 (0, 8) ∧ (0, 0) → (0, 8) TR1-1 (0, 12) ∧ (0, 0) → (0, 12) TR1-2 (1, 11) ∧ (0, 8) → (0, 12) TR1-3 (1, 11) ∧ (5, 5) → (1, 11) TR1-4 (2, 8) ∧ (0, 8) → (0, 8) TR1-4-1 (2, 10) ∧ (0, 8) → (0, 12) TR1-4-2 (4, 8) ∧ (0, 12) → (0, 8) (12) TR1-4-3 (2, 8) ∧ (2, 8) → (2, 8) (13) TR1-4-3-3 (2, 8) ∧ (4, 8) → (4, 8) TR1-4-3-4 (3, 9) ∧ (2, 10) → (2, 10) TR1-4-3-5 (2, 10) ∧ (4, 8) → (3, 9) TR1-4-3-6 (4, 8) ∧ (3, 9) → (4, 8) (14) TR1-4-3-7 (3, 9) ∧ (3, 9) → (3, 9) TR1-4-4 (3, 9) ∧ (0, 12) → (0, 12) TR1-4-5 (2, 10) ∧ (2, 8) → (1, 11) TR1-4-6 (4, 8) ∧ (1, 11) → (2, 8) TR1-4-7 (3, 9) ∧ (1, 11) → (1, 11) TR1-5 (2, 8) ∧ (5, 5) → (2, 8) TR1-5-1 (4, 8) ∧ (5, 7) → (2, 8) TR1-5-1 (15), TR2-2 TR2-5 TR1-4-3-1 (2, 10) ∧ (2, 8) → (2, 10) TR1-4-3-2 (4, 8) ∧ (2, 10) → (2, 8) TR1-4-2 (12), TR1-4-3-2 (13), TR1-4-6 (14), (18), TR3-1 (16), TR2-3-2 (17), (19) have no following rule to be applied, even though they cannot derive the final bf-relations between processes represented by bf-annotations such as jb(2, 10). For example, suppose that the rule TR1-4-3-2 has been applied, then vector annotation (2, 8) of bf-literal ( pi , pk , t) just indicates that the final bf-relation between processes Pri and Pr k is represented by one of three bf-annotations, jb(2, 10), sb(3, 9) or ib(4, 8) because vector annotation (2, 8) is the greatest lower bound of those bf-annotations. Therefore, if one of transitive bfinference rules (12),(13),(14),(15),(16), (17),(18) and (19), has been applied, one of (0, 8)-rule, (2, 8)-rule or (5, 5)-rule should be applied for deriving the final bf-annotation at the following stage. For example, if the rule TR1-4-3-2 has been applied, (2, 8)-rule should be applied at the following stage. (15) TR1-5-2 (2, 8) ∧ (7, 5) → (4, 8) 5 The process order control method in bf-EVALPSN TR1-5-3 (3, 9) ∧ (5, 7) → (2, 10) In this section, we present the process order control method with a simple example for pipeline process order verification. The process order control method has the following three steps: TR1-5-4 (2, 10) ∧ (7, 5) → (3, 9) TR2 (5, 5) ∧ (0, 8) → (0, 8) TR2-1 (5, 7) ∧ (0, 8) → (0, 12) TR2-2 (7, 5) ∧ (0, 12) → (0, 8) (16) TR2-3 (5, 5) ∧ (2, 8) → (2, 8) TR2-3-1 (5, 7) ∧ (2, 8) → (2, 10) TR2-3-2 (7, 5) ∧ (2, 10) → (2, 8) (17) TR2-3-3 (5, 5) ∧ (4, 8) → (4, 8) TR2-3-4 (7, 5) ∧ (3, 9) → (4, 8) TR2-4 (5, 7) ∧ (2, 8) → (1, 11) TR2-5 (7, 5) ∧ (1, 11) → (2, 8) (18) TR3 (5, 5) ∧ (5, 5) → (5, 5) TR3-1 (7, 5) ∧ (5, 7) → (5, 5) (19) TR3-2 (5, 7) ∧ (7, 5) → (6, 6) Note (I) The name of a transitive bf-inference rule such as TR1-4-3 indicates the application sequence of transitive bfinference rules until the transitive bf-inference rule has been applied. For example, if the rule TR1 has been applied, one 123 Step 1 translate the safety properties of the process order control system into bf-EVALPSN; Step 2 verify if permission for starting the process can be derived from the bf-EVALPSN in step1 by the basic bf-inference rule and the transitive bf-inference rule or not. The verification step 2 can be carried out not only just before starting the process, but also at any time. We assume a pipeline system consisting of two pipelines, PIPELINE-1 and 2, which deal with pipeline processes Pr 0 , Pr 1 , Pr 2 and Pr 3 . The process schedule of those processes are shown in Fig. 7. Moreover, we assume that the pipeline system has four safety properties SPR -i(i = 0, 1, 2, 3). S P R-0 process Pr 0 must start before any other processes, and process Pr 0 must finish before process Pr 2 finishes, Vietnam J Comput Sci (2014) 1:29–37 35 PIPELINE-1 PIPELINE-2 Fig. 7 Pipeline process schedule S P R-1 process Pr 1 must start after process Pr 0 starts, S P R-2 process Pr 2 must start immediately after process Pr 1 finishes, S P R-3 process Pr 3 must start immediately after processes Pr 0 and Pr 2 finish. where bf-EVALPSN clause (27) declares that if process Pr 1 has not finished before process Pr 2 starts, it should be forbidden from starting process Pr 2 ; the vector annotation (11, 0) of bf-literal R( p2 , p1 , t) is the greatest lower bound of {da(12, 0), ma(11, 1)}, which implies that process Pr 1 has finished before process Pr 2 starts; bf-EVALPSN clauses (28)/(30) declare that if there is no forbiddance from starting/finishing process Pr 2 , it should be permitted to start/finish process Pr 2 , respectively; and bf-EVALPSN clauses (29) declare that if process Pr 0 has not finished before process Pr 2 finishes, it should be forbidden from finishing process Pr 2 . SPR-3 ∼ R( p3 , p0 , t) : [(11, 0), α] → st( p3 , t) : [f, β], Step 1 All safety properties SPR-i(i = 0, 1, 2, 3) can be translated into the following bf-EVALPSN clauses. (20) ∼ R( p0 , p2 , t) : [(0, 8), α] → st( p2 , t) : [f, β], (21) ∼ R( p0 , p3 , t) : [(0, 8), α] → st( p3 , t) : [f, β], (22) st( p1 , t) : [f, β] ∧ st( p2 , t) : [f, β] ∼ fi( p0 , t) : [f, β] → fi( p0 , t) : [f, γ ], (23) (24) where bf-EVALPSN clauses (20), (21) and (22) declare that if process Pr 0 has not started before other processes Pri (i = 1, 2, 3) start, it should be forbidden from starting each process Pri (i = 1, 2, 3); bf-EVALPSN clause (23) declares that if each process Pri (i = 1, 2, 3) is forbidden from starting, it should be permitted to start process Pr 0 ; and bf-EVALPSN clause (24) declares that if there is no forbiddance from finishing process Pr 0 , it should be permitted to finish process Pr 0 . SPR-1 ∼ st( p1 , t) : [f, β] → st( p1 , t) : [f, γ ], (25) ∼ fi( p1 , t) : [f, β] → fi( p1 , t) : [f, γ ], (26) where bf-EVALPSN clause (25)/(26) declares that if there is no forbiddance from starting/finishing process Pr 1 , it should be permitted to start/finish process Pr 1 , respectively. SPR-2 ∼ R( p2 , p1 , t) : [(11, 0), α] → st( p2 , t) : [f, β], (27) ∼ st( p2 , t) : [f, β] → st( p2 , t) : [f, γ ], (28) ∼ R( p2 , p0 , t) : [(10, 2), α] → fi( p2 , t) : [f, β], (29) ∼ fi( p2 , t) : [f, β] → fi( p2 , t) : [f, γ ], ∼ R( p3 , p1 , t) : [(11, 0), α] → st( p3 , t) : [f, β], (32) SPR-0 ∼ R( p0 , p1 , t) : [(0, 8), α] → st( p1 , t) : [f, β], ∧ st( p3 , t) : [f, β] → st( p0 , t) : [f, γ ], (31) (30) ∼ R( p3 , p2 , t) : [(11, 0), α] → st( p3 , t) : [f, β], (33) ∼ st( p3 , t) : [f, β] → st( p3 , t) : [f, γ ], (34) ∼ fi( p3 , t) : [f, β] → fi( p3 , t) : [f, γ ], (35) where bf-EVALPSN clauses (31), (32) and (33) declare that if one of processes Pri (i = 0, 1, 2) has not finished yet, it should be forbidden from starting process Pr 3 ; and bfEVALPSN clauses (34)/(35) declare that if there is no forbiddance from starting/finishing process Pr 3 , it should be permitted to start/finish process Pr 3 , respectively. Step 2 Here, we show how the bf-EVALPSN process order safety verification is carried out at five time points, t0 , t1 , t2 , t3 and t4 in the process schedule (Fig. 7). We consider five bf-relations between processes Pr 0 , Pr 1 , Pr 2 and Pr 3 , represented by the vector annotations of bf-literals, R( p0 , p1 , t), R( p0 , p2 , t), R( p0 , p3 , t), R( p1 , p2 , t), R( p2 , p3 , t) which should be verified based on safety properties SPR-0, 1, 2 and 3 in real time. Initial stage (at time t0 ) no process has started at time t0 , thus, the bf-EVALP clauses, R( p0 , p1 , t0 ) : [(0, 0), α], (36) R( p1 , p2 , t0 ) : [(0, 0), α], (37) R( p2 , p3 , t0 ) : [(0, 0), α] (38) R( p0 , p2 , t0 ) : [(0, 0), α], (39) R( p0 , p3 , t0 ) : [(0, 0), α] (40) are obtained by transitive bf-inference rule TR0; then, bf-EVALP clauses (36), (39) and (40) satisfy each body of bf-EVALPSN clauses (20), (21) and (22), respectively; therefore, the forbiddance, 123 36 Vietnam J Comput Sci (2014) 1:29–37 st( p1 , t0 ) : [f, β], (41) st( p2 , t0 ) : [f, β], (42) st( p3 , t0 ) : [f, β] (43) from starting each process Pri (i = 1, 2, 3) is derived. Moreover, since bf-EVALP clauses (41), (42) and (43) satisfy the body of bf-EVALPSN clause (23), the permission for starting process Pr 0 , st( p0 , t0 ) : [f, γ ] are derived by basic bf-inference rules (2, 8)-rule-3, (0, 8)rule-2 and (0, 0)-rule-1, respectively. Moreover, the bfEVALP clauses, R( p0 , p2 , t2 ) : [(2, 8), α], R( p0 , p3 , t2 ) : [(0, 12), α] are obtained by transitive bf-inference rules TR1-4-6 and TR1-2, respectively. Then, since bf-EVALP clause (51) does not satisfy the body of bf-EVALPSN clause (27), the forbiddance from starting process Pr 2 , is derived; therefore, process Pr 0 is permitted to start at time t0 . st( p2 , t2 ) : [f, β] 2nd Stage (at time t1 ) process Pr 0 has already started but all other processes Pri (i = 1, 2, 3) have not started yet; then the bf-EVALP clauses, cannot be derived. Since there is no forbiddance (53), it satisfies the body of bf-EVALPSN clause (28), and the permission for starting process Pr 2 , R( p0 , p1 , t1 ) : [(0, 8), α], (44) R( p1 , p2 , t1 ) : [(0, 0), α], (45) R( p2 , p3 , t1 ) : [(0, 0), α] (46) are obtained, where the bf-EVALP clause (44) is derived by basic bf-inference rule (0, 0)-rule-1. Moreover, the bfEVALP clauses, R( p0 , p2 , t1 ) : [(0, 8), α], (47) R( p0 , p3 , t1 ) : [(0, 8), α] (48) are obtained by transitive bf-inference rule TR1; as bfEVALP clause (44) does not satisfy the body of bf-EVALPSN clause (20), the forbiddance from starting process Pr 1 , st( p1 , t1 ) : [f, β] (49) cannot be derived. Then, since there is no forbiddance (49), the body of bf-EVALPSN clause (25) is satisfied and the permission for starting process Pr 1 , st( p1 , t1 ) : [f, γ ] is derived. On the other hand, since bf-EVALP clauses (47) and (48) satisfy the body of bf-EVALPSN clauses (27) and (31), respectively, the forbiddance from starting both processes Pr 2 and Pr 3 , st( p2 , t1 ) : [f, β], st( p3 , t1 ) : [f, β] are derived; therefore, process Pr 1 is permitted to start at time t1 . 3rd Stage (at time t2 ) process Pr 1 has just finished and process Pr 0 has not finished yet; then, the bf-EVALP clauses, R( p0 , p1 , t2 ) : [(4, 8), α], (50) R( p1 , p2 , t2 ) : [(1, 11), α], (51) R( p2 , p3 , t2 ) : [(0, 8), α] (52) 123 (53) st ( p2 , t2 ) : [f, γ ] is derived. On the other hand, since bf-EVALP clause (53) satisfies the body of bf-EVALPSN clause (31), the forbiddance from starting process Pr 3 , t ( p3 , t2 ) : [f, β] is derived; therefore, process Pr 2 is permitted to start. However, process Pr 3 is still forbidden from starting at time t2 . 4th Stage (at the t3 ) process Pr 0 has finished, process Pr 2 has not finished yet, and process Pr 3 has not started yet; then, the bf-EVALP clauses, R( p0 , p1 , t3 ) : [(4, 8), α], (54) R( p1 , p2 , t3 ) : [(1, 11), α], (55) R( p2 , p3 , t3 ) : [(0, 8), α] (56) in which the vector annotations are the same as in the previous stage are obtained because bf-annotations of bf-EVALP clauses (54) and (55) have been already reasoned, and the before–after relation between processes Pr 2 and Pr 3 is the same as in the previous stage. Moreover, the bf-EVALP clauses, R( p0 , p2 , t3 ) : [(2, 10), α], (57) R( p0 , p3 , t3 ) : [(0, 12), α] (58) are obtained, where bf-EVALP clause (57) is derived by basic bf-inference rule (2, 8)-rule-1. Then, bf-EVALP clause (57) satisfies the body of bf-EVALP clause (33), and the forbiddance from starting process Pr 3 , S( p3 , t3 ) : [f, β] is derived. Therefore, process Pr 3 is still forbidden from starting because process Pr 2 has not finished yet at time t3 . 5th Stage (at time t4 ) process Pr 2 has just finished and process Pr 3 has not started yet; then, the bf-EVALP clauses, Vietnam J Comput Sci (2014) 1:29–37 37 R( p0 , p1 , t4 ) : [(4, 8), α], (59) R( p1 , p2 , t4 ) : [(1, 11), α], (60) R( p2 , p3 , t4 ) : [(1, 11), α], (61) R( p0 , p2 , t4 ) : [(2, 10), α], (62) R( p0 , p3 , t4 ) : [(0, 12), α] (63) are obtained. bf-EVALP clause (61) is derived by basic bf-inference rule (0, 8)-rule-2. Moreover, since bf-EVALP clauses (59), (62) and (63) do not satisfy the bodies of bfEVALP clauses (31), (32) and (33), the forbiddance from starting process Pr 3 , st( p3 , t4 ) : [f, β] (64) cannot be derived. Therefore, the body of bf-EVALPSN clause (34) is satisfied, and the permission for starting process Pr 3 , st( p3 , t4 ) : [f, γ ] is derived. Therefore, process Pr 3 is permitted to start because processes Pr 0 , Pr 1 and Pr 2 have finished at time t4 . 6 Concluding remarks In this paper, we have introduced the process order control method based on a paraconsistent annotated logic program bf-EVALPSN, which can deal with before–after relation between processes with a small pipeline process order safety verification control. We would like to conclude this paper by describing the advantages and disadvantages of the process order control method based on bf-EVALPSN safety verification. Advantages – If a bf-EVALPSN is locally stratified [5], it can be easily implemented in Prolog, C language, Programmable Logic Controller (PLC) ladder program, etc. In practice, such control bf-EVALPSNs are locally stratified. – It has been proved that EVALPSN can be implemented as electronic circuits on micro chips [10]. Therefore, if real-time processing is required in the system, the method might be very useful. – The safety verification methods for both process control and process order control can be implemented under the same environment. Disadvantages – Since EVALPSN/bf-EVALPSN itself is basically not a specific tool of formal safety verification, it includes complicated and redundant expressions to construct safety verification systems. Therefore, it should be better to develop safety verification-oriented tool or programming language based on EVALPSN/bf-EVALPSN if EVALPSN/bf-EVALPSN can be applied to formal safety verification. References 1. Allen, J.F.: Towards a general theory of action and time. Artif. Intell. 23, 123–154 (1984) 2. Allen, J.F., Ferguson, G.: Actions and events in interval temporal logic. J. Log. Comput. 4, 531–579 (1994) 3. Blair, H.A., Subrahmanian, V.S.: Paraconsistent logic programming. Theor. Comput. Sci. 68, 135–154 (1989) 4. da Costa, N.C.A., et al.: The paraconsistent logics PT . Zeitschrift für Mathematische Logic und Grundlangen der Mathematik 37, 139–148 (1989) 5. Gelder, A.V., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. J. Assoc. Comput. Mach. ACM 38, 620–650 (1991) 6. Nakamatsu, K., Suzuki, A.: Annotated semantics for default reasoning. In: Proceedings of the 3rd Pacific Rim International Conference of Artificial Intelligence (PRICAI94), pp. 180–186. International Academic Publishers (1994) 7. Nakamatsu, K.: On the relation between vector annotated logic programs and defeasible theories. Log. Log. Philos. 8, 181–205 (2001) 8. Nakamatsu, K., et al.: A defeasible deontic reasoning system based on annotated logic programming. In: Proceedings of the 4th International Conference of Computing Anticipatory Systems (CASYS2000), AIP Conference Proceedings, vol. 573, pp. 609– 620. American Institute of Physics (2001) 9. Nakamatsu, K., et al.: Annotated Semantics for Defeasible Deontic Reasoning. LNAI 2005, pp. 432–440. Springer, New York (2001) 10. Nakamatsu, K., Mita, Y., Shibata, T.: An intelligent action control system based on extended vector annotated logic program and its hardware implementation. J. Intell. Autom. Soft Comput. 13, 222– 237 (2007) 11. Nakamatsu, K.: The paraconsistent annotated logic program EVALPSN and its application. Comput. Intell. Compend. Stud. Comput Intell. 115, 233–306 (2008). Springer 12. Nakamatsu, K., Abe, J.M.: The development of paraconsistent annotated logic program. Int. J. Reason.-Based Intell. Syst. 1, 92– 112 (2009) 13. Nakamatsu, K., Abe, J.M., Akama, S.: A logical reasoning system of process before–after relation based on a paraconsistent annotated logic program bf-EVALPSN. J. Knowl.-Based Intell. Eng. Syst. 15, 145–163 (2011) 14. Nute, D.: Basic defeasible logics. In: del Cerro, L. F., Penttonen, M. (eds.) Intensional Logics for Programming, pp. 125–154. Oxford University Press, Oxford (1992) 123