LT and LTT
LOCAL and LOCAL THRESHOLD TESTABILITY THEOREMS on GRAPHS
Let SCC be strongly connected component, node from cycle (with right unit) is an C-node, the
reachability on the graph is denoted by >, two-side reachability
let us denote by ~, the direct product of n copies of the
graph G let us denote by Gn, the node ps is the end of the path s with beginning
in p.
THEOREM (local testability)
Reduced DFA with state transition graph G
is locally testable iff for any C-node (p, q)
of G2 such that p > q we have
1. If q ~ p then p = q.
2. For any s from transition semigroup S
holds ps > q iff qs > q.
The case of local threshold testability is essentially more complicated.
Nevertheless, the most simple first items coincide in both theorems.
THEOREM (local threshold testability)
DFA A with state transition complete graph G
(or completed by sink state) is locally threshold testable iff
1) for every C-node ( p, q) of G2 p ~ q implies p = q,
2) for every four nodes p, q, t, r1 of
G such that
a) the node ( p, r1) is an C-node,
b) ( p,r1) > ( q, t),
c) there exists a node r such that
p > r > r1 and ( r, t) is an C-node
holds q > t.
3) every T3SCC is well defined,
Here is involved concept of strongly connected component T3SCC
defined on three nodes p, q, r1
Definition.Let p, q, r1 be nodes of graph G
such that ( p, r1)
is an C-node, p > q , p > r > r1 and
for some node r the node ( q, r) is an C-node.
For such nodes p, q, r1
let T3SCC( p, q, r1) be the SCC of G
containing the set
T( p, q, r1:={ t | ( p,r1) > (q, t), q > t and (q, t) is an C-node}
T3SCC is not well defined in general case, but an another situation holds for local
threshold testability.
4) for every four nodes p, q, r, q1 of
G such that
a) the nodes ( p, q1) and ( q, r) are C-nodes of
the graph G2,
b) p > q and p > r,
c) there exists a node r1 such that
( q,r) > ( q1, r1) and
( p, r1) is an C-node
holds T3SCC( p,q,r1) = T3SCC( p,r,q1).
next