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