import vcsn
c = vcsn.context('lal_char(ab), b')
Let's take a simple 3-state automaton $\mathcal{A}$:
%%automaton -s a
context = "lal_char(ab), b"
0 -> 0 a
0 -> 1 b
1 -> 0 a
1 -> 1 b
2 -> 0 b
2 -> 1 a
We can check that $\mathcal{A}$ is synchronizing:
a.is_synchronizing()
We can guess from the figure that $aa$ is a synchronizing word of $\mathcal{A}$. We can verify that with is_synchronized_by
:
a.is_synchronized_by('aa')
To find a short synchronizing word, we need to use the synchronizing_word()
method, which takes an algorithm in paramater.
The default algorithm is greedy
, when no algorithm is specified.
a = c.cerny(4)
Eppstein's greedy is a $O(n^3)$ greedy algorithm which always synchronizes the closest pair first.
It can be called using synchronizing_word('greedy')
or synchronizing_word('eppstein')
a.synchronizing_word('greedy')
Cycle is a $O(n^3)$ algorithm similar to Greedy, which ensures that the pair synchronized contains the latest singleton in which the synchronization previously took place. This is less efficient in the general case but gives optimal results ($(n - 1)^2$) for Černý automata.
a.synchronizing_word('cycle')
SynchroP is a "one-step ahead" heuristic with a $O(n^5)$ time complexity that checks the distance of the new active states from $q_0$ after synchronizing a specific pair, and tries to minimize the sum of these distances.
a.synchronizing_word('synchrop')
SynchroPL is similar to SynchroP but adds the distance of the synchronized pair as a "cost" in the heuristic. Its time complexity is also $O(n^5)$.
a.synchronizing_word('synchropl')
FastSynchro finds labels that reduces the new distances of the active states when appended to the synchronizing word. To guarantee that the algorithm terminates, it is only used if the label reduces the overall distance. If not, a bounded SynchroPL heuristic is used. The complexity of this algorithm is $O(n^3)$.
a.synchronizing_word('fastsynchro')
All the algorithms can also be used with k-tapes transducers:
%%automaton -s t
context = "lat<lal_char(ab), lal_char(cd)>, b"
0 -> 1 a|c, b|c, b|d
0 -> 2 a|d
1 -> 0 a|d, b|c
1 -> 1 a|c
1 -> 2 b|d
2 -> 1 a|c, a|d, b|d
2 -> 2 b|c
t.synchronizing_word()
t.is_synchronized_by(t.synchronizing_word('fastsynchro'))
t.pair()