banner
KendyZ

KendyZ

feedId:65592353402595328+userId:54400481666870272
twitter
github
bilibili

Model learning Angluins' L-star algorithm

DFA#

The grammar of a regular language can be described using a regular expression or represented using a deterministic finite automaton (DFA), for example:

A string that contains only the characters 'a' and 'b', and each of them appears an even number of times.

Can be represented as

image

where q0 is both the initial and final state.

If the DFA is treated as a black box and the user can only obtain a boolean value (accept/reject) indicating whether a string satisfies the grammar after inputting a string, then the process of inferring the grammar/DFA based on trying different combinations of symbols and judging whether they satisfy the grammar can be seen as learning the state model.

Definitions, Notations#

A DFA is represented by a quintuple (Q,Σ,δ,F,q0)(Q,\Sigma,\delta,F,q_0):

  • QQ is the finite set of all possible states.
  • Σ\Sigma is the finite set of all possible symbols.
  • δ:Q×ΣQ\delta:Q\times\Sigma\rightarrow Q is the transition function: given a state and a symbol, the automaton will transition to the next state.
  • FF is the set of final states.
  • q0q_0 is the initial state.

Observation Table, OT#

The core of the L* algorithm is an observation table (OT), which can be represented as a triple $(S_D,E_D,T_D)$:

  • SDS_D contains a set of prefix-closed strings, which is part of the row index of the table. These strings represent possible states and are called access strings.
  • EDE_D contains a set of suffix-closed strings, which is the set of column indices of the table. These strings are used to distinguish different states (i.e., define the equivalence relation of states) and are called distinguish strings. For any two rows $s,t$, if each item of the distinguish strings they correspond to has the same value (i.e., the contents of these two rows are identical), then the states corresponding to these two rows are equivalent, denoted as sts\cong t. Equivalent states can be merged into one state, represented as one node in the DFA.
  • TDT_D: (SDSDΣ)×ED{0,1}(S_D \cup S_D \cdot \Sigma)\times E_D\rightarrow \{0,1\} represents the entries of each row and column in the table. The row index includes not only SDS_D, but also SDΣS_D\cdot\Sigma, which is a set of strings obtained by appending a symbol to each possible SDS_D. The value of TD(s,e)T_D(s,e) is determined by whether the string ses\cdot e (directly concatenated) can be accepted, and is a boolean value.
    • The rows SDS_D and SDΣS_D\cdot\Sigma are used to represent the states, while the additional rows are used to assist in determining the transition relationships between states.

To represent the OT as a valid DFA, two properties need to be satisfied:

  • Closure: Since SDΣS_D\cdot\Sigma represents the next state reached by starting from a state and adding a symbol, if this new state is not equivalent to any state in SDS_D, it means that there is at least one new state, i.e., the OT is not closed and can be further expanded. When constructing the DFA, it is known which destination state SDS_D will transition to after adding any symbol Σ\Sigma, if the destination state already exists in SDS_D, it is fine, but if it does not exist in SDS_D, it means that there are new states that have not been explored.
  • Consistency: For any two equivalent states s,tSDs,t\in S_D, for each symbol iΣi\in\Sigma, it should hold that sitis\cdot i\cong t\cdot i. If this is not true, it means that s and t are not equivalent, because starting from them and going through the same symbol may lead to different states. The equivalence relation is generated based on the current column index (distinguish string) of the OT, so the equivalence relation will also change when the column index changes. Generally, the understanding of a state is a process from fuzzy to precise, so the equivalence relation that was previously considered equal often becomes unequal as the distinguish string increases.

L* Algorithm#

  1. Initialize SD=ED={ϵ}S_D=E_D=\{\epsilon\}, and construct all rows of the OT together with SDΣS_D\cdot\Sigma.
  2. To obtain the values of each entry in the table, perform membership queries to the oracle: for (s,e)(s,e), ask the oracle if there is a path from state s through symbol e that can be accepted. Fill the entire table.
  3. Check for closure and consistency:
    1. If not closed, take an unclosed row from SDΣS_D\cdot\Sigma and move it to the SDS_D section.
    2. If not consistent, i.e., TD(si,e)TD(ti,e)T_D(s\cdot i,e)\neq T_D(t\cdot i,e), add iei\cdot e to the distinguish string. Expand the OT horizontally and fill the table with membership queries.
  4. If consistent, construct the DFA using the OT and perform an equivalence query to the oracle:
    1. If not equivalent, the oracle will return a counterexample, add all prefixes of the counterexample string to SDS_D, expand SDΣS_D\cdot\Sigma, and go back to step 2.
    2. If equivalent, then it is finished.

Example#

The complete process of the example given in "Reverse Engineering Enhanced State Models of Black Box Software Components to support Integration Testing" is as follows. Assume that the oracle has the following DFA.

image

where Σ={a,b}\Sigma=\{a,b\}, SDΣS_D\cdot\Sigma is ϵ\epsilon plus each symbol in Σ\Sigma (ϵa,ϵb{\epsilon\cdot a,\epsilon\cdot b}), and the initial state is q0=[ϵ]q0=[\epsilon].

image

  • The OT is consistent but not closed because ϵa\epsilon\cdot a does not have an equivalent row in SDS_D (ϵb\epsilon\cdot b), so ϵa\epsilon\cdot a (i.e., aa) is moved to SDS_D.
  • Since aa has been added to SDS_D, SDΣS_D\cdot\Sigma needs to add aa,aba\cdot a, a\cdot b, and perform membership queries to the oracle to obtain TD(aa,ϵ)=1, TD(ab,ϵ)=0T_D(a\cdot a,\epsilon)=1,\ T_D(a\cdot b,\epsilon)=0.
  • At this point, the OT is closed and consistent, and there are only 2 equivalence classes: {ϵ,aa}\{\epsilon,a\cdot a\} and {a,b,ab}\{a,b,a\cdot b\}. These two equivalence classes correspond to 2 states in the DFA, and the different states reached by adding characters a and b to the latter class can be obtained.

image

  • Perform an equivalence query and get the counterexample bbb\cdot b, which is not satisfied by the constructed DFA. Add all prefixes of bbb\cdot b ({b,bb}\{b,b\cdot b\}) to SDS_D and add {ba,bba,bbb}\{b\cdot a,b\cdot b\cdot a,b\cdot b\cdot b\} to SDΣS_D\cdot\Sigma.

image

  • The OT is closed but not consistent because TD(b,b)TD(ab,b)T_D(b,b)\neq T_D(a\cdot b,b). Therefore, further distinction is needed for states a,ba,b, based on the possible states they can transition to after adding another symbol aa.
  • Add aa to EDE_D and perform membership queries to the oracle to fill the entire OT. The previously equivalent states a,ba,b are no longer equivalent.
  • At this point, the OT is consistent and closed, and the DFA can be constructed.

image

  • Perform an equivalence query to the oracle and get the counterexample abba\cdot b\cdot b, which is accepted by the constructed DFA but rejected by the oracle. Add all prefixes of abba\cdot b\cdot b ({aba,abba,abbb}\{a\cdot b\cdot a,a\cdot b\cdot b\cdot a,a\cdot b\cdot b\cdot b\}) to SDS_D and add {aba,abba,abbb}\{a\cdot b\cdot a,a\cdot b\cdot b\cdot a,a\cdot b\cdot b\cdot b\} to SDΣS_D\cdot\Sigma.

image

  • At this point, the OT is closed but not consistent because TD(b,b)TD(ab,b)T_D(b,b)\neq T_D(a\cdot b,b). Therefore, add bb to EDE_D and expand the OT horizontally.
  • Perform membership queries to the oracle for the DFA, fill the entire table, and at this point, the OT is consistent and closed. The constructed DFA is equivalent to the oracle DFA according to the equivalence query.

image

  • Finally, the structure of the oracle DFA is obtained.

Conclusion#

  • The OT table is divided into two parts: the upper part SDS_D is represented by strings (symbol strings), and the lower part SDΣS_D\cdot\Sigma is used to assist in determining whether the transition target of SDS_D is known. If it is known, it should correspond to a certain SDS_D, and if it is unknown, it means that there should be new members in SDS_D.
  • The learning process of the L* algorithm is essentially a process of gradually clarifying the understanding of each state.
    • When the OT is not closed, it means that new states need to be added, and the scope needs to be further expanded.
    • When the OT is not consistent, it means that the understanding of equivalent states needs to be further refined.
  • EDE_D is the "characteristic value" used to distinguish different states. In the DFA, two states are considered equivalent if they can both reach final states through the same symbols or if they cannot reach final states through any symbols.

References:

Loading...
Ownership of this post data is guaranteed by blockchain and smart contracts to the creator alone.