T E S T A
S
A package TESTAS for checking some kinds
of testability, finding synchronizing words and road coloring.
Download the freeware version for WINDOWS:
TESTAS (zip file, about 200
KB)
The package
includes three main and some auxiliary programs. The main programs:
1)
analyze an automaton of the language presented as oriented labeled graph;
2)
find syntactic semigroup of the language,
3)
find road coloring of directed complete
graph,
4) view visual image of the
transition graph (and its subgraphs) based on the structure properties of the
graph.
The auxiliary programs (not included in DEMO version) find:
1) direct product of two transition graphs of the automaton;
2) direct
product of two syntactic semigroups of the
automaton,
TESTAS on
several prominent
CONFERENCES
Road coloring:
The program changed the labels (colors) on edges of the automaton for to turn it
into synchronizing automaton. The input automaton must be deterministic (no
empty cells in input). The search (input) table is considered as an
automaton with an arbitrary coloring (sometimes even synchronizing). One can see
visual presentation of the search automaton and after the coloring compare with
the visualization of the result. Subquadratic algorithm.
Visualisation:
A linear algorithm of the visualization of the graph (automaton). Labels on arcs
are presented by colors of the arcs.
Strongly connected components and paths (partially) are seen on the layout.
There is a deep connection between problems in
string pattern matching and finite automata. A number of classical algorithms in
everyday use in text editors actually compute finite automata from descriptions
of patterns as regular expressions. The class of languages arising from here is
the class of locally testable languages and
their genaralizations.
The concept of local testability is connected with
languages, finite automata, graphs and
semigroups.
Locally testable automata
have a wide spectrum of applications.
The package contains a set
of procedures for deciding whether or not a language given by transition graph
or by transition semigroup of its automaton is locally
testable, left [right] locally testable, threshold locally testable, bilateral
locally testable or piecewise testable .
The bounds for the order of local testability of transition graph and
order of local testability of transition semigroup are also found.
The k-testability of transition graph is verified for
arbitrary k.
Strictly locally testable
automata and their order are checked.
The local idempotency is verified on the
transition graph of the automaton.
Synchronizability of transition graph of automaton is
verified and some synchronizing words of short
(and of minimal) length are found.
The syntactic
semigroup is constructed from the transition graph of the automaton.
The complexity of the algorithms is lowest
between known for today.
Some definitions
Local testability, Threshold local
testability
Left, Right local
testability
Piecewise testability
Verification Tools
readme
Synchronizability
Paper in postscript file
A package TESTAS for checking some kinds of testability.
http://www.cs.biu.ac.il/~trakht
Thank You for any remarks concerning
the package!