m, where m ∈ N,1 < m ≤ |T|. In the following, we will also denoteT = (S0, . . . , Sn)as T =S0→. . .→Sn.
Example 4.2. LetT1 =a→b →abe a trace of execution. T1 is a trace of size 2 anda→ b andb→aare sub-traces of size 1 ofT1.
Definition 4.4(Consistent traces). LetT = (S0, . . . , Sn)andT′ = (S0′, . . . , Sm′ )be two traces of execution. T andT′ arek-consistent, withk∈N, iff∀i, j ∈N, i < n, j < m,Si =Sj and next(i, T)6=next(j, T′)implyprev(i, k, T)6=prev(j, k, T′).T andT′are said consistent iff they aremax(n, m)-consistent.
As shown in Figure4.4, a Markov(k) system may seem non-deterministic when it is represented by a state transitions diagram (right part of the figure). That is because such state transitions diagram only represents 1-step transitions. In this example, the transition from the statebis not Markov(1): the next state can be eithera,borǫ. But it can be Markov(2), because all traces of size 2 of Figure4.4are consistent.
Definition 4.5(k-step interpretation transitions). LetP be a logic program,Bbe the Herbrand base ofP andBkbe the timed Herbrand base ofPwith periodk. LetSbe a Markov(k′) system w.r.tP,k′ ≥k. Ak-step interpretation transition is a pair of interpretations(I, J)whereI ⊆ Bk
andJ ⊆ B.
Example 4.3. The traceab→b→acan be interpreted in the three following ways:
-(at−2bt−2bt−1, a): the 2-step interpretation transition that corresponds to the full traceab→ b→a.
-(at−1bt−1, b): the 1-step interpretation transition corresponding to the sub-traceab→b.
-(bt−1, a): the 1-step interpretation transition that corresponds to the sub-traceb→a.
Definition 4.6 (Extended Consistency). Let R be a rule and (I, J)be a k-step interpretation transition. Risconsistentwith(I, J)iffb+(R) ⊆I andb−(R)∩I =∅implyh(R)∈J. Let T be a sequence of state transitions, Ris consistent withT if it is consistent with everyk-step interpretation transitions ofT. LetO be a set of sequences of state transitions,Ris consistent withOifRis consistent with allT′ ∈O.
Algorithm 12LFkT(O) : Learn the most general rules that explainE 1: INPUT:Oa set of sequences of state transitions (traces of executions) 2: OUTPUT: The logic program that realizes the transitions ofO.
3: P′a vector of set of rules
4: Ea vector of set of pairs of interpretations(I, J) 5: maxk:=the size of the longest trace ofO
// 1) InitializeP′withmaxk, the logic program that contains the most general rules 6: foreachkfrom1tomaxkdo
7: Pk′ :=∅
8: foreachA∈ Bdo 9: Pk′ :=Pk∪ {A.}
10: end for 11: end for
12: // 2) Extract interpretation from trace of executions 13: E:=interprete(O)
14: // 3) SpecifyP′by the interpretation of the trace of executions 15: foreachkfrom1tomaxkdo
16: Ek:=thekthset of interpretation ofE 17: whileEk6=∅do
18: Pick(I, J)∈Ek; Ek:=Ek\ {(I, J)}
19: foreachA∈ Bdo
20: ifA /∈Jthen
21: RAI :=A←V
Bi∈IBi∧V
Cj∈(B\I)¬Cj
22: Pk′ :=thekthset of rule ofP′ 23: Pk′ :=Specialize(Pk′,RIA)
24: end if
25: end for
26: end while 27: end for
28: // 4) Merge the programs into a unique logic program 29: P :=∅
30: foreachkfrom1tomaxkdo 31: Pk′ :=thekthset of rule ofP′
32: Remove fromPk′ all rules that do not contain any literal of the formvt−k 33: P :=P∪Pk′
34: end for 35: returnP
i ≤n. The idea is to learn rules independently for each possiblek-step relation: 1-step rules, 2-step rules, . . . ,k-step rules. The rules learned from step interpretations will go into the 1-step program, the rules learned from 2-1-step interpretations will go into the 2-1-step program and so on. These different programs are merged at the end to constitute a logic program that realizes all consistent traces ofO.
Step 2: In order to use minimal specialization, we need to convert the input traces of execution into interpretation transitions. This conversion is done by the functioninterprete, whose pseudo code is given in Algorithm20. It extracts allk-step interpretations from each traceT ∈ O. It can be done by extracting and converting all sub-traces ofT into corresponding interpretations.
This way it produce one|T|-step interpretation, one|T| −1interpretation, . . . , one 1-step in-terpretation. The function outputs them as a vector of set of interpretation transitionsE, where each setEi corresponds to interpretation of sub-traces of sizei.
Algorithm 13interprete(O) : Extract interpretations transition from traces 1: INPUT:Oa set of sequences of state transitions (traces of executions) 2: OUTPUT:Ea vector of set of pairs of interpretations(I, J)
3: E:=∅
// Extract interpretations 4: foreach sequenceT ∈Odo 5: foreachkfrom|T|to1do
6: foreach sub-traceT′of sizekinTdo 7: sk:=thekthstate ofT′
8: I:=∅
9: foreach statesk′beforeskinT′do
10: i:=k−k′
11: foreach atoma∈sk′ do
12: I:=I∪ {at−i}
13: end for
14: Ek :=thekthset of interpretation ofE 15: Ek :=Ek∪ {(I, sk)}
16: end for
17: end for
18: end for 19: end for 20: returnE
Step 3: The algorithm iteratively learns from each set of pairs of interpretationsEi ∈E. Now it only needs to apply theLF1Tmethod of [64] on each setEi by analyzing each pair of inter-pretations(I, J) ∈ Ei. For each variableA thatdoes not appearinJ, it infers ananti-rule RAI := A ← V
Bi∈IBi ∧V
Cj∈(Bi\I)¬Cj, whereBi is the i-step atoms ofEi, i.e. all atoms that can appear in a rule ofEi. Then, minimal specialization is used to make the corresponding logic programPi′ consistent withRIA. Algorithm27shows the pseudo code of this operation.
In the function specialize, it first extracts all rules RP ∈ P that subsumes RIA. It generates the minimal specialization of eachRP by generating a rule for each literal in RIA. Each rule contains all literals ofRP plus the opposite of a literal inRIAso that RIA is not subsumed by that rule. Thenspecializeadds inP all the generated rules that are not subsumed byP, so that P becomes consistent with the transition(I, J).When all transitions have been analyzed,LF1T outputsP that has become the logic program that realizesE.
Step 4: After analyzing all interpretation transitions, the programs that have been learned are merged into a unique logic program. This operation guarantees that the rule outputted are con-sistent with all input traces of executions. If a rule is not concon-sistent with a trace of execution, it has to be deleted. It can be checked by comparing each rule with other logic programs. If an-step ruleR is more general than an′-step rulesR′, n′ < n, thenR is not consistent with the observations from whichR′ has been learned. To avoid this case, we just need to remove
Algorithm 14specialize(P,R) : specialize the logic programPto not subsume the ruleR 1: INPUT: a logic programPand a ruleR
2: OUTPUT: the minimal specific specialization of the rule ofPbyR.
3: conf licts: a set of rules 4: conf licts:=∅
// Search rules that need to be specialized 5: foreach ruleRP ∈Pdo
6: ifRP subsumesRthen
7: conf licts:=conf licts∪RP
8: P :=P\RP
9: end if 10: end for
// Revise the rules by minimal specialization 11: foreach ruleRc ∈conf lictsdo
12: foreach literall∈b(R)do 13: ifl /∈b(Rc)and¯l /∈b(Rc)then 14: R′c:= (h(Rc)←(b(Rc)∪¯l)) 15: ifPdoes not subsumeR′cthen
16: P :=P\ {R|Ris subsumed byRc′}
17: P :=P∪Rc′
18: end if
19: end if 20: end for 21: end for 22: returnP
n-step rules that have novnvariable. Finally, LFkToutputs a logic program that realizes all consistent traces of executions ofO. IfO is a set of traces of execution of a Boolean network, the logic program outputted byLFkTrepresents the Boolean functions of each variables. For each variable, it corresponds to the conditions over thekprevious step to make it active att+ 1.
Theorem 4.7 (Correctness ofLFkT). Let P be a logic program,B be the Herbrand base of P andBkbe the timed Herbrand base ofP with periodk. Let S be a Markov(k) system with respect toP. LetO be a set of traces ofS. UsingO as input,LFkToutputs a logic program that realizes all consistent traces ofO.
Proof. LetV be the vector of interpretation transition extracted fromO byLFkT(Algorithm 20). According to Theorem 4 of [64], initializing LF1T with {p.|p ∈ B}, by using minimal specialization iteratively on a set of interpretation transitionsE, we obtain a logic programP that realizesE. SinceLFkTuse the same method asLF1Ton each element ofV,LFkTlearns a vector of logic programsP′ such that each logic programp′n ∈P′ realizes the corresponding set of interpretation transitionsvn∈V,n≥1.
Let p′n ∈ P′ be the logic program learn from vn ∈ V, n ≥ 1. p′n is obtained by minimal specialization of{p.|p∈ B}with all anti-rule ofvn(non consistent rule). According to Theorem 3 of [64],p′ndoes not subsume any anti-rule that can be infered fromvn. Then,p′nrealizes all deterministic transition ofvn, that is∀(I, J)∈vn,6 ∃(I, J′), J 6=J′.
Sincevncontainsn-step interpretation transition that represent all sub-traces of sizenofO,p′n realizes all consistent sub-trace of size nofO. LetPn−1 be a logic program that realizes all consistent sub-traces of size at mostn−1ofO.p′ncan contains a ruleRsuch that(Bn\Bn−1)∩ b(R) = ∅ (no literal ofR refers to thet−nstate of the variables). In this caseRrealizes a sub-trace of sizenand also some sub-traces of size at mostn−1. If these sub-traces of size n−1 are consistent, then they are necessary realized byPn−1. Pn−1 ∪ {R}does not realize more consistent sub-trace of size at mostn−1thanPn−1. LetSRbe the set of rules ofp′nof the formR, then(p′n\SR)only realizes all sub-traces of sizenofO. Then the logic program Pn=Pn−1∪(p′n\SR)only realizes all consistent sub-trace of size at mostn−1ofOand all sub-traces of sizenofO, that isPnrealizes all consistent sub-traces of size at mostnofO.
Letp′1 ∈ P′ be the logic program learn from v1 ∈ V, and letP = p′1. Let R′ be all rule of the logic programp′nsuch that(Bn\ Bn−1)∩b(R′) 6= ∅. Iteratively adding rules R′ into P, starting by the logic programp′2untilp′k, we obtain a logic program that realizes all consistent sub-traces of size at mostkofO. So that, usingOas input,LFkToutputs a logic program that realizes all consistent traces ofO.
Theorem 4.8(Complexity). LetP be a logic program,Bbe the Herbrand base ofP andBkbe the timed Herbrand base ofP with periodk. LetS be a Markov(k) system with respect toP. LetO be a set of trace of execution ofS. The complexity of learningS fromO withLFkTis respectively:O(2nk)for memory andO(P
T∈O
|T| ·n2nk)for runtime.
Proof. n = |B| is the number of possible heads of rules ofS. nk = |Bk|is the maximum size of a rule ofS, i.e. the number of literals in the body; a literal can appear at most one time in the body of a rule. For each rule head ofB there are3nk possible bodies: each literal can either be positive, negative or absent from the body. From these preliminaries we conclude that the size of a Markov(k) system S learned byLFkT is at most|S| = n·3nk. But thanks to minimal specialization,|S|cannot exceedn·2nk; in the worst case,S contains only rules of sizenkwhere all literals appear and there is onlyn·2nk such rules. IfScontains a rule withm literals (m < nk), this rule subsumes2nk−mrules which cannot appear inS. Finally, minimal specialization also ensures thatSdoes not contain any pair of complementary rules, so that the complexity is further divided bynk; that is,|S|is bounded byO(n·2nknk) =O(2nkk ). To learnS, LFkTneeds to storekprogramsPithat are Markov(i) system with respect toP,1≤i≤k.
Conclusion 1:the memory use ofLFkTisO(Pk
i=1
|Pi|) =O(k·2nkk ) =O(2nk).
For each traceT ofO,LFkTextracts|T|pairs of interpretations. For each pair of interpretation (I, J),LFkTinfers an anti-rule ruleRIAfor eachA∈ B, A6∈J.LFkTcompares eachRIAwith all rules of each programsPi. There is atmost|B|anti-rules that can be infered from(I, J)by
LFkTand the size of each programPiis bound byO(2nkk ). Then, the complexity of learning one trace of executionT ∈OwithLFkTisO(|T| · |B| ·k|Pi|) =O(|T| ·n·k2nkk ) =O(|T| ·n2nk).
Conclusion 2:The complexity of learningS fromOwithLFkTisO(P
T∈O
|T| ·n2nk).
interpretation transition: (at−2bt−1, b) (abridged(a2b1, b)in the table to save space); and two 1-step interpretation transitions:(at−1, b)and(bt−1, b)that respectively represent the begin and the end of the trace. The aforementioned 2-step interpretation is used to revise the 2-step rules and the 1-step interpretations are used to revise the 1-step rules. From(at−2bt−1, b), sinceais not present in the second interpretation, the algorithm infers the anti-ruleR :=a←at−2, bt−1. Ris used to revise the 2-step rules that subsume it, so that these rules become consistent with the interpretation. This is done by the addition of the negation of each element of the body ofRinto the rulesatandbt. From(at−1, b)it also infers an anti-rule ofathat isR′ := a← at−1. The 1-step rules are revised byR′ and then it analyzes the second 1-step interpretation transition.
From(bt−1, b), it infers the anti-ruleR′′ :=a←bt−1, that is now used to revise the new 1-step rules. Here the rule ofbis not modified because it is consistent with the interpretation and, by extension, consistent with the trace.
Now, LFkTanalyzes the trace ab → b → a. The 2-step rules of b are revised by the anti-ruleR := b ← at−2, bt−2, bt−1 extracted from(at−2bt−2bt−1, a). The 1-step rules are revised by R′ := a ← at−1, bt−1 extracted from (at−1bt−1, b). Here, the rule a ← at−1, bt−1 is removed because it subsumes R′ (here it is R’ itself) and cannot be specified. This kind of deletion is represented by double stroked rules. the rule ofbis then revised by the second 1-step interpretation.
Then, the algorithm analyzes the traceb → b → a. Some 2-step rules ofbare specialized to become consistent with the trace. Some of them are removed because after specialization they are subsumed by other rules and them become useless. These rules are stroked in the table, it is the case ofR := b← ¬at−2,¬bt−2 the specialization ofR′ := b ← ¬at−2 by addingbt−2. This rule is subsumed byR′′ :=b← ¬bt−2and sinceR′′is consistent with the trace, we do not need to keepRbecause all rules that can be specialized fromRcan also be obtained byR′′. Solving continues until all traces have been analyzed. At the end, the 2-step rules are merged with the 1-step rules by removing the 1-step rules from the set of 2-step rules. These rules can be non consistent with some 1-step interpretations since they have not been revised by all of them. They can safely be removed, because if they are consistent with all 1-step interpretations, this means they will appear in the set of 1-step rules.
LFkTfinally outputs the two rules R1 := a ← bt−2, bt−1 andR2 := b ← at−2,¬bt−2, that correspond to the system of Example4.1. To ensure that the output is correct it will need to analyzes all possible traces of the system that is 2n∗k, withn the number of variables of the system andkthe size of a trace. Here it will require the analysis of all 16 possible traces. But, in this example, the algorithm succeeds to learn the rules of the system after the analysis of 8 traces of execution.
Run time (# of seconds)
# Traces k=1 k=2 k=3 k=4 k=5
10 0.23s 0.27s 0.16s 0.28s 0.31s
100 1.87s 2.49s 1.63s 2.37s 2.84s
1,000 15.3s 18.5s 13.3s 20.1s 23.8s
10,000 146s 218s 147s 201s 234s
100,000 2,177s 2,577s 1,643s 1,764s 2,243s 1,000,000 27,768s 22,517 12,384 15,670 20,413
Output size (# of rules)
# Traces k=1 k=2 k=3 k=4 k=5
10 994 735 413 1,162 1,278
100 837 736 383 1,025 1,156
1,000 835 647 364 942 1,096
10,000 728 739 408 857 987
100,000 929 535 390 788 950
1,000,000 833 559 350 769 930
0 200000 400000 600000 800000 1000000
0 5000 10000 15000 20000 25000 30000
k=1 k=2 k=3 k=4 k=5
# Traces
Time (s)