|
RFC Matchbounds |
|
Description
The idea of RFC Matchbounds on SCCs is based on the idea of RFC Matchbounds on TRSs.
The difference is that instead of proving termination of a string rewrite system R, we want to prove absence of
infinite P-chains over R.
To prove absence of infinite P-chains over R, a certificate automaton is constructed, which is closed under
rewriting of match((P ∪ R)#). Initially, this automaton is constructed to recognize the set T of all strings
(b1, 0)(b2, 0)...(bn, 0)(#, 0)k for all l → b1b2...bn ∈ P.
If after the closure, the automaton is finite, the highest match height occurring in the automaton is
the match bound of P over R on T. As all string rewrite systems are trivially right-linear and
we can restrict our attention to minimal P-chains over R, this match bound implies the absence of
infinite P-chains over R.
Application and Configuration
The user can limit the number of nodes and/or edges created in search of a certificate automaton.
By selecting the Reverse option, RFC Matchbounds are tried both on the input SCC and
on the reversed SCCs (see Rule Reversal). The option Strip Symbols
removes superfluous identical symbols from the rules before attempting the proof using RFC Matchbounds.
One should apply this technique for SCCs for which P and R are string rewrite systems,
especially for small but hard ones.