Experiment: Mining state graphs for concepts

Experiment

This blog primarily discusses new types of concepts, and new ways to use concepts, detailing the existing library of concepts, as well as how users can write their own concepts.

What if someone wants to use an existing design in their concept specification, however? They may have to manually convert the design, in STG or FSM form for example, to a concept specification, which may be a time consuming process.

To address this, we are experimenting with process-mining, and using this to find behaviours that can be described as concepts.

Background

Process-mining is a field which has multiple applications, for example, looking at the real world processes that occur in a business. Information provided for this consists of lists of events of the process in question. This will consist of many lists, each detailing a different instance of this process, with the events in the order they occured in this instance. Each event may occur in a different order in each instance, and listing all of these different event orders leads to something called an event log.

Process-mining takes these event-logs, and finds various points of interest that can reveal various points about the process. This could be problem areas, where for example, one event tends to always occur last, when it could occur much earlier. The idea of this is finding methods of improving the process for higher efficiency, for reduced costs, quicker process times and so on.

Process-mining with specifications

For this experiment, we are interested in the order of events that occur in a specification for an asynchronous system. In this case, the events are signal transitions, and the event logs are lists of the possible orders these signal transitions can occur in the system.

These event logs can be generated from any specification by looking at the state graph of this system, the graph which shows what possible signal transitions are possible when in any state. A state graph can be generated for nearly any system, and this is why we use these to mine.

We use a tool, pgminer to automatically find concurrency in these event logs, which can help us find concepts.

C-element example

We will start off with a simple example, a C-element. We have discussed the specification of a C-element in this blog before but now we need to imagine that we have got a C-element specification, for example an STG, but no concept specification.

An STG for a C-element could be as follows:

And the state graph for this:

Now, from the initial state, we can see that either a+ or b+ can occur, and this is important. This format shows the possible transitions at any time. Now we need to convert this to an event log.

This specification does state that for signals a and b to fall, c must have risen already, but this is done for clarity in the STG. If we were to test the C-element gate itself, we would find that there is no baring on the input from the output. With that said, we can produce the following event log:

a+ b+ c+
b+ a+ c+
a- b- c-
b- a- c-

Note that the first two lines are the set-phase of the C-element, what is required to set the output high, and the last two lines are the reset-phase. Each of the phases contains both possible orders of the signals a and b.

This event log can then be passed into pgminer. pgminer is integrated as a back-end tool for Workcraft, and can take an event log such as this, and produce a Conditional Partial Order Graph (CPOG), which can visualise the results, which will be a list of all possible events, with arcs to show possible orderings. The resulting CPOG from pgminer will be as follows:

This gives us two separate objects, one showing a+ and b+ directing to c+ , and one showing a- and b- directing to c-. These can be identified as separate concepts:

outputRise = rise a ~> rise c <> rise b ~> rise c
outputFall = fall a ~> fall c <> fall b ~> fall c

And this is the specification of a C-element, as we know from the post on C-elements.

Buck example

We will now take three scenarios of an asynchronous buck controller, used to regulate the voltage in a circuit. We will not discuss the ins and outs of the operation of this, but we will state that there are three scenarios, one for each operating mode of the buck. We will mine each one separatley.

First of all, we have the zc absent scenario. The STG for this is as follows:

Notice this is a loop. In this case we will consider all possible traces of events that return the system to the initial state, which in this case is before uv+.

The state graph for this STG is:

Note that it looks similar, there are no intracicies in the possible orders of transitions. If we simulate this, trying to find all possible orders of events, we will find the following event log will be produced.

uv+ gn- gn_ack- gp+ gp_ack+ uv- oc- gp- gp_ack- gn+ gn_ack+ oc-

This is to be expected, as the above STG has one path from the initial state and back to this state. Similarly, mining this with pgminer will produce the following CPOG:

This is completely flat, with no choices or joins etc, so there is no interesting concepts to be found from this. We can simply create the following concept:

zcAbsent = rise uv ~> fall gn     <> fall gn ~> fall gn_ack
        <> fall gn_ack ~> rise gp <> rise gp ~> rise gp_ack
        <> rise gp_ack ~> fall uv <> fall uv ~> rise oc
        <> rise oc ~> fall gp     <> fall gp ~> fall gp_ack
        <> fall gp_ack ~> rise gn <> rise gn ~> rise gn_ack
        <> rise gn_ack ~> fall oc <> fall oc ~> rise uv

This is quite a long specifiation, but it captures the behaviours we detected from mining the event log for this scenario, that is, that each signal transition directly causes another.

Now lets move onto the zc late scenario, which is a little more interesting to mine. The STG for this is:

This features some concurrency, and some interesting interactions, detailed in the state graph:

This shows that after uv+, zc+ and zc- will occur in that order at any point before uv-. This means, the state graph encompasses every possible order of these signal transitions. The event log for this scenario therefore is as follows:

uv+ zc+ zc- gn- gn_ack- gp+ gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ zc+ gn- zc- gn_ack- gp+ gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ zc+ gn- gn_ack- zc- gp+ gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ zc+ gn- gn_ack- gp+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ zc+ gn- gn_ack- gp+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- zc+ zc- gn_ack- gp+ gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- zc+ gn_ack- zc- gp+ gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- zc+ gn_ack- gp+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- zc+ gn_ack- gp+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- gn_ack- zc+ zc- gp+ gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- gn_ack- zc+ gp+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- gn_ack- zc+ gp+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- gn_ack- gp+ zc+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- gn_ack- gp+ zc+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
uv+ gn- gn_ack- gp+ gp_ack+ zc+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-

This is long, but ultimatley accounts for every possible order of events. If we mine this, however, we find the following CPOG:

This image shows the same concurrency with zc as in the STG, but also shows us how we can describe this in concepts:

zcLate = uvReact <> fallUV
      <> fall gn ~> fall gn_ack <> fall gn_ack ~> rise gp
      <> rise gp ~> rise gp_ack <> fall uv ~> rise oc
      <> rise oc ~> fall gp     <> fall gp ~> fall gp_ack
      <> fall gp_acl ~> rise gn <> rise gn ~> rise gn_ack
      <> rise gn_ack ~> fall oc <> fall oc ~> rise uv
  where
    uvReact = rise uv ~> fall gn     <> rise uv ~> rise zc
    fallUV  = rise gp_ack ~> fall uv <> fall zc ~> fall uv

Here, the concurrency showed with zc and the other branch can be captured in concepts, leading to uvReact and fallUV. The other concepts can be found as just simple causalities once again.

The final scenario is zc early, which has some differences, and a bit more concurrency. The STG is:

Note that zc+ occurs before uv+ in this, and that uv+ occuring will only then allow gp+. The state graph for zc early is as follows:

This indicates that uv may rise any time after zc+, but gp+ cannot occur until after uv+. Following gp+, zc- must occur before uv- can occur, but this can happen at anytime, before or after gp_ack+.

All of the concurrency leads to the following event log for this scenario:

zc+ gn- gn_ack- uv+ gp+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
zc+ gn- uv+ gn_ack- gp+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
zc+ uv+ gn- gn_ack- gp+ gp_ack+ zc- uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
zc+ gn- gn_ack- uv+ gp+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
zc+ gn- uv+ gn_ack- gp+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-
zc+ uv+ gn- gn_ack- gp+ zc- gp_ack+ uv- oc+ gp- gp_ack- gn+ gn_ack+ oc-

Mining this will provide us with another CPOG, with similar layouts to the STG:

But this leads us to another specification:

zcLate = zcReact <> gpRise <> fallUV
      <> fall gn ~> fall gn_ack <> rise gp ~> rise gp_ack
      <> fall uv ~> rise oc     <> rise oc ~> fall gp
      <> fall gp ~> fall gp_ack <> fall gp_acl ~> rise gn
      <> rise gn ~> rise gn_ack <> rise gn_ack ~> fall oc
      <> fall oc ~> rise zc
  where
    zcReact = rise zc ~> fall gn     <> rise zc ~> rise uv
    gpRise  = fall gn_ack ~> rise gp <> rise uv ~> rise gp
    fallUV  = rise gp_ack ~> fall uv <> fall zc ~> fall uv

Still, a long specification, but it encompasses all the reactions we can find from the mined state graph.

Finally

We find that we can mine event logs generated from state graphs in order to find a concept specification, but this method is in its infancy. We are yet to determine if there are any limitations to this, or the possible scope.

The concept specifications that this produces may not encompass some useful interactions, such as handshakes or mutual exclusion, but the concepts should still produce a viable STG for further use, verification and synthesis.

The specifications produced are also reasonably long, and we are also working on a method of taking a specification produced from this method, and optimising it, finding higher-level concepts which can replace some. This may or may not reveal to a reader some interesting interactions, and for some concepts like a handshake, which may not be revealed obviously, some embelishment with transitive concepts may be useful to help produce a more optimised, or at least more easily understood concept specification.

We will continue the experiment, aiming to find a way to automate this process and allow existing designs to be used along with concepts.

The tools used for this experiment are all open-source, and available online:

Plato - https://github.com/tuura/plato

pgminer - https://github.com/tuura/process-mining

Workcraft - http://workcraft.org - Plato and pgminer are also included in the download.