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 G

THEOREM (local testability)

Reduced DFA with state transition graph G is locally testable iff for any C-node (p, q) of G

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 G

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 G

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