Determining whether a state is new from the equivalence oracle's perspective.

[steve-anunknown]

I'm studying the implementation of the StatePrefixEqOracle and I've taken an interest in the depth_first parameter which, when true, makes the oracle explore the new states of the hypothesis first, as explained in the comments:

class StatePrefixEqOracle(Oracle):
    """
    Equivalence oracle that achieves guided exploration by starting random walks from each state a walk_per_state
    times. Starting the random walk ensures that all states are reached at least walk_per_state times and that their
    surrounding is randomly explored. Note that each state serves as a root of random exploration of maximum length
    rand_walk_len exactly walk_per_state times during learning. Therefore excessive testing of initial states is
    avoided.
    """
    def __init__(self, alphabet: list, sul: SUL, walks_per_state=10, walk_len=12, depth_first=False):
        """
        Args:

            alphabet: input alphabet

            sul: system under learning

            walks_per_state:individual walks per state of the automaton over the whole learning process

            walk_len:length of random walk

            depth_first:first explore newest states
        """

I noticed that to achieve this, the list of states to be explored is sorted based on the length of the access sequence, as showcased in the following snippet:

if self.depth_first:
    # reverse sort the states by length of their access sequences
    # first do the random walk on the state with longest access sequence
    states_to_cover.sort(key=lambda x: len(x.prefix), reverse=True)
else:
    random.shuffle(states_to_cover)

Does greater length of access sequence imply that a state is newer?

[emuskardin]

Hi,

in general yes, but not necessarily*. I will explain in a bit why. This self.depth_first is a small heuristic that I have added when developing this oracle, tbh, it would have the same guarantees and everything without it, I just liked the idea that you first try to find counterexamples for states with the longer prefix. In the end, it does not matter as much, as all states will serve as an origin for a test case exactly walks_per_state times.

* I like to think of L* as a BFS exploration of underlying/hidden state space, while KV is more depth-first. So, in L*, shorter prefixes are generally identified early on, while in KV this is not necessarily the case.

TLDR:
The heuristic I liked, may lead to earlier identification of counterexamples, but upon completion of the whole test suite (walks_per_state tests of from each state of length walk_len), the order does not matter.

[steve-anunknown]

Understood, thanks for the insight! I will explore it some more on my own.

[emuskardin]

Just had a random realization: if you care about which states are youngest/identified last, in the L* you can see this by simply looking at the S set of the observation table. The S set is an ordered list where the the last element of the list is the last identified element, first element is the initial state and so on... so it is ordered from youngest to oldest.

In KV I would have to think a bit more, but this does not help you much from oracle perspective.

In an oracle, you can keep a list of list of states, where each sublist "identifies" the age of the state.

So in eq Oracle, you can do something like this:

       ....
       # in init
        # list of lists which identifies in which learning round state is identified/how old the state is
        # [[s1,s2], [s3], [s4,s5,s6]]
        # s1 and s2 are oldest, and s4,s5,s6 youngest
        self.state_identification_round = []

    def find_cex(self, hypothesis):

        if self.state_identification_round is []:
            self.state_identification_round.append([s.state_id for s in hypothesis.states])
        
        new_states = []
        for s in hypothesis.states:
            state_existed_before = any(s.state_id in previous_generation for previous_generation in self.state_identification_round)
            if not state_existed_before:
                new_states.append(s.state_id)
        
        self.state_identification_round.append(new_states)

[steve-anunknown]

This looks good. I tried something similar, using a dictionary with the state ids as keys and the 'age' of the states as values, incrementing them with each round. I will give your idea a try too, just for the sake of comparison.