Random Uniform walK In Automata

Rukia is a C++ library to explore graphical models by generating at random paths in automata.

Instead of using an isotropic random walk (i.e., choosing the next state uniformly at random among the successors of the current state), Rukia guides the random walk to guarantee a global uniform distribution among the elements to be covered, whatever the model topology. To do that, Rukia uses combinatorial techniques to count the number of elements to be covered and then guide the model exploration in order to maximize the minimal probability of covering one of those elements.

One particularity of Rukia is the use of space-efficient algorithms that leverage the limitation on the size of model and the length of paths that can be generated with this approach (See, for example, the Dichopile algorithm). Thus, it was possible to generate paths of length 4000 in an automaton with more than 12 million states.

Currently, Rukia supports the following coverage criteria:

  • All paths of length n (there is a trick to also allow all paths of length less or equal to n)
  • All lassos (kind of paths that end by a cycle -- useful for Monte Carlo model-checking)
  • An extension is under development for handling additional criteria besides "all paths" : "all edges" and "all vertices" and maybe criteria describing other sets of edges or vertices.


More on simulation

We have some experimental results that show the effectiveness of uniform drawing in relation to (isotropic) random walks.


More on download

Rukia is freely available. Please click on the link in the sidebar or refer to the download section.