How to minimize a chained mealy automata

[grandnew]

How to minimize a chained mealy automata

[mtf90]

Automata#minimize should do the trick, or if you don't need the original automaton anymore, Automata#invasiveMinimize. The Automata class is part of the automata-util module.

[grandnew]

Hi, @mtf90
Thanks for your reply. I'm new to automatalib so I'm not familiar with the APIs and their capabilities.
I tried Automata#invasiveMinimize using the following code:

public static void main(String[] args) throws IOException {
    Alphabet<Character> alphabet = Alphabets.characters('a', 'b');
    CompactMealy<Character, Integer> mealy = AutomatonBuilders.<Character, Integer>newMealy(alphabet)
            .withInitial(0)
            .from(0).on('a').withOutput(1).to(1)
            .from(1).on('b').withOutput(2).to(2)
            .from(2).on('a').withOutput(1).to(3).from(3).on('b').withOutput(2).to(4)
            .create();
    StringBuilder b = new StringBuilder();

    GraphDOT.write(mealy, mealy.getInputAlphabet(), b);
    System.out.println(b.toString());

    CompactMealy<Character, Integer> mealy_minimized = Automata.invasiveMinimize(mealy, mealy.getInputAlphabet());
    GraphDOT.write(mealy_minimized, mealy_minimized.getInputAlphabet(), b);
    System.out.println(b.toString());
    
}

The output is

digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="circle" label="4"];
        s0 -> s1 [label="a / 1"];
        s1 -> s2 [label="b / 2"];
        s2 -> s3 [label="a / 1"];
        s3 -> s4 [label="b / 2"];

__start0 [label="" shape="none" width="0" height="0"];
__start0 -> s0;

}

digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="circle" label="4"];
        s1 -> s3 [label="a / 1"];
        s2 -> s1 [label="b / 2"];
        s3 -> s0 [label="b / 2"];
        s4 -> s2 [label="a / 1"];

__start0 [label="" shape="none" width="0" height="0"];
__start0 -> s4;

}

The mealy automata was not minimized. Did I use it wrong? Thanks.

[mtf90]

Sorry, I should have looked at the automaton models more closely. Your two models are not equivalent. Your first model only supports translating the input sequence "abab" (there are no successors to state 4) whereas your expected model supports translating alternations of "a" and "b" of indefinite length. You probably want to change the last .to(4) to .to(0).

As a result, the minimization essentially reconstructs the original automaton and only renames the existing nodes.

[grandnew]

Got it! Thank you for your time and expertise.
My goal is to infer the protocol state machine based on the protocol session. For instance, consider the TCP session below:

C  -- SYN --> S
S  -- SYN/ACK --> C
C -- SYN --> S
S -- PUSH --> C
C -- SYN --> S
S -- PUSH --> C
C -- SYN --> S
S -- PUSH --> C

By modeling each tuple of request and response, we can generate the following chained Mealy machine:

digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s2 [shape="circle" label="2"];
        s3 [shape="circle" label="3"];
        s4 [shape="circle" label="4"];
        s0 -> s1 [label="SYN / SYN/ACK"];
        s1 -> s2 [label="SYN / PUSH"];
        s2 -> s3 [label="SYN / PUSH"];
        s3 -> s4 [label="SYN / PUSH"];

__start0 [label="" shape="none" width="0" height="0"];
__start0 -> s0;

}

Since the protocol session has a limited length, it is impossible to construct a chained Mealy machine of indefinite length. However, based on the insight, we can infer that the protocol state machine should be:

digraph g {

        s0 [shape="circle" label="0"];
        s1 [shape="circle" label="1"];
        s0 -> s1 [label="SYN / SYN/ACK"];
        s1 -> s1 [label="SYN / PUSH"];

__start0 [label="" shape="none" width="0" height="0"];
__start0 -> s0;

}

I wonder if there is any tool that can help me minimize the chained Mealy machine generated from a protocol session and can be used as the protocol state machine.

[mtf90]

Your description sounds exactly like the problem that automata learning is trying to solve: based on a finite set of observations, try to generalize the observed behavior to a finite state machine. Depending on how you can provide the observations either passive automata learning or active automata learning may be better suited. Conveniently, LearnLib offers solutions for both use-cases 😆.

If it is of any help, there also has been some research on applying automata learning to TCP implementations in the recent past (https://doi.org/10.1007/978-3-319-10702-8_6, https://doi.org/10.1007/978-3-319-67113-0_12). However, the register automata stuff is not yet implemented in LearnLib.

[grandnew]

@mtf90 Thanks for your helpful guidance! As my task involves inferring a protocol model based on a set of traffic observations, I believe that passive automata learning is the way to go. However, I have been unsuccessful in finding any examples or tutorials on how to accomplish this in LearnLib. LearnLib is a powerful tool, but there are relatively few tutorials available for it. Could you please let me know which class/function can help me achieve this? Thanks so much for your time and expertise.

[mtf90]

There exists an examples module which contains some exemplary setups to get you going. The module also contains an example for setting up a passive learning process. Unfortunately, LearnLib mainly focuses on active automata learning, so there is a somewhat restricted support for passive learning algorithms. While we have an RPNI implementation for Mealy systems, I can't really comment on its practical performance.

[grandnew]

@mtf90 Thanks for your helpful guidance! I'll try it 😆.

[mtf90]

@grandnew are there any question left to this particular issue, or can it be closed?

[mtf90]

I'm closing this issue for now since the problem seems to be solved. Feel free to open it again, if you find an actual problem within AutomataLib.