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.

Expression	Starheight	Automaton	Computation 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*)^6	1	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 Computing Starheight of a Deterministic Automaton Checking Limitedness of a MultiCounter Automaton Checking Value 1 of a Probabilistic Automaton Computing the Stabilisation Monoid of a MultiCounter Automaton Computing the Stabilisation Monoid of a Probabilistic Automaton

Letters states counters

Density 10%20%30%40%30%60%70%80%90% Initial   Final

Output

---

Installation

The github directory is here.
Compiling stamina requires C++11 (or above) and cmake.
Open a terminal, go to the Stamina directory, type

mkdir build; cd build; cmake ..; make

The command

./StaminaTest file.txt -o out.dot

reads the automaton from file.txt, and outputs what is computed in out.dot, a graphical 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].