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:
- Starheight Problem : compute the starheight of a regular language,
i.e. the minimal number of nested Kleene stars needed
for expressing the language with a regular expression.
- Limitedness problem : decide whether a
regular cost function is limited or not.
- Value 1 problem : decide whether a leaktight probabilistic automaton has value 1,
i.e. whether the automaton accepts some words
with probability arbitrarily close to 1.
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.
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.
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:
- the first line is the size of the automaton (number of states).
- the second line is the type of the automaton: c for classical, p for probabilistic.
- the third line is the alphabet. Each character is a letter, they should not be separated.
- the fourth line is the initial states. Each state should be separated by spaces.
- the fifth line is the final states. Each state should be separated by spaces.
- the next lines are the transition matrices, one for each letter in the input order.
A transition matrix is given by actions (1 and _) separated by spaces.
Each matrix is preceded by a single character line, the letter (for readability and checking purposes).
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].