STAMINA: STabilisation Monoids IN Automata Theory



Presentation

Stamina is a tool implementing algebraic techniques to solve decision problems from automata theory. Most importantly, it is, to the best of our knowledge, the very first implementation of an algorithm solving the starheight problem!
It has been written in C++, by Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi and Denis Kuperberg. The code is available on Github.
The core generic algorithm takes as input an automaton and computes its stabilisation monoid, which is a generalisation of its transition monoid.
Stamina is the successor of ACME, which also implements the transformation of an automaton into a stabilisation monoid. Thanks to several optimisations, Stamina is much faster and can handle much larger automata, which is necessary to solve the starheight problem.

Stamina may be used to solve these three algorithmic problems:

These three problems reduce to the computation of the stabilization monoid associated with the automaton, which is a challenge since the monoid is exponentially larger than the automaton. The compact data structures used in Stamina, together with optimizations and heuristics, allow this program to handle automata with several hundreds of states.


Support

The developpment of this tool has been supported by the ANR project StochMC.


Starheight computation examples

Stamina was able to determine the starheight of the following expressions.

ExpressionStarheightAutomatonComputation Log
(aa)*1 sh_1 sh_1.out
b*(b*ab*a)*2 sh_2 sh_2.out
(aa(ab)*bb(ab*))*2 sh_3 sh_3.out
(a*b*c)*2 sh_4 sh_4.out
(b*ab*)^61 sh_5 sh_5.out
(ab + aabb)^*1 sh_6 sh_6.out

Online demo

The following online demo can be used to solve the bounddness problem for automata with counters and the value 1 problems for probabilistic automata.

Problem to solve
Letters states counters
Density
Initial
  Final  

Output






Installation

The github directory is here.
To compile, open a terminal, go to the Stamina directory, type

cmake .

and then

make


The command

./StaminaTest file.txt -o out.dot

reads the automaton from file.txt, and outputs what is computed in out.dot, a graphic format.
If the automaton is a probabilistic automaton, it runs the Markov Monoid algorithm, if it is a classical non-deterministic automaton, it computes its starheight.
Line by line description of the input file format for automata:

Sage

Stamina can be integrated to Sage as a module.

After compiling Stamina, copy the files stamina.py and libacme.so to sage/stamina-0.1/src/.
To create a Sage package:

$ sage --pkg stamina-0.1


It produces a file stamina-0.1.spkg. It can be installed by

$ sage -p stamina-0.1.spkg


Now run Sage:

$ sage

sage: import stamina

sage: aut = Automaton({0:[(1,'a')],1:[(1,'a')]})

sage: aut.state(0).is_initial = True

sage: aut.state(1).is_final = True

sage: m = stamina.to_monoid(aut)

sage: m.has_val1()

sage: m.starheight()


Webmaster: Hugo Gimbert [hugo dot gimbert at cnrs dot fr].