❋♦r ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st✐♥❣✱ ❛ ❞✐st✐♥❝t✐♦♥ ♠✉st ❜❡ ♠❛❞❡ ❜❡t✇❡❡♥ ❡✈❡♥ts ♦❢ t❤❡ ❙❯❚ t❤❛t ❛r❡ ❝♦♥tr♦••❛❜•❡ ❜② t❤❡ t❡st s②st❡♠✱ ❢r♦♠ t❤♦s❡ t❤❛t ❛r❡ ♦♥•② ♦❜s❡r✈❛❜•❡✳ ❚❤❡r❡❢♦r❡✱ ✐♥ t❤✐s r❡♣♦rt ✇❡ ✉s❡ t❤❡ ■❖▲❚❙ ✭■♥♣✉t✲❖✉t♣✉t ▲❛❜❡•❡❞ ❚r❛♥s✐t✐♦♥ ❙②st❡♠✮ ♠♦❞❡•❬✻( ✱ ✇❤✐❝❤ ❛••♦✇s ❞✐✛❡r❡♥t✐❛t✐♥❣ ✐♥♣✉t✱ ♦✉t♣✉t ❛♥❞ ✐♥t❡r♥❛• ❡✈❡♥ts ✇❤✐•❡ ♣r❡❝✐s❡•② ✐♥❞✐❝❛t✐♥❣ t❤❡ ✐♥t❡r❢❛❝❡s s♣❡❝✐✜❡❞ ❢♦r ❡❛❝❤ ❡✈❡♥t✳ ❉❡✜♥✐t✐♦♥ ✶ ❆♥ ■❖▲❚❙ ✐s ❛ t✉♣•❡ M = (Q M , Σ M , T M , q M 0 ) ✇❤❡r❡ Q M ✐s t❤❡ s❡t ♦❢ st❛t❡s ♦❢ t❤❡ s②st❡♠ M ✇✐t❤ q M 0 ✐ts ✐♥✐t✐❛• st❛t❡✳ Σ M ✐s t❤❡ s❡t ♦❢ ♦❜s❡r✈❛❜•❡ ❡✈❡♥ts ❛t t❤❡ ✐♥t❡r❢❛❝❡s ♦❢ M ✳ ■♥ ■❖▲❚❙ ♠♦❞❡•✱ ✐♥♣✉t ❛♥❞ ♦✉t♣✉t ❛❝t✐♦♥s ❛r❡ ❞✐✛❡r❡♥t✐❛t❡❞✿ ❲❡ ♥♦t❡ p?a ✭r❡s♣✳ p!a✮ ❢♦r ❛♥ ✐♥♣✉t ✭r❡s♣✳ ♦✉t♣✉t✮ ♦❢ ♠❡ss❛❣❡ a ❛t ✐♥t❡r❢❛❝❡ p✳ T M ⊆ Q M × (Σ M ∪ τ ) × Q M ✐s t❤❡ tr❛♥s✐t✐♦♥ r❡•❛t✐♦♥✱ ✇❤❡r❡ τ / ∈ Σ M st❛♥❞s ❢♦r ❛♥ ✐♥t❡r♥❛• ❛❝t✐♦♥✳ ❚r❛♥s✐t✐♦♥ (q, α, q ′ ) ∈ T M ❝❛♥ ❜❡ ❡q✉❛••② ♥♦t❡❞ q α -→ M q ′ ✳ ❖t❤❡r ♥♦t❛t✐♦♥s ▲❡t ✉s ❝♦♥s✐❞❡r ❛♥ ■❖▲❚❙ M ✱ ❛♥❞ •❡t ❛♥ ♦❜s❡r✈❛❜•❡ ❡✈❡♥t α ∈ Σ M ✇✐t❤ α = p • {?, !} • m✱ ❛♥ ❡①❡❝✉t❛❜•❡ ❡✈❡♥t ♦❢ t❤❡ s②st❡♠ µ i ∈ Σ M ∪ τ ✱ ❛ s✉❝❝❡ss✐♦♥ ♦❢ ❡✈❡♥ts σ ∈ (Σ M ) * ✱ ❛♥❞ q✱ q ′ ∈ Q M ✳ ❲❡ ❞❡✜♥❡ t❤❡ ❢♦••♦✇✐♥❣ ♥♦t❛t✐♦♥s✿ • Σ M ❝❛♥ ❜❡ ♣❛rt✐t✐♦♥❡❞✿ Σ M =Σ M U ∪ Σ M L ✱ ✇❤❡r❡ Σ M U ✭r❡s♣✳ Σ M L ✮ ✐s t❤❡ s❡t ♦❢ ♠❡ss❛❣❡s ❡①❝❤❛♥❣❡❞ ♦♥ t❤❡ ✉♣♣❡r ✭r❡s♣✳ •♦✇❡r✮ ✐♥t❡r❢❛❝❡s✳ Σ M ❝❛♥ ❛•s♦ ❜❡ ♣❛rt✐t✐♦♥❡❞ t♦ ❞✐st✐♥❣✉✐s❤ ✐♥♣✉t ✭Σ M I ✮ ❛♥❞ ♦✉t♣✉t ♠❡ss❛❣❡s ✭Σ M O ✮✳ ■♥ ❛❞❞✐t✐♦♥✱ ✐♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st✐♥❣✱ ❝♦♥tr♦••❛❜•❡ ❡✈❡♥ts ❛♥❞ ♦❜s❡r✈❛❜•❡ ❡✈❡♥ts s❤♦✉•❞ ❜❡ ❞✐✛❡r❡♥t✐❛t❡❞✳ ■♥❞❡❡❞✱ Σ M I U ✐s t❤❡ s❡t ♦❢ t❤❡ ✐♥♣✉t ❡✈❡♥ts ♦♥ t❤❡ ✉♣♣❡r ✐♥t❡r❢❛❝❡s✱ ✐✳❡✳✱ t❤❡② r❡♣r❡s❡♥t t❤❡ ♠❡ss❛❣❡ ❝♦♠✐♥❣ ❢r♦♠ t❤❡ ✉♣♣❡r •❛②❡r✳ ■♥ ♣r❛❝t✐❝❡✱ t❤❡② ❛r❡ ♦❢t❡♥ ❝♦♥s✐❞❡r❡❞ ❛s ❝♦♥tr♦••❛❜•❡ st✐♠✉•✐ s❡♥t ❜② t❤❡ t❡st s②st❡♠✳ ❆•• ♦t❤❡r t②♣❡s ♦❢ ❡✈❡♥ts ❛r❡ ♦❜s❡r✈❛❜•❡ ❡✈❡♥ts✳ ✹ ◆✳ ❈❤❡♥ • Out(q) = def {α ∈ Σ M O |∃q ′ , q α -→M q ′ } ✐s t❤❡ s❡t ♦❢ ♣♦ss✐❜•❡ ♦✉t♣✉ts ❛t st❛t❡ q✳ ❙✐♠✐•❛r•②✱ In(q) = def {α ∈ Σ M I |∃q ′ , q α -→M q ′ } ✐s t❤❡ s❡t ♦❢ ♣♦ss✐❜•❡ ✐♥♣✉ts ❛♥❞ Γ(q) = def {α ∈ Σ M |∃q ′ , q α -→M q ′ } ✐s t❤❡ s❡t ♦❢ ❛•• ♣♦ss✐❜•❡ ❡✈❡♥ts ❛t t❤❡ st❛t❡ q✳ • q ❛❢t❡r σ = def {q ′ ∈ Q M |q σ ⇒M q ′ }
✐s t❤❡ s❡t ♦❢ st❛t❡s ✇❤✐❝❤ ❝❛♥ ❜❡ r❡❛❝❤❡❞ ❢r♦♠ q ❜② t❤❡ s❡q✉❡♥❝❡ ♦❢ ❛❝t✐♦♥s σ✳ ❙✉s♣❡♥s✐♦♥ ■❖▲❚❙ ■♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st✐♥❣✱ t❤❡ t❡st s②st❡♠ ❞♦❡s ♥♦t ♦♥•② ♦❜s❡r✈❡ tr❛❝❡s ♣r♦❞✉❝❡❞ ❜② ❛ s②st❡♠✱ ❜✉t ❛•s♦ q✉✐❡s❝❡♥❝❡ ❜② t✐♠❡rs✳ ❚❤❡r❡❢♦r❡✱ ✇❡ ❝♦♥s✐❞❡r q✉✐❡s❝❡♥❝❡ ❛♥ ♦❜s❡r✈❛❜•❡ ♦✉t♣✉t✳ ❚❤r❡❡ s✐t✉❛t✐♦♥s ♠❛② •❡❛❞ t♦ q✉✐❡s❝❡♥❝❡ ♦❢ ❛ s②st❡♠ ❛♥❞ ❛r❡ ✐••✉str❛t❡❞ ✐♥ t❤❡ ❢♦••♦✇✐♥❣ ✜❣✉r❡✳ ❆ ❞❡❛❞•♦❝❦ st❛t❡ ✭❝❢✳ ❋✐❣✳✷✲❛✮ ✐s ❛ st❛t❡ ✇❤❡r❡ t❤❡ s②st❡♠ ❝❛♥♥♦t ❡✈♦•✈❡ ❛♥②♠♦r❡✳ ✐✳❡✳ Γ✭q✮ ❂ Ø✳ ❆♥ ♦✉t♣✉t•♦❝❦ st❛t❡ ✭❝❢✳ ❋✐❣✳✷✲❜✮ ✐s ❛ st❛t❡ ✇❤❡r❡ t❤❡ s②st❡♠ ✐s ✇❛✐t✐♥❣ ♦♥•② ❢♦r ✐♥♣✉t✭s✮✱ ✐✳❡✳ Γ✭q✮⊆Σ M I ✳ ❆ •✐✈❡•♦❝❦ st❛t❡ ✭❝❢✳ ❋✐❣✳✷✲❝✮ ✐s ❛ st❛t❡ ❢r♦♠ ✇❤✐❝❤ t❤❡ s②st❡♠ ❞✐✈❡r❣❡s ❜② ❛♥ ✐♥✜♥✐t❡ s❡q✉❡♥❝❡ ♦❢ ✐♥t❡r♥❛• ❛❝t✐♦♥s✳ ✐✳❡✳ q ∈ livelock(M ) = def ∃τ 1 ,✳✳✳✱ τ n, q τ1...τn -→ M q✳ ❲❡ ❞❡♥♦t❡ t❤❡ s❡t ♦❢ ❞❡❛❞

•♦❝❦❡❞ st❛t❡s✱ ♦✉t♣✉t•♦❝❦ st❛t❡s ❛♥❞ •✐✈❡•♦❝❦ st❛t❡s ♦❢ t❤❡ ■❖▲❚❙ ▼ ❜② ❞❡❛❞•♦❝❦✭▼✮✱ ♦✉t♣✉t✲ •♦❝❦✭▼✮✱ ❛♥❞ •✐✈❡•♦❝❦✭▼✮ r❡s♣❡❝t✐✈❡•②✳ ❆ ❞❡❛❞•♦❝❦ ✐s ✐♥ ❢❛❝t ❛ s♣❡❝✐❛• ❝❛s❡ ♦❢ ♦✉t♣✉t•♦❝❦✱ ✐✳❡✳✱ ❞❡❛❞•♦❝❦✭▼✮⊆♦✉t♣✉t•♦❝❦✭▼✮✳ ❚❤❡r❡❢♦r❡✱ t❤❡ s❡t ♦❢ ❛•• q✉✐❡s❝❡♥t st❛t❡s ✐s ❞❡♥♦t❡❞ ❜②✿ q✉✐❡s❝❡♥t✭▼✮ ❂ ♦✉t♣✉t•♦❝❦✭▼✮ ∪ •✐✈❡•♦❝❦✭▼✮✳ ❋✐❣✉r❡ ✷✿ ◗✉✐❡s❝❡♥t st❛t❡s ❆♥ ■❖▲❚❙ ✐♥ ✇❤✐❝❤ q✉✐❡s❝❡♥❝❡ ✐s ♠♦❞❡•❡❞ ✐s ❝❛••❡❞ ❛ s✉s♣❡♥s✐♦♥ ■❖▲❚❙ ❛♥❞ ✐s ❞❡✜♥❡❞ ❜❡••♦✇✿ ❉❡✜♥✐t✐♦♥ ✷ ❚❤❡ s✉s♣❡♥s✐♦♥ ❛✉t♦♠❛t♦♥ ♦❢ ❛♥ ■❖▲❚❙ M = (Q M , Σ M , T M , q M 0 ) ✐s ❛♥ ■❖▲❚❙ △(M ) = (Q ∆(M ) ✱ Σ ∆(M ) ✱ T ∆(M ) ✱ q ∆(M ) 0 ) ✇❤❡r❡ Q ∆(M ) ❂ Q M ❀ q ∆(M ) 0 = q M 0 ❀ Σ ∆(M ) ❂Σ M ∪{δ} ✇✐t❤ δ ∈Σ ∆(M ) O ✳ ✐✳❡✳✱ δ ✐s ✉s❡❞ t♦ r❡♣r❡s❡♥t q✉✐❡s❝❡♥❝❡✱ ✇❤✐❝❤ ✐s r❡❣❛r❞❡❞ ❛s ❛♥ ♦❜s❡r✈❛❜•❡ ♦✉t♣✉t ♦❢ t❤❡ s②st❡♠✳ ❚❤❡ tr❛♥s✐t✐♦♥ r❡•❛t✐♦♥ T ∆(M ) ✐s ♦❜t❛✐♥❡❞ ❢r♦♠ T M ❜② ❛❞❞✐♥❣ •♦♦♣s ❢♦r ❡❛❝❤ q✉✐❡s❝❡♥t st❛t❡ q✳ ✐✳❡✳✱ T ∆(M ) ❂ T M ∪④(q, δ, q) |q ∈ quiescent(M )⑥ ❋♦r ❛ s♣❡❝✐✜❝❛t✐♦♥ ❙✱ t❤❡ tr❛❝❡s ♦❢ △(S) ❛r❡ ❝❛••❡❞ t❤❡ s✉s♣❡♥s✐♦♥ tr❛❝❡s ♦❢ ❙ ❛♥❞ ❛r❡ ❞❡♥♦t❡❞ ❜② ❙❚r❛❝❡s✭❙✮✳ ❙❚r❛❝❡s ✭❙✮ r❡♣r❡s❡♥ts ❛•• t❤❡ ❜❡❤❛✈✐♦r ♦❢ ❙ t❤❛t ❝❛♥ ❜❡ ♦❜s❡r✈❡❞✱ ✐♥❝•✉❞✐♥❣ q✉✐❡s❝❡♥❝❡✳ ❙✐♠✐•❛r•②✱ t❤❡ ✈✐s✐❜•❡ ❜❡❤❛✈✐♦r ♦❢ ❛♥ ■❯❚ ✐s ❛•s♦ ❝❤❛r❛❝t❡r✐③❡❞ ❜② ✐ts s✉s♣❡♥s✐♦♥ tr❛❝❡s ❙❚r❛❝❡s✭IU T ✮✳ ❆s②♥❝❤r♦♥♦✉s ■♥t❡r❛❝t✐♦♥ ■♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st✐♥❣✱ t❤❡ ✐♥t❡r❛❝t✐♦♥ ❜❡t✇❡❡♥ t✇♦ ■❯❚s ✐s ❛s②♥❝❤r♦♥♦✉s ❬✶✵✱ ✻( ❛s ♠❡ss❛❣❡s ♠❛② ❜❡ ❛❝t✉❛••② ❡①❝❤❛♥❣❡❞ ❜② tr❛✈❡rs✐♥❣ s❡✈❡r❛• ♣r♦t♦❝♦• •❛②❡rs✳ ❆❝❝♦r❞✐♥❣ t♦ ❬✻(✱ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ✐s ✉s✉❛••② ♠♦❞❡•❡❞ ❛s t✇♦ ✉♥✐❞✐r❡❝t✐♦♥❛• ❋■❋❖ q✉❡✉❡s✳ ❆♥❞✱ ❛s ✉s✉❛••② ❞♦♥❡ ✐♥ t❤❡ ✜❡•❞ ♦❢ t❡st✐♥❣✱ ✇❡ ❝♦♥s✐❞❡r t❤❛t t❤❡ t❡st✐♥❣ ❡♥✈✐r♦♥♠❡♥t ✐s ❡rr♦r✲❢r❡❡✳ ❋♦r♠❛••②✱ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ✐s ♥♦t❡❞ S 1 A S 2 ❢♦r t✇♦ ❝♦♠♠✉♥✐❝❛t✐♥❣ ■❖▲❚❙ S 1 ❛♥❞ S 2 ✳ ❆ st❛t❡ ✐♥ S 1 A S 2 ✐s ❛ ❢♦✉r✲t✉♣•❡ (q 1 , q 2 , f 1 , f 2 ) ✇❤❡r❡ q 1 ∈Q S1 ,q 2 ∈Q S2 , f 1 ✭r❡s♣✳f 2 ✮ st❛♥❞s ❢♦r t❤❡ ♠❡ss❛❣❡s ✐♥ t❤❡ ✐♥♣✉t ❝❤❛♥♥❡• ♦❢ S 1 ✭r❡s♣✳S 2 ✮✳ ■♥❢♦r♠❛••②✱ ❛ st❛t❡ (q 1 , q 2 , f 1 , f 2 ) ♠❡❛♥s t❤❛t t❤❡ ❡①❡❝✉t✐♦♥ ♦❢ S 1 ❛♥❞ S 2 ❤❛✈❡ r❡❛❝❤❡❞ st❛t❡ q 1 ❛♥❞ q 2 r❡s♣❡❝t✐✈❡•②✱ ✇❤✐•❡ t❤❡ ✐♥♣✉t ❝❤❛♥♥❡•s ♦❢ S 1 ❛♥❞ S 2 st♦r❡ t❤❡ •✐st ♦❢ ♠❡ss❛❣❡s f 1 ❛♥❞ f 2 r❡s♣❡❝t✐✈❡•②✳ ■♦♣ ❈r✐t❡r✐❛ ■♥ t❤✐s r❡♣♦rt✱ ✇❡ ❞❡❛• ✇✐t❤ t❤❡ ❣•♦❜❛• t♦t❛• ✐♦♣ t❡st✐♥❣ ❛r❝❤✐t❡❝t✉r❡✱ ✐✳❡✱ ❜♦t❤ •♦✇❡r ❛♥❞ ✉♣♣❡r ■❆P ♦❢ t✇♦ ■❯❚s ❛r❡ ❛❝❝❡ss✐❜•❡✳ ❚❤❡ ❝♦rr❡s♣♦♥❞✐♥❣ ❣•♦❜❛• t♦t❛• ✐♦♣ ❝r✐t❡r✐♦♥ s❛②s t❤❛t✿ ❚✇♦ ■❯❚s ❛r❡ ❝♦♥s✐❞❡r❡❞ ✐♥t❡r♦♣❡r❛❜•❡ ✐✛ ❛❢t❡r ❛ s✉s♣❡♥s✐♦♥ tr❛❝❡ ♦❢ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s ✐♥t❡r❛❝t✐♦♥✱ ❛•• ♦✉t♣✉ts✱ ✐♥❝•✉❞✐♥❣ q✉✐❡s❝❡♥❝❡ ♦❜s❡r✈❡❞ ❞✉r✐♥❣ t❤❡ ✐♥t❡r❛❝t✐♦♥ ♦❢ t❤❡ ✐♠♣•❡♠❡♥t❛t✐♦♥s ♠✉st ❜❡ ❢♦r❡s❡❡♥ ✐♥ t❤❡ ✐♥t❡r❛❝t✐♦♥ ♦❢ t❤❡✐r s♣❡❝✐✜❝❛t✐♦♥s✳ I 1 iop G I 2 ❂ ∀σ∈ ❙❚r❛❝❡s ✭S 1 A S 2 ✮✱ ❖✉t ✭I 1 A I 2 ✱ σ✮ ⊆ ❖✉t ✭△✭S 1 A S 2 ✮✱ σ✮ ✺ ✸ ■♥t❡r♦♣❡r❛❜✐•✐t② ❚❡st •❡♥❡r❛t✐♦♥ ✸✳✶ ❖✉t•✐♥❡s ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ ✐♥✈❡st✐❣❛t❡ ❛♥ ❛♣♣r♦❛❝❤ t♦ ❣•♦❜❛• t♦t❛• ✐♦♣ t❡st ❣❡♥❡r❛t✐♦♥✳ ❚❤❡ ♦❜•❡❝t✐✈❡ ♦❢ t❤❡ ♠❡t❤♦❞ ✐s t♦ ❣❡♥❡r✲ ❛t❡ ❡①❡❝✉t❛❜•❡ ■♥t❡r♦♣❡r❛❜✐•✐t② ❚❡st ❈❛s❡s ✭■❚❈✮ t♦ ✈❡r✐❢② t❤❡ ✐♥t❡r♦♣❡r❛❜✐•✐t② ♦❢ t✇♦ ■❯❚s✳ ❚❤❡ ✐♥♣✉ts ♦❢ t❤❡ ❛•❣♦r✐t❤♠ ❛r❡ t❤❡ s✉s♣❡♥s✐♦♥ s♣❡❝✐✜❝❛t✐♦♥s ♦♥ ✇❤✐❝❤ t❤❡ ■❯❚s ❛r❡ ❜❛s❡❞✱ ❛♥❞ ❛♥ ■♥t❡r♦♣❡r❛❜✐•✐t② ❚❡st P✉r♣♦s❡ ✭■❚P✮ ✇❤✐❝❤ r❡♣r❡✲ s❡♥ts ❛ ♣❛rt✐❝✉•❛r ♦❜•❡❝t✐✈❡ t♦ ❜❡ ✈❡r✐✜❡❞✳ ❚❤❡ ❡①❡❝✉t✐♦♥ ♦❢ ❛♥ ■❚❈ ♦♥ ❙❯❚ r❡t✉r♥s ❛ ✈❡r❞✐❝t ✿ verdict(IT C, SU T ) ∈ {P ass, F ail, Inconclusive}✳ ❱❡r❞✐❝t P ass ♠❡❛♥s t❤❡ t❡st ♣✉r♣♦s❡ ✐s r❡❛❝❤❡❞ ✇✐t❤♦✉t ❛♥② ❡rr♦r ❞❡t❡❝t❡❞✱ F ail ♠❡❛♥s ❛t •❡❛st ♦♥❡ ❡rr♦r ✐s ❞❡t❡❝t❡❞✱ ❛♥❞ Inconclusive ♠❡❛♥s t❤❡ ❜❡❤❛✈✐♦r ♦❢ ■❯❚s ✐s ❝♦rr❡❝t ✇✳r✳t t❤❡ ✐♥t❡r❛❝t✐♦♥ ♦❢ t❤❡✐r s♣❡❝✐✜❝❛t✐♦♥s✱ ❤♦✇❡✈❡r ❞♦❡s ♥♦t ❝♦rr❡s♣♦♥❞ t♦ t❤❡ t❡st ♣✉r♣♦s❡✳ ❚❤❡ ♠❡t❤♦❞ ❜❡❣✐♥s ✇✐t❤ t❤❡ ❝♦♥str✉❝t✐♦♥ ♦❢ ❛ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t ♦❢ t❤❡ s✉s♣❡♥s✐♦♥ s♣❡❝✐✜❝❛t✐♦♥s △(S 1 )✱ △(S 2 ) ❛♥❞ ■❚P✱ ✇❤✐❝❤ ❝♦rr❡s♣♦♥❞s t♦ ♣❛rt✐❛••② ❝❛•❝✉•❛t❡s t❤❡ s♣❡❝✐✜❝❛t✐♦♥s △✭S 1 A S 2 ✮ ✇✳r✳t t❤❡ ■❚P✳ ❚❤❡ ♣r♦❞✉❝t ✐♥t❡♥❞s t♦ ❝❛•❝✉•❛t❡ t❤❡ ❞✐✛❡r❡♥t ✇❛②s ♦❢ s♣❡❝✐✜❝❛t✐♦♥s✬ ✐♥t❡r❛❝t✐♦♥ t♦ r❡❛❝❤ t❤❡ ■❚P✳ ❚♦ ♦❜t❛✐♥ t❤❡ ♣r♦❞✉❝t✱ ❛s ✇❡•• ❛s t♦ ♠✐♥✐♠✐③❡ t❤❡ ♠❡♠♦r② r❡q✉✐r❡♠❡♥t✱ ❛ ❞❡♣t❤✲✜rst ❛•❣♦r✐t❤♠ ✐s ❛♣♣•✐❡❞✳ ❚♦ r❡❞✉❝❡ st❛t❡ ❡①♣•♦r❛t✐♦♥✱ t❤❡ tr❛♣ st❛t❡s ♦❢ ❡❛❝❤ ■❚P ❛r❡ ❛ss✐❣♥❡❞ ✇✐t❤ ❛ttr✐❜✉t❡s ❆❝❝❡♣t ✭♠❛♥❞❛t♦r②✮ ❛♥❞ |❡❢✉s❡ ✭♦♣t✐♦♥❛•✮✱ ✇❤❡r❡ ❆❝❝❡♣t ✭r❡s♣✳ |❡❢✉s❡ ✮ r❡♣r❡s❡♥ts t❤❡ ❞❡s✐r❡❞ ❜❡❤❛✈✐♦r ✭r❡s♣✳ ✉♥❞❡s✐r❡❞ ❜❡❤❛✈✐♦r✮ ✇✳r✳t ■❚P✳ ❚❤❡ ❛ttr✐❜✉t❡s ❛•s♦ s❡r✈❡ t♦ ✐♥❤✐❜✐t t❤❡ ❣❡♥❡r❛t✐♦♥ ♦❢ r❡❞✉♥❞❛♥t tr❛♥s✐t✐♦♥s✳ ✐✳❡✳✱ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ❝❛•❝✉•❛t✐♦♥ ✐s ❝✉t ❛s s♦♦♥ ❛s ❛♥ ❛ttr✐❜✉t❡ ✐s r❡❛❝❤❡❞✳ ❉✉r✐♥❣ t❤❡ ❝❛•❝✉•❛t✐♦♥✱ ✐t ♠❛② ❤❛♣♣❡♥ t❤❛t s♦♠❡ st❛t❡s ❝♦♥t❛✐♥ ❝♦♥✢✐❝t ✭❝♦♥tr♦••❛❜•❡ ❡✈❡♥ts ❛♥❞ ❛♥ ♦❜s❡r✈❛❜•❡ ❡✈❡♥ts✮✱ ✇❡ ❛♣♣•② ❝♦♥✢✐❝t ♠❛♥❛❣❡♠❡♥t r✉•❡s t♦ ❛✈♦✐❞ ❣❡♥❡r❛t✐♥❣ ✉♥♥❡❝❡ss❛r② ❝♦♥✢✐❝t tr❛♥s✐t✐♦♥s✳ ❋✐♥❛•②✱ ✇❡ ❢✉rt❤❡r ❛♣♣•② ✈❡r❞✐❝ts ❛ss✐❣♥♠❡♥t ❛♥❞ t❡st ❝❛s❡ ♠✐♥✐♠✐③❛t✐♦♥ r✉•❡s t♦ ♦❜t❛✐♥ ❛ ♠✐♥✐♠✐③❡❞ ❡①❡❝✉t❛❜•❡ ✐♦♣ t❡st ❝❛s❡✳ ✸✳✷ ❋♦r♠❛•✐③✐♥❣ ■♥t❡r♦♣❡r❛❜✐•✐t② ❚❡st P✉r♣♦s❡ ❛♥❞ ❚❡st ❈❛s❡ ✸✳✷✳✶ ■♥t❡r♦♣❡r❛❜✐•✐t②❚❡st P✉r♣♦s❡ ❚❤❡ ❣♦❛• ♦❢ t❡st✐♥❣ ✐s t♦ ✜♥❞ ❡rr♦rs ✐♥ ❙❯❚✳ ❍♦✇❡✈❡r ♣r♦✈✐♥❣ ❝♦rr❡❝t♥❡ss ✐s ❡•✉s✐✈❡ ❛s ✐t ✐s ❣❡♥❡r❛••② ✐♠♣♦ss✐❜•❡ t♦ ✈❛•✐❞❛t❡ ❛•• ♣♦ss✐❜•❡ ❜❡❤❛✈✐♦r ❞❡s❝r✐❜❡❞ ✐♥ s♣❡❝✐✜❝❛t✐♦♥s ❬✺(✳ ❋r♦♠ t❤❡ ♠❡t❤♦❞♦•♦❣✐❝❛• ♣♦✐♥t ♦❢ ✈✐❡✇✱ ♠♦st t❡sts ❛r❡ ❝❛rr✐❡❞ ♦♥ ❜② s❡tt✐♥❣ t❡st ♣✉r♣♦s❡s✳ ❆ t❡st ♣✉r♣♦s❡ ✐s ✐♥ ❣❡♥❡r❛• ✐♥❢♦r♠❛•✱ ✐♥ t❤❡ ❢♦r♠ ♦❢ ❛♥ ✐♥❝♦♠♣•❡t❡ s❡q✉❡♥❝❡ ♦❢ ❛❝t✐♦♥s r❡♣r❡s❡♥t✐♥❣ ❛ ❝r✐t✐❝❛• ♣r♦♣❡rt② t♦ ❜❡ ✈❡r✐✜❡❞✳ ■t ❝❛♥ ❜❡ ❞❡s✐❣♥❡❞ ❜② ❡①♣❡rts ♦r ♣r♦✈✐❞❡❞ ❜② st❛♥❞❛r❞s ❣✉✐❞❡•✐♥❡s ❢♦r t❡st s❡•❡❝t✐♦♥ ❬✹(✳ ■♥ t❤✐s r❡♣♦rt✱ ✇❡ ❛r❣✉❡ ♦♥ t❤❡ ✉s❡ ♦❢ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ♣✉r♣♦s❡ t♦ s❡•❡❝t t❡st ❝❛s❡s✳ ■♥❢♦r♠❛• ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ♣✉r♣♦s❡s ✭■❚P✮ ❛r❡ ❢♦r♠❛•✐③❡❞ ❜② ■❖▲❚❙ ♠♦❞❡•✳ ❚♦ s❡•❡❝t t❤❡ t❛r❣❡t ❜❡❤❛✈✐♦r✱ s♦♠❡ st❛t❡s ✐♥ t❤❡ ■❚P ❛r❡ ❛ss♦❝✐❛t❡❞ ✇✐t❤ ❛ttr✐❜✉t❡s ❆❝❝❡♣t t♦ ❞❡✜♥❡ P❛ss ✈❡r❞✐❝t✱ ✇❤✐•❡ |❡❢✉s❡ t♦ r❡♣r❡s❡♥t t❤❡ ♣♦ss✐❜•❡ ♦♣t✐♦♥s ✐♥ s♣❡❝✐✜❝❛t✐♦♥s ❜✉t ♥♦t t❤❡ ♦❜•❡❝t✐✈❡s ♦❢ t❤❡ t❡st✳ ❉❡✜♥✐t✐♦♥ ✸ ❆♥ ■♥t❡r♦♣❡r❛❜✐•✐t② ❚❡st P✉r♣♦s❡ ✐s ❛ ❞❡t❡r♠✐♥✐st✐❝ ❛❝②❝•✐❝ ❝♦♥tr♦••❛❜•❡ ■❖▲❚❙✿ ■❚P ❂ ✭Q IT P , Σ IT P ✱ T IT P ✱ q IT P 0 ✮ ✇❤❡r❡✿ • Σ IT P ⊆Σ S 1 ∪Σ S 2 ✳ ❚❤❡ s❡t ♦❢ ❜❡❤❛✈✐♦r ❞❡s❝r✐❜❡❞ ❜② t❤❡ ■❚P ♠✉st ❜❡ ✐♥❝•✉❞❡❞ ✐♥ t❤❡ s❡t ♦❢ ❜❡❤❛✈✐♦r ♦❢ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s✳ ✐✳❡✱ ❛♥ ■❚P ♠✉st ❜❡ ❝♦♥s✐st❡♥t ✇✳r✳t t❤❡ s♣❡❝✐✜❝❛t✐♦♥s✳ • Q IT P ✐s t❤❡ s❡t ♦❢ st❛t❡s✳ ❆♥ ■❚P ❤❛s t✇♦ s❡ts ♦❢ tr❛♣ st❛t❡s Accept IT P ❛♥❞ Ref use IT P ✳ Accept IT P st❛♥❞ ❢♦r t❤❡ ❞❡s✐r❡❞ ❜❡❤❛✈✐♦r t♦ ❜❡ ♦❜s❡r✈❡❞ ❛♥❞ ❛r❡ ❛ss♦❝✐❛t❡❞ ✇✐t❤ ❛ttr✐❜✉t❡ ❆❝❝❡♣t✳ Ref use IT P st❛♥❞ ❢♦r ♣♦ss✐❜•❡ ♦♣t✐♦♥s ✐♥ s♣❡❝✐✜❝❛t✐♦♥s r❛t❤❡r t❤❛♥ t❤❡ ❞❡s✐r❡❞ ❜❡❤❛✈✐♦r t♦ ❜❡ ✈❡r✐✜❡❞✱ ❛♥❞ ❛r❡ ❛ss♦❝✐❛t❡❞ ✇✐t❤ ❛ttr✐❜✉t❡ |❡❢✉s❡✳ ❙t❛t❡s ✐♥ Accept IT P ❛♥❞ Ref use IT P ❛r❡ ♦♥•② ❞✐r❡❝t•② r❡❛❝❤❛❜•❡ ❜② t❤❡ ♦❜s❡r✈❛t✐♦♥ ♦❢ ♦✉t♣✉ts ♣r♦❞✉❝❡❞ ❜② t❤❡ ■❯❚s✳ ❚❤✐s ✐s ❜❡❝❛✉s❡ ✐♥ ❜•❛❝❦ ❜♦① t❡st✐♥❣✱ t❤❡ ✈❡r✐✜❝❛t✐♦♥ ♦❢ ♦✉t♣✉ts ✐s ♠♦r❡ r❡•✐❛❜•❡✳ ■♥ ❢❛❝t✱ t❤❡ t❡st s②st❡♠ ❝❛♥ ♦♥•② ❦♥♦✇ ✐❢ ❛ ♠❡ss❛❣❡ ❤❛s ❜❡❡♥ s❡♥t t♦ ❛♥ ■❯❚✱ ❜✉t ♥♦t ✇❤❡t❤❡r t❤✐s ■❯❚ ❤❛s ❛❝t✉❛••② ♣r♦❝❡ss❡❞ t❤❡ ♠❡ss❛❣❡✳ ▼♦r❡♦✈❡r✱ Accept IT P =Ø ∧ Accept IT P ∩Ref use IT P ❂ Ø✳ • ■❚P s❛t✐s✜❡s t❤❡ ❝♦♥tr♦•❛❜✐•✐t② ❝♦♥❞✐t✐♦♥✿ ❢♦r ❡❛❝❤ st❛t❡ ✐♥ ■❚P✱ ♥♦ ❝❤♦✐❝❡ ✐s ❛••♦✇❡❞ ❜❡t✇❡❡♥ s❡✈❡r❛• st✐♠✉•✐ s❡♥t ❜② ❚❙ ✭❝♦♥tr♦••❛❜•❡ ❡✈❡♥ts✮ ♦r ❜❡t✇❡❡♥ ❛ st✐♠✉•✉s ❛♥❞ ❛♥ ♦✉t♣✉t ♦❢ ■❯❚ ✭♦❜s❡r✈❛❜•❡ ❡✈❡♥ts✮✳ • ■❚P ✐s ❝♦♠♣•❡t❡✱ ✇❤✐❝❤ ♠❡❛♥s t❤❛t ❡❛❝❤ st❛t❡ ❛••♦✇s ❛•• ❛❝t✐♦♥s✳ ❚❤✐s ✐s ❞♦♥❡ ❜② ✐♥s❡rt✐♥❣ ✏ * ✑ •❛❜•❡ ❛t ❡❛❝❤ st❛t❡ ♦❢ t❤❡ ■❚P✱ ✇❤❡r❡ ✏ * ✑ ✐s ❛♥ ❛❜❜r❡✈❛t✐♦♥ ❢♦r t❤❡ ❝♦♠♣•❡♠❡♥t s❡t ♦❢ ❛•• ♦t❤❡r ❡✈❡♥ts •❡❛✈✐♥❣ q✳ ■♥❞❡❡❞✱ ✏ * ✑ ❛••♦✇s ❞❡s❝r✐❜✐♥❣ t❡st ♣✉r♣♦s❡s ❛t ❛♥ ❛❜str❛❝t •❡✈❡• ✇✐t❤♦✉t ❝♦♥s✐❞❡r✐♥❣ ❞❡t❛✐•❡❞ ✐♥t❡r❛❝t✐♦♥✳ ✸✳✸ ■♥t❡r♦♣❡r❛❜✐•✐t② ❚❡st P✉r♣♦s❡ ✲ ❙♣❡❝✐✜❝❛t✐♦♥s Pr♦❞✉❝t ❚❤❡ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❣❡♥❡r❛t✐♦♥ ♠❡t❤♦❞ ❜❡❣✐♥s ✇✐t❤ t❤❡ ❝♦♥str✉❝t✐♦♥ ♦❢ ❛ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t ♦❢ △(S 1 )✱ △(S 2 ) ❛♥❞ ■❚P✱ ✇❤✐❝❤ ❝♦rr❡s♣♦♥❞s t♦ t❤❡ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ❝❛•❝✉•❛t✐♦♥ △✭S 1 A S 2 ✮ ✇✳r✳t t❤❡ ■❚P✳ ❚❤❡ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t ✐♥t❡♥❞s t♦ ❝❛•❝✉•❛t❡ t❤❡ ❞✐✛❡r❡♥t ✇❛②s t♦ ♦❜s❡r✈❡✴❡①❡❝✉t❡ t❤❡ ■❚P ♦♥ t❤❡ ❙❯❚✳ ❈♦••❡❝t✐♦♥ ❞❡s P✉❜•✐❝❛t✐♦♥s ■♥t❡r♥❡s ❞❡ •✬■r✐s❛ ❝ ■|■❙❆ ✻ ◆✳ ❈❤❡♥ ❉❡✜♥✐t✐♦♥ ✹ ❚❤❡ ♣r♦❞✉❝t ♦❢ △(S1)✱ △(S2) ❛♥❞ ■❚P ✐s ❛ ❝♦♥tr♦••❛❜•❡ s✉s♣❡♥s✐♦♥ ■❖▲❚❙ △(ST P ) =✭Q △(ST P ) , Σ △(ST P ) ✱ T △(ST P ) ✱ q △(ST P ) 0 ✮ ✇❤❡r❡✿ • Σ △(ST P ) ⊆Σ △(S 1 ) ∪Σ △(S 2 ) ✐s t❤❡ ❛•♣❤❛❜❡t✳ • Q △(ST P ) ✐s t❤❡ s❡t ♦❢ st❛t❡s✳ ❊❛❝❤ st❛t❡ ✭q △(S 1 ) , q △(S 2 ) ✱q IT P ✱f1✱f2✮ ∈ Q △(ST P ) ✐s s✉❝❤ t❤❛t q △(S 1 ) ∈Q △(S 1 ) ✱ q △(S 2 ) ∈Q △(S 2 ) ✱ q IT P ∈Q IT P ✱ f1 ✭r❡s♣✳ f2✮ r❡♣r❡s❡♥ts t❤❡ ✐♥♣✉t q✉❡✉❡ ♦❢ △(S1) ✭r❡s♣✳ △(S2)✮✳ q ST P 0 ❂ ✭q △(S 1 ) 0 ✱q △(S 2 ) 0 ✱q IT P 0 ✱ε✱ε✮ ✐s t❤❡ ✐♥✐t✐❛• st❛t❡ ♦❢ ❙❚P✱ ✇❤❡r❡ q △(S 1 ) 0 , q △(S 2 ) 0 ✱ q IT P 0 ❛r❡ t❤❡ ✐♥✐t✐❛• st❛t❡s ✐♥ △(S1), △(S2) ❛♥❞ ■❚P r❡s♣❡❝t✐✈❡•②✳ ε ❞❡♥♦t❡s ❛♥ ❡♠♣t② ✐♥♣✉t q✉❡✉❡✳ • Accept △(ST P ) , Ref use △(ST P ) ⊆Q △(ST P ) ✇❤❡r❡ Accept △(ST P ) ❂ Q △(ST P ) ∩ (Q △(S 1 ) ×Q △(S 2 ) ×Accept IT P ) ❛♥❞ Ref use △(ST P ) ❂ Q △(ST P ) ∩ (Q △(S 1 ) × Q △(S 2 ) × Ref use IT P ) • △(ST P ) ✐s ❝♦♥tr♦••❛❜•❡✿ ◆♦ ❝❤♦✐❝❡ ✐s ❛••♦✇❡❞ ❜❡t✇❡❡♥ s❡✈❡r❛• st✐♠✉•✐ s❡♥t ❜② ❚❙ ♦r ❜❡t✇❡❡♥ ❛ st✐♠✉•✉s ❛♥❞ ❛♥ ♦✉t♣✉t ♦❢ ■❯❚✳ ❚❤❡ ❝♦♥tr♦••❛❜•❡ ♣r♦♣❡rt② ✐♠♣•✐❡s t❤❛t ✐♥ ❛ st❛t❡ ✇✐t❤ ❛ ❝♦♥✢✐❝t✱ s♦♠❡ tr❛♥s✐t✐♦♥s ♠✉st ❜❡ ♣r✉♥❡❞✿ ❊✐t❤❡r ♦♥❡ st✐♠✉•✉s ✐s ❦❡♣t ❛♥❞ ❛•• ♦t❤❡r st✐♠✉•✐ ❛♥❞ ■❯❚ ♦✉t♣✉ts ❛r❡ ♣r✉♥❡❞✱ ♦r ❛•• ■❯❚ ♦✉t♣✉ts ❛r❡ ❦❡♣t ❜✉t st✐♠✉•✐ ❛r❡ ♣r✉♥❡❞✳ • T △(ST P ) ✐s t❤❡ s❡t ♦❢ tr❛♥s✐t✐♦♥s✳ • Q △(ST P ) ❛♥❞ T △(ST P ) ❛r❡ ♦❜t❛✐♥❡❞ ✐♥ t❤❡ ❢♦••♦✇✐♥❣ ✇❛②✿ ▲❡t q △(ST P ) = ✭q △(S 1 ) , q △(S 2 ) ✱q IT P ✱f1✱f2✮ ❜❡ ❛ st❛t❡ ✐♥ △(ST P )✱ ❛♥❞ •❡t a ❜❡ ❛ ♣♦ss✐❜•❡ ❛❝t✐♦♥ ❛t st❛t❡ q △(S 1 ) ♦r q △(S 2 ) ♦r q IT P ✳ ◆♦t✐❝❡ t❤❛t a ❝❛♥ ❜❡ ❛♥ ♦✉t♣✉t✱ ❛♥ ✐♥♣✉t✱ ♦r ❛ q✉✐❡s❝❡♥❝❡✳ ❆ ♥❡✇ tr❛♥s✐t✐♦♥ (q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✐s ❝r❡❛t❡❞ ❛❝❝♦r❞✐♥❣ t♦ t❤❡ ❢♦••♦✇✐♥❣ ❝♦♥❞✐t✐♦♥s✿ ✭✐✮ ■❢ ■❚P ✐s ✐♥ ♥❡✐t❤❡r ❆❝❝❡♣t ♥♦r |❡❢✉s❡ st❛t❡✱ ❝❤❡❝❦ t❤❡ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ♦♣❡r❛t✐♦♥ r✉•❡s ❜❡•♦✇✳ ■❢ ♦♥❡ r✉•❡ ✐s ❡①❡❝✉t❛❜•❡✱ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ △(ST P ) •❛❜❡•❡❞ ❜② a ✐s ❝r❡❛t❡❞ ❛❝❝♦r❞✐♥❣ t♦ t❤❡ r✉•❡✳ ✭✐✐✮ ■❢ ■❚P ✐s ✐♥ ❆❝❝❡♣t ♦r |❡❢✉s❡ st❛t❡✱ ♥♦ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ ❝r❡❛t❡❞✳ ✐✳❡✳✱ ❆❝❝❡♣t ❛♥❞ |❡❢✉s❡ ✐♥❤✐❜✐t ✉♥♥❡❝❡ss❛r② ❣•♦❜❛• ❜❡❤❛✈✐♦r ❝❛•❝✉•❛t✐♦♥✳ ❆s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ♦♣❡r❛t✐♦♥ r✉•❡s |✉•❡ ✶ ■❢ a ✐s ❛♥ ✉♣♣❡r ✐♥t❡r❢❛❝❡ ❛❝t✐♦♥ ♦r ❛ q✉✐❡s❝❡♥❝❡ ♦❢ △(Si) ✭✐❂④✶✱✷⑥✮✱ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ △(ST P ) •❛❜❡•❡❞ ❜② a ✐s ❝r❡❛t❡❞✳ ❚❤❡s❡ ❡✈❡♥ts ❞♦ ♥♦t ✐♥✢✉❡♥❝❡ t❤❡ ❝♦♠♠✉♥✐❝❛t✐♦♥ ❝❤❛♥♥❡•s ♦❢ t❤❡ ■❯❚s✳ ✭✶✳✶✮ ■❢ a ∈ Σ △(S 1 )
U ✱ (q △(S 1 ) , a, p △(S 1 ) ) ∈ T △(S 1 ) ✱ (q IT P , a, p IT P ) ∈ △ IT P =⇒(q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✇❤❡r❡ p △(ST P ) = ✭p △(S 1 ) , q △(S 2 ) ✱p IT P ✱f1✱f2✮✳ ✭✶✳✷✮ ■❢ a ∈ Σ △(S 2 ) U ✱ (q △(S 2 ) , a, p △(S 2 ) ) ∈ T △(S 2 ) ✱(q IT P , a, p IT P ) ∈ △ IT P =⇒ (q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✇❤❡r❡ p △(ST P ) = ✭q △(S 1 ) , p △(S 2 ) ✱p IT P ✱f1✱f2✮✳

|✉•❡ ✷ ■❢ a ✐s ❛ •♦✇❡r ✐♥t❡r❢❛❝❡ ♦✉t♣✉t ♦❢ △(Si) ✭❡①❝❡♣t q✉✐❡s❝❡♥❝❡✮✱ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ △(ST P ) •❛❜❡•❡❞ ❜② a ✐s ❝r❡❛t❡❞✳ a ✐s ♣✉t ✐♥t♦ t❤❡ t❛✐• ♦❢ t❤❡ ✐♥♣✉t q✉❡✉❡ ♦❢ △(Sj) ✭✐✱•❂④✶✱✷⑥✱ ✐ =•✮ ✿ ✭✷✳✶✮ ■❢ a ∈ Σ △(S 1 ) O L ❭δ✱ (q △(S 1 ) , a, p △(S 1 ) ) ∈ △ (S 1 ) ✱ (q IT P , a, p IT P ) ∈ △ IT P =⇒ (q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✇❤❡r❡ p △(ST P ) = (p △(S 1 ) , q △(S 2 ) , p IT P , f1, f ′ 2 ) ✇✐t❤ f ′ 2 = f2.a✳ ✭✷✳✷✮ ■❢ a ∈ Σ △(S 2 ) O L ❭δ✱ (q △(S 2 ) , a, p △(S 2 ) ) ∈ T △(S 2 ) ✱ (q IT P , a, p IT P ) ∈ △ IT P =⇒ (q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✇❤❡r❡ p △(ST P ) = (q △(S 1 ) , p △(S 2 ) , p IT P , f ′ 1 , f2) ✇✐t❤ f ′ 1 = f1.a✳ |✉•❡ ✸ ■❢ a ✐s ❛ •♦✇❡r ✐♥t❡r❢❛❝❡ ✐♥♣✉t✱ ❛♥❞ a ✐s t❤❡ ✜rst ❡•❡♠❡♥t ✐♥ t❤❡ ✐♥♣✉t q✉❡✉❡ ♦❢ △(Si)✱ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ △(ST P ) •❛❜❡•❡❞ ❜② a ✐s ❝r❡❛t❡❞✳ ✭✸✳✶✮ ■❢ a ∈ Σ △(S 1 ) I L ✱ a ∈ head(f1)✱ (q △(S 1 ) , a, p △(S 1 ) ) ∈ T △(S 1 ) ✱ (q IT P , a, p IT P ) ∈ △ IT P =⇒ (q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✇❤❡r❡ p △(ST P ) = (p △(S 1 ) , q △(S 2 ) , p IT P , f ′ 1 , f2) ✇✐t❤ f1 = a.f ′ 1 ✳ ✭✸✳✷✮ ■❢ a ∈ Σ △(S 2 ) I L ✱ a ∈ head(f2)✱ (q △(S 2 ) , a, p △(S 2
) ) ∈ T △(S 2 ) ✱ (q IT P , a, p IT P ) ∈ △ IT P =⇒ (q △(ST P ) , a, p △(ST P ) ) ∈ T △(ST P ) ✇❤❡r❡ p △(ST P ) = (q △(S 1 ) , p △(S 2 ) , p

IT P , f1, f ′ 2 ) ✇✐t❤ f2 = a.f ′ 2 ✳ • |✉•❡ ✶ ❞❡❛•s ✇✐t❤ ✉♣♣❡r ✐♥t❡r❢❛❝❡ ❡✈❡♥ts ♦r q✉✐❡s❝❡♥❝❡✿ ❚❤❡s❡ ❡✈❡♥ts ❞♦ ♥♦t ❞❡♣❡♥❞ ♦♥ t❤❡ st❛t❡ ♦❢ q✉❡✉❡s ❜❡t✇❡❡♥ t❤❡ t✇♦ s♣❡❝✐✜❝❛t✐♦♥s✱ ❜✉t ♦♥•② t❤❡ ❝✉rr❡♥t st❛t❡ ♦❢ t❤❡ △(Si) ❝♦♥❝❡r♥❡❞ ❜② t❤❡ ❡✈❡♥t✳ ✐✳❡✳✱ t❤❡ ❡✈❡♥t ✐s ❡①❡❝✉t❛❜•❡ ❞✉r✐♥❣ t❤❡ ✐♥t❡r❛❝t✐♦♥ ✐❢ ✐t ✐s ❡①❡❝✉t❛❜•❡ ❢♦r t❤❡ ❝♦♥❝❡r♥❡❞ △(Si) ❛t ✐ts st❛t❡ q △(S i ) ✳ ■♥ ❛❞❞✐t✐♦♥✱ t❤❡ ❡①❡❝✉t✐♦♥ ♦❢ t❤❡s❡ ❡✈❡♥ts ❞♦❡s ♥♦t ❛✛❡❝t t❤❡ st❛t✉s ♦❢ q✉❡✉❡s✳ ◆♦t✐❝❡ t❤❛t ✐♥ t❤✐s r✉•❡✱ q △(S i ) ❝❛♥ ❜❡ ❡q✉❛• t♦ p △(S i ) ✱ ✐♥ t❤❡ ❝❛s❡ ♦❢ a ✐s ❛ q✉✐❡s❝❡♥❝❡✳ ▼♦r❡♦✈❡r✱ q IT P ❝❛♥ ❜❡ ❡q✉❛• t♦ p IT P ❢♦r t❤❡ ❢♦••♦✇✐♥❣ r❡❛s♦♥✿ ❲❡ ❝♦♥s✐❞❡r t❤❛t t❤❡ ■❚P ✐s ❝♦♠♣•❡t❡✱ ✐✳❡✳✱ ❡❛❝❤ st❛t❡ ✐♥ ■❚P ❛••♦✇s ❛•• ❛❝t✐♦♥s✳ ❚❤❡ ❝♦♠♣•❡t❡♥❡ss ✼ ♦❢ ■❚P ✐s r❡❛•✐③❡❞ ❜② t❤❡ ✏ ✯✑ •♦♦♣s✳ ✏ ✯✑ st❛♥❞s ❢♦r ❛•• ❛❝t✐♦♥s ❛t ❛ st❛t❡ ❡①❝❡♣t t❤❡ ❡✈❡♥ts ✇❤✐❝❤ •❛❜❡• t❤❡ ♦✉t❣♦✐♥❣ tr❛♥s✐t✐♦♥s ❛t t❤✐s st❛t❡✳ • |✉•❡ ✷ ❞❡❛•s ✇✐t❤ •♦✇❡r ✐♥t❡r❢❛❝❡ ♦✉t♣✉t ❡✈❡♥ts✳ ❆♥ ♦✉t♣✉t ✐s ❡①❡❝✉t❛❜•❡ ❜② t❤❡ s②st❡♠ ❞✉r✐♥❣ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♥❣ ✐❢ △(Si) ✐s ✐♥ ❛ st❛t❡ ✇❤❡r❡ t❤❡ ♦✉t♣✉t ✐s s♣❡❝✐✜❡❞✳ ❚❤❡ ♠❡ss❛❣❡ a ✐s t❤❡♥ ❛❞❞❡❞ t♦ t❤❡ ❡♥❞ ♦❢ t❤❡ ✐♥♣✉t q✉❡✉❡ ♦❢ △(Sj)✳ ◆♦t✐❝❡ t❤❛t ♥♦r♠❛••② t❤❡ ❋■❋❖ q✉❡✉❡ ✐s ❜♦✉♥❞❡❞✳ ❚❤❡r❡❢♦r❡✱ ❛♥ ♦✉t♣✉t ✐s ❡①❡❝✉t❛❜•❡ ✐❢ t❤❡ q✉❡✉❡ ✐s ♥♦t ❢✉••✳ • |✉•❡ ✸ ❞❡❛•s ✇✐t❤ •♦✇❡r ✐♥t❡r❢❛❝❡ ✐♥♣✉t ❡✈❡♥ts✳ ❋♦r t❤❛t ❛♥ ✐♥♣✉t ❛t ❛ •♦✇❡r ❛♥ ✐♥t❡r❢❛❝❡ ❜❡ ❡①❡❝✉t❛❜•❡✱ t❤❡ r❡❝❡✐✈❡r △(Si) s❤♦✉•❞ ❜❡ ❛t ❛ st❛t❡ ✇❤❡r❡ t❤❡ r❡❝❡♣t✐♦♥ ✐s ❡①♣❡❝t❡❞ ❛♥❞ t❤❡ ❝♦rr❡s♣♦♥❞✐♥❣ ♠❡ss❛❣❡ ♠✉st ❤❛✈❡ ❜❡❡♥ s❡♥t ❜② △(Sj)✳ ✐✳❡✳ ❚❤❡ ♠❡ss❛❣❡ a t♦ ❜❡ r❡❝❡✐✈❡❞ ♠✉st ❜❡ ❛t t❤❡ ❤❡❛❞ ♦❢ t❤❡ ❋■❋❖ q✉❡✉❡ ♦❢ ✐ts ✐♥♣✉t •♦✇❡r ✐♥t❡r❢❛❝❡✳ △(Si) t❤❡♥ r❡♠♦✈❡s t❤❡ ♠❡ss❛❣❡ ❢r♦♠ t❤❡ q✉❡✉❡✳ ✸✳✸✳✶ ❉❡♣t❤✲✜rst ❙✉s♣❡♥s✐♦♥ ❙❚P ❈♦♥str✉❝t✐♦♥ ❚❤❡ r✉•❡s ❞❡✜♥❡❞ ❛❜♦✈❡ ❛••♦✇ ❜✉✐•❞✐♥❣ ❛ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t ♦❢ △(S 1 )✱ △(S 2 ) ❛♥❞ ■❚P r❡❝✉rs✐✈❡•② ❢r♦♠ t❤❡ ✐♥✐t✐❛• st❛t❡ q △(ST P ) 0 ✳ ❚❤❡ ❛ttr✐❜✉t❡s ❆❝❝❡♣t ♦r |❡❢✉s❡ ❛••♦✇ ❝♦♠♣✉t✐♥❣ ♦♥•② t❤❡ ♥❡❝❡ss❛r② ♣❛rt ♦❢ t❤❡ ❣•♦❜❛• ❜❡❤❛✈✐♦r ♦❢ t❤❡ s♣❡❝✐❝❛t✐♦♥s ✇✳r✳t t❤❡ ■❚P✳ ■♥❞❡❡❞✱ ❆❝❝❡♣t ♠❡❛♥s t❤❡ ✐♥t❡r❛❝t✐♦♥ ♦❢ t❤❡ s♣❡❝✐❝❛t✐♦♥s ❤❛s r❡❛❝❤❡❞ t❤❡ ■❚P✳ ❲❤✐•❡ |❡❢✉s❡ ♠❡❛♥s t❤❡ ✐♥t❡r❛❝t✐♦♥ ♦❢ s♣❡❝✐❝❛t✐♦♥s •❡❛❞ t♦ ❛♥ ♦♣t✐♦♥ ✐♥ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s ❛♥❞ ✇✐•• ♥♦t r❡❛❝❤ t❤❡ ❆❝❝❡♣t st❛t❡ ♦❢ t❤❡ ■❚P✳ ❚❤❡r❡❢♦r❡ ✐t ✐s ♥♦ ♥❡❡❞ t♦ ❝♦♥t✐♥✉❡ ❢✉rt❤❡r ❣•♦❜❛• ❜❡❤❛✈✐♦r ❝❛•❝✉•❛t✐♦♥✳ ❚❤❡ ❛•❣♦r✐t❤♠ ♦❢ △(ST P ) ❝♦♥str✉❝t✐♦♥ ✐s ❞❡♣t❤✲✜rst tr❛✈❡rs❛•✳ ❋r♦♠ t❤❡ ✐♥✐t✐❛• st❛t❡ q △(ST P ) 0 ✱ ❛t ❡❛❝❤ st❡♣ ✇❡ ❝❤❡❝❦ ✐❢ ❛ tr❛♥s✐t✐♦♥ ❝♦✉•❞ ❜❡ ❝r❡❛t❡❞ ❛❝❝♦r❞✐♥❣ t♦ t❤❡ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ♦♣❡r❛t✐♦♥ r✉•❡s✳ ❚❤r❡❡ ❝❛s❡s ❛r❡ ♣♦ss✐❜•❡✿ ✶✳ ❆t st❛t❡ q ✱ ♦♥•② ♦♥❡ r✉•❡ ❝❛♥ ❜❡ ❛♣♣•✐❡❞✿ ❚❤❡ ❝♦rr❡s♣♦♥❞✐♥❣ r✉•❡ ✐s ❛♣♣•✐❡❞ t♦ ❣❡♥❡r❛t❡ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ △(ST P )✳ ✷✳ ❆t st❛t❡ q ✱ s❡✈❡r❛• r✉•❡s ❝❛♥ ❜❡ ❛♣♣•✐❡❞✳ ✐✳❡✳✱ ❛t •❡❛st t✇♦ tr❛♥s✐t✐♦♥s ❝❛♥ ❜❡ ❣❡♥❡r❛t❡❞✳ q ✐s t❤❡♥ ❝❛••❡❞ ❜r❛♥❝❤✐♥❣ st❛t❡ ❛♥❞ st♦r❡❞ ✐♥ ❛ st❛❝❦✳ ❚❤❡♥ ✇❡ ❝❤♦♦s❡ ♦♥❡ ♦❢ t❤❡ ❛♣♣•✐❝❛❜•❡ r✉•❡s t♦ ❝❛rr② ♦✉t △(ST P ) ❝♦♥str✉❝t✐♦♥ ✉♥t✐• ♥♦ ♠♦r❡ r✉•❡s ❝❛♥ ❜❡ ❛♣♣•✐❡❞✳ ✐✳❡✳✱ Accept ♦r Ref use ❛ttr✐❜✉t❡ ✐s r❡❛❝❤❡❞✳ • ■❢ Accept △(ST P ) ✐s r❡❛❝❤❡❞✱ t❤❡ ❛•❣♦r✐t❤♠ ❝❛••s ❛ ❢✉♥❝t✐♦♥ ❆❝❝❡♣t❴♣❛t❤❴❝❛•❝✉•❛t✐♦♥ t♦ ❝❛•❝✉•❛t❡ t❤❡ ❝♦rr❡s♣♦♥❞✐♥❣ ♣❛t❤ t❤❛t tr❛✈❡rs❡s q △(ST P ) 0 ❛♥❞ t❤❡ Accept △(ST P ) ✳ ❚❤❡♥ t❤❡ ❛•❣♦r✐t❤♠ ❜❛❝❦tr❛❝❦s t♦ st❛t❡ q ❛♥❞ ❝❤♦♦s❡ ❛♥♦t❤❡r ♣♦ss✐❜•❡ r✉•❡ t♦ ❝♦♥t✐♥✉❡ ❙❚P ❝♦♥str✉❝t✐♦♥✳ • ■❢ Ref use △(ST P ) ✐s r❡❛❝❤❡❞✱ t❤❡ ❛•❣♦r✐t❤♠ ❜❛❝❦tr❛❝❦s t♦ st❛t❡ q ❛♥❞ ❝❤♦♦s❡ ❛♥♦t❤❡r ♣♦ss✐❜•❡ r✉•❡ t♦ ❝♦♥t✐♥✉❡ △(ST P ) ❝♦♥str✉❝t✐♦♥✳ • ■❢ ❛•• t❤❡ ♣♦ss✐❜•❡ r✉•❡s ❛t st❛t❡ q ❤❛✈❡ ❜❡❡♥ ❛♣♣•✐❡❞✱ q ✐s r❡♠♦✈❡❞ ❢r♦♠ t❤❡ st❛❝❦✳ ■♥ ♦r❞❡r t♦ s❛t✐s❢② t❤❡ ❝♦♥tr♦••❛❜•❡ ♣r♦♣❡rt② ♦❢ △(ST P )✳ ✐✳❡✳✱ ❡❛❝❤ st❛t❡ ♦❢ △(ST P ) ❤❛s ♥♦ ❝❤♦✐❝❡ ❜❡t✇❡❡♥ s❡✈❡r❛• st✐♠✉•✐ ♦r ❛ st✐♠✉•✉s ❛♥❞ ♦t❤❡r ❛❝t✐♦♥s✱ t❤❡ ❢♦••♦✇✐♥❣ r✉•❡s ❛r❡ ❞❡✜♥❡❞✿ • ❆t ❜r❛♥❝❤✐♥❣ st❛t❡ q ✱ ✐❢ ♥♦ r✉•❡ ❤❛s ❜❡❡♥ ❛♣♣•✐❡❞ ②❡t✱ ✇❡ ❛♣♣•② ♦♥❡ ♦❢ t❤❡ ❛♣♣•✐❝❛❜•❡ r✉•❡s t♦ ❣❡♥❡r❛t❡ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✐♥ △(ST P )✳ • ❆t ❜r❛♥❝❤✐♥❣ st❛t❡ q ✱ ✐❢ ✭❛t •❡❛st✮ ♦♥❡ tr❛♥s✐t✐♦♥ ❤❛s ❛•r❡❛❞② ❜❡❡♥ ❣❡♥❡r❛t❡❞✱ ❛♥❞ t❤❡r❡ ❡①✐sts ❛♥♦t❤❡r ♣♦ss✐❜•❡ r✉•❡ t❤❛t ❤❛s ♥♦t ❜❡❡♥ ❛♣♣•✐❡❞ ②❡t✳ ❲❡ ❝❤❡❝❦ ✐❢ t❤✐s r✉•❡ ❝♦♥✢✐❝ts ✇✐t❤ t❤❡ ❡①✐st✐♥❣ •❛❜❡•s Γ(q) ❛t st❛t❡ q✳ ❚✇♦ ❝❛s❡s ❛r❡ ♣♦ss✐❜•❡✿ ✕ ❚❤❡ r✉•❡ ❞♦❡s ♥♦t ❝♦♥✢✐❝t ❛♥② ♦❢ t❤❡ ❡①✐st✐♥❣ •❛❜❡•s ❛t st❛t❡ q ✳ ❚❤❡♥ ✇❡ ❛♣♣•② t❤❡ r✉•❡ ❛♥❞ ❝♦♥t✐♥✉❡ △(ST P ) ❝♦♥str✉❝t✐♦♥ ✉♥t✐• ♥♦ ♠♦r❡ r✉•❡s ❝❛♥ ❜❡ ❛♣♣•✐❡❞✳ ✕ ❚❤❡ r✉•❡ ❝♦♥✢✐❝ts ✭❛t •❡❛st ♦♥❡✮ ❡①✐st✐♥❣ ❛❝t✐♦♥s ❛t st❛t❡ q✳ ❚❤❡♥ ✇❡ ❝❤❡❝❦ ✇❤❡t❤❡r t❤❡r❡ ✐s ❛ •❛❜❡• ✭❡✈❡♥t✮ l ∈ Γ(q) t❤❛t ❤❛s r❡❛❝❤❡❞ Accept ST P ✳ ■❢ ♥♦t✱ ✇❡ ❛♣♣•② t❤❡ r✉•❡ ❛♥❞ ❝♦♥t✐♥✉❡ △(ST P ) ❝♦♥str✉❝t✐♦♥ ✉♥t✐• ♥♦ ♠♦r❡ r✉•❡s ❝❛♥ ❜❡ ❛♣♣•✐❡❞✳ ❖t❤❡r✇✐s❡ ✇❡ ✇✐•• ♥♦t ❛♣♣•② t❤❡ r✉•❡✳ ❇② ❝❤❡❝❦✐♥❣ ❝♦♥✢✐❝t ❝♦♥❞✐t✐♦♥s✱ s♦♠❡ ❝♦♥✢✐❝t tr❛♥s✐t✐♦♥s ❝❛♥ ❜❡ ❛✈♦✐❞❡❞ ❜❡✐♥❣ ❞❡✈❡•♦♣❡❞✳ ❍♦✇❡✈❡r✱ ♥♦t ❛•• t❤❡ ❝♦♥✢✐❝t tr❛♥s✐t✐♦♥s ❝❛♥ ❜❡ ❛✈♦✐❞❡❞ ✐♥ t❤✐s ✇❛②✳ ❚♦ ♣r✉♥❡ ❛•• t❤❡ ❝♦♥✢✐❝t tr❛♥s✐t✐♦♥s✱ ❛ ❜❛❝❦tr❛❝❦✐♥❣ ♣r♦❝❡❞✉r❡ ✇✐•• ❜❡ ♣❡r❢♦r♠❡❞ ✇❤❡♥ △(ST P ) ✐s ✜♥✐s❤❡❞ ❜❡✐♥❣ ❝♦♥str✉❝t❡❞✳ ✸✳ ❆t st❛t❡ q ✱ ♥♦ r✉•❡ ❝❛♥ ❜❡ ❛♣♣•✐❡❞✳ ❚❤❡♥ ✇❡ ❝❤❡❝❦ ✐❢ t❤❡ st❛❝❦ t❤❛t st♦r❡s ❜r❛♥❝❤✐♥❣ st❛t❡s ✐s ❡♠♣t②✳ ■❢ ✐t ✐s ♥♦t ❡♠♣t②✱ ✇❡ •✉♠♣ t♦ st❛t❡ st♦r❡❞ ✐♥ t❤❡ t♦♣ ♣♦s✐t✐♦♥ ♦❢ t❤❡ st❛❝❦ ❛♥❞ ❝♦♥t✐♥✉❡ △(ST P ) ❝♦♥str✉❝t✐♦♥✳ ❖♥ t❤❡ ❝♦♥tr❛r②✱ ✐❢ t❤❡ st❛❝❦ ✐s ❡♠♣t②✳ ✐✳❡✳✱ ♥♦ ♠♦r❡ st❛t❡ ❝❛♥ ❜❡ ❡①♣•♦r❡❞✳ ❚❤❡ ❛•❣♦r✐t❤♠ st♦♣s✳ ❚❤❡ △(ST P ) ❝♦♥str✉❝t✐♦♥ ❛•❣♦r✐t❤♠ ❛♥❞ ❆❝❝❡♣t P❛t❤ ❈❛•❝✉•❛t✐♦♥ ❛•❣♦r✐t❤♠ ❝❛♥ ❜❡ ❢♦✉♥❞ ✐♥ ❆♣♣❡♥❞✐① ❆✳ ❈♦••❡❝t✐♦♥ ❞❡s P✉❜•✐❝❛t✐♦♥s ■♥t❡r♥❡s ❞❡ •✬■r✐s❛ ❝ ■|■❙❆ ✽ ◆✳ ❈❤❡♥ ✸✳✸✳✷ ❆♣♣•✐❝❛t✐♦♥ t♦ ❛ s✐♠♣•❡ ❝♦♥♥❡❝t✐♦♥ ♣r♦t♦❝♦• ❈♦♥s✐❞❡r t❤❡ ❡①❛♠♣•❡ ♦❢ ❛ s✐♠♣•❡ ❝♦♥♥❡❝t✐♦♥ ♣r♦t♦❝♦• ✐••✉str❛t❡❞ ✐♥ ❋✐❣✳✸✳ ❙✉s♣❡♥s✐♦♥ s♣❡❝✐✜❝❛t✐♦♥s S 1 ❛♥❞ S 2 r❡♣r❡s❡♥t r❡s♣❡❝t✐✈❡•② ❛ ❝•✐❡♥t ❛♥❞ ❛ s❡r✈❡r✳ U 1?CN R ✐s ❛ ❝♦♥♥❡❝t✐♦♥ r❡q✉❡st ❢r♦♠ t❤❡ ✉♣♣❡r •❛②❡r✱ ✇❤✐•❡ U 1?Close ✐s ❛ ❞✐s❝♦♥♥❡❝t✐♦♥ r❡q✉❡st✳ l1!cnr ✭r❡s♣✳ l2?cnr✮ ✐s t❤❡ r❡q✉❡st s❡♥t t♦ ✭r❡s♣✳ r❡❝❡✐✈❡❞ ❜②✮ t❤❡ ♣❡❡r ■❯❚✳ l2!ack ✭r❡s♣✳ l2!nack✮ ✐s t❤❡ ♣♦s✐t✐✈❡ ✭r❡s♣✳ ♥❡❣❛t✐✈❡✮ r❡s♣♦♥s❡ ♦❢ t❤❡ s❡r✈❡r✱ ❛♥❞ U 1!ACK ✭r❡s♣✳ U 1!N ACK✮ ✐s t❤❡ r❡s♣♦♥s❡ ❢♦r✇❛r❞❡❞ t♦ t❤❡ ✉♣♣❡r •❛②❡r ❢♦••♦✇✐♥❣ t❤❡ r❡❝❡♣t✐♦♥ ♦❢ l2!ack ✭r❡s♣✳ l2!nack✮✳ ▼♦r❡♦✈❡r✱ q✉✐❡s❝❡♥❝❡ st❛t❡s ❛r❡ ❡①♣•✐❝✐t•② ♠♦❞❡•❡❞✿ ■♥ S 1 ✱ t✇♦ st❛t❡s ❝♦♥t❛✐♥ ♦✉t♣✉t•♦❝❦s ④✵✱ ✷⑥❀ ✇❤✐•❡ ✐♥ S 2 ✱ st❛t❡ ✵ ❝♦♥t❛✐♥s ❛♥ ♦✉t♣✉t•♦❝❦✳ ❚❤❡ ■❚P ✐♥ t❤✐s ❡①❛♠♣•❡ ❛✐♠s ❛t t❡st✐♥❣ ❛ ❝♦♥♥❡❝t✐♦♥ r❡q✉❡st CN R s❡♥t t♦ IU T 1 •❡❛❞s t♦ ❛ ♣♦s✐t✐✈❡ r❡s♣♦♥s❡ l2!ack✱ ✇❤✐•❡ l2!nack ✐s ❞❡✜♥❡❞ ❛s Ref use ❜❡❤❛✈✐♦r✳ ✐✳❡✳✱ ❛•• ❡✈❡♥ts s✉❜s❡q✉❡♥t t♦ l2!nack ❛r❡ ♥♦t t❤❡ t❛r❣❡t ♦❢ t❡st ❝❛s❡ ❛♥❞ s❤♦✉•❞ ♥♦t ❜❡ t❛❦❡♥ ✐♥t♦ ❛❝❝♦✉♥t✳ ❋✐❣✉r❡ ✸✿ ❈♦♥♥❡❝t✐♦♥ ♣r♦t♦❝♦• s♣❡❝✐✜❝❛t✐♦♥s ❛♥❞ ✐♦♣ t❡st ♣✉r♣♦s❡ ■♥ ♣r❛❝t✐❝❡✱ ❛ ♠❛①✐♠❛• ❞❡♣t❤ ❝❛♥ ❜❡ ✉s❡❞ ❞✉r✐♥❣ △(ST P ) ❝♦♥str✉❝t✐♦♥✱ ✇❤✐❝❤ ❝❛♥ ❜❡ q✉✐t❡ ✉s❡❢✉• ✇❤❡♥ t❤❡r❡ ❛r❡ ❝②❝•❡s ✐♥ s♣❡❝✐✜❝❛t✐♦♥✳ ■♥ t❤✐s ❡①❛♠♣•❡ ✇❡ ❛♣♣•② t❤❡ ❞❡♣t❤✲✜rst △(ST P ) ❝♦♥str✉❝t✐♦♥ ❛•❣♦r✐t❤♠ ✇✐t❤ ❛ ♠❛①✐♠❛• ❞❡♣t❤ ❝♦♥✜❣✉r❡❞ t♦ ✺✳ ❚❤❡ ♦❜t❛✐♥❡❞ ❣r❛♣❤ △(ST P ) ✐s ✐••✉str❛t❡❞ ✐♥ ❋✐❣✳✹✳ ❋✐❣✉r❡ ✹✿ ❈♦♠♣♦s✐t❡ ♣r♦❞✉❝t ❙❚P ❚❤❡r❡ ❛r❡ t✇♦ ♣♦ss✐❜•❡ △(ST P ) ❣❡♥❡r❛t✐♦♥ ♦r❞❡rs✿ ❋✐❣✳✹✲❛ ❝♦rr❡s♣♦♥❞s t♦ t❤❡ ❝❛s❡ ✇❤❡r❡ ✐♥ ❜r❛♥❝❤✐♥❣ st❛t❡ (2, 0, 1, ε, cnr)✱ l2?cnr ✐s ❣❡♥❡r❛t❡❞ ✜rst ♦t❤❡r t❤❛♥ U 1?Close✳ ❆s t❤❡ tr❛♥s✐t✐♦♥s ❢♦••♦✇✐♥❣ l2?cnr ❤❛✈❡ r❡❛❝❤❡❞ Accept △(ST P ) ✱ t❤❡r❡ ✐s ♥♦ ♥❡❡❞ t♦ ❢✉rt❤❡r ❣❡♥❡r❛t❡ ✐ts ❝♦♥✢✐❝t ❛❝t✐♦♥ ❯✶❄❈•♦s❡✳ ❖♥ t❤❡ ❝♦♥tr❛r②✱ ❋✐❣✳✹✲❜ ✐••✉str❛t❡s t❤❡ ❝❛s❡ ✇❤❡r❡ ❯✶❄❈•♦s❡ ✐s ❡①♣•♦r❡❞ ❜❡❢♦r❡ l2?cnr✳ ■♥ t❤✐s ❝❛s❡✱ ♠♦r❡ st❛t❡s ❛r❡ ❡①♣•♦r❡❞ t♦ r❡❛❝❤ Accept △(ST P ) ✳ ■♥ ❜♦t❤ ✜❣✉r❡s✱ t❤❡ ❜♦•❞ ♣❛rts ❛r❡ t❤❡ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ♦❜t❛✐♥❡❞ ❜② ❆❝❝❡♣t❴♣❛t❤❴❝❛•❝✉•❛t✐♦♥✳ ■♥❞❡❡❞✱ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s r❡♣r❡s❡♥ts t❤❡ ❞❡t❛✐•❡❞ ✐♥t❡r❛❝t✐♦♥ ♦❢ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s ❢r♦♠ t❤❡✐r ✐♥✐t✐❛• st❛t❡s t♦ r❡❛❝❤ t❤❡ ♦❜•❡❝t✐✈❡ ❞❡✜♥❡❞ ❜② t❤❡ ■❚P ✭❆❝❝❡♣t ❛ttr✐❜✉t❡✮✳ ❲❡ ❝❛♥ s❡❡ t❤❛t ✐♥ ❋✐❣✳✹✲❜✱ st❛t❡ (0, 0, 1, ε, cnr) ❝♦♥t❛✐♥s ❝♦♥✢✐❝t ❛❝t✐♦♥s ❯✶✦❈◆| ❛♥❞ L2?cnr✳ ❈♦♥✢✐❝t tr❛♥s✐t✐♦♥s ✇✐•• ❜❡ ♣r✉♥❡❞ •❛t❡r ✐♥ ❛ ❜❛❝❦tr❛❝❦✐♥❣ ✇❛②✳ ❇❡s✐❞❡s✱ ❛•• t❤❡ q✉✐❡s❝❡♥❝❡s ❛r❡ ♣r❡s❡r✈❡❞ ❞✉r✐♥❣ ❛s②♥❝❤r♦♥♦✉s s♣❡❝✐✜❝❛t✐♦♥s ✐♥t❡r❛❝t✐♦♥✱ ✐♥❞✐❝❛t✐♥❣ t❤❛t ✐♥ t❤❡s❡ ❝♦♠♣♦s✐t❡ st❛t❡s✱ s♣❡❝✐✜❡❞ q✉✐❡s❝❡♥❝❡s ❛r❡ ❛✉t❤♦r✐③❡❞✳ ✾ ✸✳✹ ❚❡st ❈❛s❡ ▼✐♥✐♠✐③❛t✐♦♥ ❚❤❡ ❞❡r✐✈❛t✐♦♥ ♦❢ ❛♥ ❡①❡❝✉t❛❜•❡ ✐♦♣ t❡st ❝❛s❡ ✐♥✈♦•✈❡s ✐♥ ♣❡r❢♦r♠✐♥❣ t❤❡ ❢♦••♦✇✐♥❣ ✐♥str✉❝t✐♦♥s t♦ ❡①tr❛❝t ❛ s✉❜❣r❛♣❤ ❢r♦♠ △(ST P )✳ ❖❜s❡r✈❛❜•❡ ❜❡❤❛✈✐♦r ❡①tr❛❝t✐♦♥ ❋✐rst✱ ✐♦♣ t❡st ❝❛s❡ ♠✐♥✐♠✐③❛t✐♦♥ ✐♥✈♦•✈❡s ✐♥ ❡①tr❛❝t✐♥❣ t❤❡ ♦❜s❡r✈❛❜•❡ ❜❡❤❛✈✐♦r ❢r♦♠ △(ST P ) ✇❤✐•❡ ♠❛s❦✐♥❣ t❤❡ ♥♦♥✲♦❜s❡r✈❛❜•❡ ❛❝t✐♦♥s✳ ❆s ✐♥ ✐♦♣ t❡st✐♥❣✱ ❡❛❝❤ ✐♠♣•❡♠❡♥t❛t✐♦♥ ✐s s❡❡♥ ❛s ❛ ❜•❛❝❦ ❜♦①✱ ❛♥ ✐♥♣✉t ♦❢ ■❯❚ ✐s ✐♥ ❢❛❝t ❛♥ ✐♥t❡r♥❛• ❡✈❡♥t t❤❛t ❝❛♥♥♦t ❜❡ ❞✐r❡❝t•② ♦❜s❡r✈❡❞✳ ❚❤❡r❡❢♦r❡✱ ✇❡ r❡♣•❛❝❡ t❤❡s❡ ❛❝t✐♦♥s ❜② τ ✳ ❚❤❡♥✱ ♦❜s❡r✈❛❜•❡ ❜❡❤❛✈✐♦r ♦❢ △(ST P ) ✐s ❡①tr❛❝t❡❞ ❜② ❛♣♣•②✐♥❣ τ ✲ r❡❞✉❝t✐♦♥ ❬✶✹(✱ ✇❤✐❝❤ ❤✐❞❡s ✐♥t❡r♥❛• ❛❝t✐♦♥s τ ❢r♦♠ t❤❡ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t ❢♦••♦✇❡❞ ❜② ❞❡t❡r♠✐♥✐③❛t✐♦♥✳ ❈♦♥✢✐❝t ♣r✉♥✐♥❣ P♦ss✐❜•❡ ❝♦♥✢✐❝ts ✐♥ △(ST P ) s❤♦✉•❞ ❜❡ ♣r✉♥❡❞✱ ✇❤✐❝❤ ❝❛♥ ❜❡ ❞♦♥❡ ✐♥ ❛ ❜❛❝❦tr❛❝❦✐♥❣ ♠❛♥♥❡r✳ ❚❤❡ tr❛♥s✐t✐♦♥s t❤❛t ❝❛♥ ♥♦t •❡❛❞ t♦ ❆❝❝❡♣t ❛ttr✐❜✉t❡s ❛r❡ ♣r✉♥❡❞✳ ◗✉✐❡s❝❡♥❝❡ r❡❞✉❝t✐♦♥ ◆♦t ❛•• t❤❡ q✉✐❡s❝❡♥❝❡s ❛r❡ ❦❡♣t✳ ◗✉✐❡s❝❡♥❝❡ ✐s ♦♥•② ❦❡♣t ❛t st❛t❡s ❝♦♥t❛✐♥✐♥❣ ♦✉t♣✉ts ❜✉t ♥♦t st✐♠✉•✐ ✭st✐♠✉•✐ ❛r❡ s❡♥t ❜② t❤❡ t❡st❡r✮✳ ▼♦r❡♦✈❡r✱ tr❛♣ st❛t❡s ❞♦ ♥♦t ♥❡❡❞ t♦ ✐♥❞✐❝❛t❡ q✉✐❡s❝❡♥❝❡✱ ❜❡❝❛✉s❡ t❤❡ tr❛♣ st❛t❡s ✐♥ ❛♥ ■❚❈ ❛r❡ t❤❡ ✈❡r❞✐❝ts✳ ✸✳✺ ❱❡r❞✐❝ts ❆ss✐❣♥♠❡♥t ❚♦ ♦❜t❛✐♥ ❛♥ ❡①❡❝✉t❛❜•❡ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡✱ ✈❡r❞✐❝ts s❤♦✉•❞ ❜❡ ❛ss✐❣♥❡❞✳ ❆ ✈❡r❞✐❝t ✐s t❤❡ r❡s✉•t ♦❢ t❤❡ ❡①❡❝✉t✐♦♥ ♦❢ ❛ t❡st ❝❛s❡✳ ■t ✐s ❞❡t❡r♠✐♥❡❞ ❜② t❤❡ ❝♦♠♣❛r✐s♦♥ ❜❡t✇❡❡♥ t❤❡ ❛❝t✉❛• ❜❡❤❛✈✐♦r ♦❢ t❤❡ ❙❯❚ ❞✉r✐♥❣ t❡st ❝❛s❡ ❡①❡❝✉t✐♦♥ ❛♥❞ ✐ts ❡①♣❡❝t❡❞ ❜❡❤❛✈✐♦r✳ ■♥ ❣❡♥❡r❛•✱ t❤❡r❡ ❡①✐st t❤❡ ❢♦••♦✇✐♥❣ t②♣❡s ♦❢ ✈❡r❞✐❝ts✳ ✶✳ P❛ss✿ ❚❤❡ ♦❜s❡r✈❡❞ ❜❡❤❛✈✐♦r ♦❢ ❙❯❚ ✐s ❝♦rr❡❝t ❛♥❞ t❤❡ ✐♦♣ t❡st ♣✉r♣♦s❡ ✐s r❡❛❝❤❡❞✳ ✷✳ ■♥❝♦♥❝•✉s✐✈❡✿ ❚❤❡ ♦❜s❡r✈❡❞ ❜❡❤❛✈✐♦r ✐s ❝♦rr❡❝t✱ ❤♦✇❡✈❡r ❞♦❡s ♥♦t ❝♦rr❡s♣♦♥❞ t♦ t❤❡ t❡st ♣✉r♣♦s❡ ✸✳ ❋❛✐•✿ ❆t •❡❛st ❛♥ ❡rr♦r ✐s ❞❡t❡❝t❡❞✳ ❚♦ ❛ss♦❝✐❛t❡ t❤❡ ❣r❛♣❤ ✇✐t❤ ✈❡r❞✐❝ts✱ t❤❡ ❛•❣♦r✐t❤♠ t❛❦❡s ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ❛♥❞ △(ST P ) ❛s ✐♥♣✉ts✳ ❋♦r ❡❛❝❤ st❛t❡ v ∈ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ✱ t❤❡ ❢♦••♦✇✐♥❣ ❝♦♥❞✐t✐♦♥s ❛r❡ ❝❤❡❝❦❡❞✿
✶✳ ❋♦r v∈ Accept △(ST P ) ✱ v ✐s ❛ss♦❝✐❛t❡❞ ✇✐t❤ ✈❡r❞✐❝t P ass✿ P ass =④v| u ∈❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s✱ v∈ Accept △(ST P ) ✱ a ∈ • q✳✈✐s✐t❡❞ ✿ ❚❤❡ s❡t ♦❢ t❤❡ tr❛♥s✐t✐♦♥s ❛t st❛t❡ q t❤❛t ❤❛✈❡ ❛•r❡❛❞② ❜❡❡♥ ❣❡♥❡r❛t❡❞✳

Σ △(ST P ) ✱ u a -→ △(ST P ) v⑥✳ ✷✳ ❋♦r v ∈ Accept △(ST P ) t❤❛t ❛••♦✇s ❛♥ ♦✉t♣✉t r❡❛❝❤✐♥❣ ❛ st❛t❡ ✐♥ △(ST P ) ❜✉t ♥♦t ❝♦♥t❛✐♥❡❞ ✐♥ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ✐ts❡•❢✱ ❛ ♥❡✇ tr❛♥s✐t✐♦♥ ✇✐t❤ ✈❡r❞✐❝t ■♥❝♦♥❝•✉s✐✈❡ ❛♥❞ t❤❡ ❛••♦✇❡❞ ♦✉t♣✉t ✐s ❛❞❞❡❞✳ Inconclusive ❂④u|∃v ∈ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ✱u ∈ Q △(ST P ) ∩ u / ∈ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ✱ a ∈ Γ(v), v a -→ △(ST P ) u⑥✳ ✸✳ ■❢ ❛ st❛t❡ v ✇❤✐❝❤ ❝♦✉•❞ ❤❛✈❡ ❛♥ ✉♥❡①♣❡❝t❡❞ ♦✉t♣✉t ✐♥ ❡✐t❤❡r S1 ♦r S2✳ ❆ ♥❡✇ tr❛♥s✐t✐♦♥ ✇✐t❤ ❡✈❡♥t ıotherwise✑ ❛♥❞ ✈❡r❞✐❝t F ail ✐s ❛❞❞❡❞✳ (v, otherwise, F ail) ✇❤❡r❡ F ail =④u|v ∈ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ✱otherwise / ∈ Σ △(ST P ) O ,¬(v otherwise -→ △(ST P ) u)⑥✳ ❚❤❡ •❛❜❡• ❖t❤❡r✇✐s❡ r❡♣r❡s❡♥ts ✉♥❡①♣❡❝t❡❞ ♦✉t♣✉ts ❛s ✇❡•• ❛s t❤❡ t✐♠❡♦✉t ♥♦♥ s♣❡❝✐✜❡❞ ❛t t❤❡s❡ st❛t❡s✳ ✐✳❡✳✱ s♣❡❝✐✜❡❞ t✐♠❡♦✉t ✐s t♦•❡r❛t❡❞✳ ✸✳✻ ■♦♣ ❚❡st ❈❛s❡ ❇② ❛♣♣•②✐♥❣ t❤❡ △(ST P ) ❝♦♥str✉❝t✐♦♥✱ ✐♦♣ t❡st ❝❛s❡ ❞❡r✐✈❛t✐♦♥ ❛♥❞ ♠✐♥✐♠✐③❛t✐♦♥✱ ❛s ✇❡•• ❛s ✈❡r❞✐❝t ❛ss✐❣♥♠❡♥t ❛•❣♦r✐t❤♠s✱ ❛♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡ ✐s ♦❜t❛✐♥❡❞✱ ✇❤✐❝❤ st❛♥❞s ❢♦r t❤❡ ❞❡t❛✐•❡❞ s❡t ♦❢ ✐♥str✉❝t✐♦♥s t❤❛t ♥❡❡❞ t♦ ❜❡ t❛❦❡♥ ✐♥ ♦r❞❡r t♦ ♣❡r❢♦r♠ t❤❡ t❡st ✇✳r✳t t❤❡ ■❚P✳ ❉❡✜♥✐t✐♦♥ ✺ ■♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡ ✐s ❛ s✉s♣❡♥s✐♦♥ ■❖▲❚❙ △(IT C)❂✭Q △(IT C) , Σ △(IT C) ✱ T △(IT C) ✱ q △(IT C) 0 ✮ ✇❤❡r❡ • Q △(IT C) = Accept❴path❴states∪P ass∪Inconclusive∪F ail ✳ ④P❛ss✱ ❋❛✐•✱ ■♥❝♦♥❝•✉s✐✈❡ ⑥❛r❡ t❤❡ tr❛♣ st❛t❡s ♦❢ △(IT C)✱ r❡♣r❡✲ s❡♥t✐♥❣ t❤❡ ♣♦ss✐❜•❡ ✈❡r❞✐❝ts ♦❢ ❛ t❡st ❡①❡❝✉t✐♦♥✳ • Σ △(IT C) ⊆④(Σ △(S 1 ) U ∪ Σ △(S 2 ) U ✮∪(Σ △(S 1 ) O L ∪ Σ △(S 2 ) O L )∪ otherwise⑥ ✐s t❤❡ s❡t ♦❢ ❛•♣❤❛❜❡ts✳ • T △(IT C) ❂ Accept❴path❴transitions ∪ T Inconclusive ∪ T F ail ✳ ❆♥ ✐♦♣ t❡st ❝❛s❡ s❤♦✉•❞ ♠❡❡t t❤❡ ❢♦••♦✇✐♥❣ ♣r♦♣❡rt✐❡s✿ ❈♦••❡❝t✐♦♥ ❞❡s P✉❜•✐❝❛t✐♦♥s ■♥t❡r♥❡s ❞❡ •✬■r✐s❛ ❝ ■|■❙❆ ✶✵ ◆✳ ❈❤❡♥ ✶✳ ❋r♦♠ ❛♥② st❛t❡ ✐♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡s✱ ❛ ✈❡r❞✐❝t ♠✉st ❜❡ ❛❝❝❡ss✐❜•❡✿ ∀q ∈ Q △(IT C) ,
❛♥❞ ♦✈❡r✢♦✇ ❝❛♥ ❜❡ ❞❡t❡❝t❡❞✳ ❆•s♦✱ t❤❡ ❝♦♥s✐st❡♥❝② ♦❢ ■❚P ❝❛♥ ❜❡ ✈❡r✐✜❡❞✳ ❯s✐♥❣ t❤❡ ❛♣♣r♦❛❝❤ ♣r♦♣♦s❡❞✱ t❤❡ ❣❡♥❡r❛t❡❞ ✐♦♣ t❡st ❝❛s❡ ✐s ♥♦♥✲❜✐❛s❡❞✳ ✐✳❡✳✱ ∀I 1 ✱ I 2 t✇♦ ■❯❚s✱ ✐❢ σ∈ ❚r❛❝❡s ✭I 1 A I 2 ✮ ✐s ♣r♦❞✉❝❡❞ ❜② ❙❯❚ ❞✉r✐♥❣ t❤❡ ❡①❡❝✉t✐♦♥ ♦❢ ✐♦♣ t❡st ❝❛s❡✱ ✈❡r❞✐❝t F ail ✐s r❛✐s❡❞ ✐❢ ❛♥❞ ♦♥•② ✐❢ ¬✭I 1 iop G I 2 ✮✳ ❚❤❡ ♥♦♥✲❜✐❛s❡❞ ♣r♦♣❡rt② ❝❛♥ ❜❡ ❞✐✈✐❞❡❞ ✐♥t♦ t❤❡ ❢♦••♦✇✐♥❣ t✇♦ ♣r♦♣♦s✐t✐♦♥s✿ Pr♦♣♦s✐t✐♦♥ ✶ ∀I 1 ✱ I 2 t✇♦ ■❯❚s✱ ✐❢ t❤❡ ❛♣♣•✐❝❛t✐♦♥ ♦❢ ❛ ❣❡♥❡r❛t❡❞ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡ ♣r♦❞✉❝❡s ❛ ❋❛✐• ✈❡r❞✐❝t✱ t❤❡♥ ¬(I 1 iop G I 2 )✳ ▲❡t ✐♦♣ t❡st ❝❛s❡ ❛♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡ ❣❡♥❡r❛t❡❞ ❢r♦♠ s♣❡❝✐✜❝❛t✐♦♥s S 1 ✱ S 2 ✱ ❛♥❞ ❛ ✈❛•✐❞ ■❚P✳ ❙t❛t❡ ❋❛✐• ✐♥ ✐♦♣ t❡st ❝❛s❡ s♣❡❝✐✜❡s t❤❛t ❋❛✐• ✈❡r❞✐❝t ✐s ♦♥•② ♣r♦❞✉❝❡❞ ❜② ❛♥ ♦❜s❡r✈❛❜•❡ ❛❝t✐♦♥ ✇❤✐❝❤ ✐s ♥♦t ❛••♦✇❡❞ ✐♥ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s✳ ▲❡t σ ❛ tr❛❝❡ ♣r♦❞✉❝❡❞ ❜② t❤❡ ❙❯❚ ❞✉r✐♥❣ t❤❡ ❡①❡❝✉t✐♦♥ ♦❢ ✐♦♣ t❡st ❝❛s❡✱ ✈❡r❞✐❝t ✭σ✱ ❙❯❚✮❂✈❡r❞✐❝t ✭✐♦♣ t❡st ❝❛s❡ ❛❢t❡r σ✮✳ ❆s ✐♦♣ t❡st ❝❛s❡ ✐s ❞❡t❡r♠✐♥✐st✐❝✱ t❤✉s ✐♦♣ t❡st ❝❛s❡ ❛❢t❡r σ ✐s ✉♥✐q✉❡✳ ▼♦r❡♦✈❡r✱ ❛❝❝♦r❞✐♥❣ t♦ t❤❡ ❢♦r♠❛• ✐♥t❡r♦♣❡r❛❜✐•✐t② ❞❡✜♥✐t✐♦♥ ✭ ❝❢✳ ❉❡✜♥✐t✐♦♥ ✷ ✮✱ ✐❢ I 1 iop G I 2 ❂ ∀σ∈ ❙❚r❛❝❡s ✭S 1 A S 2 ✮✱ ❖✉t✭I 1 A I 2 ✱ σ✮ ⊆ ❖✉t✭△✭S 1 A S 2 ✮✱ σ✮✳ ❚❤❡r❡❢♦r❡✱ ✈❡r❞✐❝t ✭✐♦♣ t❡st ❝❛s❡ ❛❢t❡r σ✮ =❋❛✐•✳ ✈❡r❞✐❝t ✭σ✱ ❙❯❚✮ =❋❛✐•✳ Pr♦♣♦s✐t✐♦♥ ✷ ∀I 1 ✱ I 2 t✇♦ ■❯❚s✱ ✐❢ ¬(I 1 iop G I 2 )✱ t❤❡♥ t❤❡ ❛♣♣•✐❝❛t✐♦♥ ♦❢ ✐♦♣ t❡st ❝❛s❡ ♣r♦❞✉❝❡s ❛ ❋❛✐• ✈❡r❞✐❝t✳ ❖♥ t❤❡ ❝♦♥tr❛r② ♦❢ ✐♦♣ t❡st ❝❛s❡✱ ✇❤✐❝❤ ✐s ❞❡t❡r♠✐♥✐st✐❝✱ ✐♠♣•❡♠❡♥t❛t✐♦♥s ❝❛♥ ❜❡ ♥♦♥ ❞❡t❡r♠✐♥✐st✐❝✳ ❚❤✉s t❤❡ ❛♣♣•✐❝❛t✐♦♥ ♦❢ t❤❡ s❛♠❡ ✐♦♣ t❡st ❝❛s❡ ♠❛② ♣r♦❞✉❝❡ ❞✐✛❡r❡♥t ✈❡r❞✐❝ts✳ ❚❤✉s✱ ✇❡ ❛ss✉♠❡ ❛ ❜♦✉♥❞❡❞ ❢❛✐r♥❡ss ❤②♣♦t❤❡s✐s ♦♥ ✐♠♣•❡♠❡♥t❛✲ t✐♦♥s✱ ✇❤✐❝❤ ✐♠♣•✐❡s t❤❛t ❛ ❜♦✉♥❞❡❞ ♥✉♠❜❡r ♦❢ ❡①❡❝✉t✐♦♥s ♦❢ ❛ ♥♦♥ ❞❡t❡r♠✐♥✐st✐❝ ✐♠♣•❡♠❡♥t❛t✐♦♥ ✇✐•• s❤♦✇ ❛•• ✐ts ❜❡❤❛✈✐♦r✳ ✶✶ ❚❤❡r❡❢♦r❡✱ ❢♦r ❛ tr❛❝❡ σ ✇❤✐❝❤ ❝♦♥tr❛❞✐❝ts t❤❡ ✐♥t❡r❛❝t✐♦♥ ♦❢ S 1 ❛♥❞ S 2 ✱ ✈❡r❞✐❝t ✭✐♦♣ t❡st ❝❛s❡ ❛❢t❡r σ✮=❋❛✐• ✇✐•• ❜❡ r❛✐s❡❞ ❜② r❡♣❡❛t✐♥❣ ✐♦♣ t❡st ❝❛s❡✳ ❍♦✇❡✈❡r✱ t❤❡ ♣r♦♣♦s❡❞ ♠❡t❤♦❞ ❤❛s s♦♠❡ •✐♠✐t❛t✐♦♥s✿ ■♥ t❤❡ ✇♦rst ❝❛s❡✱ t❤❡ ♠❡t❤♦❞ ❞♦❡s ♥♦t r❡❞✉❝❡ t❤❡ ❣•♦❜❛• st❛t❡ s♣❛❝❡✳ ▼♦r❡♦✈❡r✱ t❤❡ ❛♣♣r♦❛❝❤ ♥❡❡❞s t❤❛t ❆❝❝❡♣t ❛ttr✐❜✉t❡ ♠✉st ♥♦t ❜❡ ❛ss✐❣♥❡❞ t♦ t✇♦ ❝♦♥✢✐❝t ❛❝t✐♦♥s✱ ♦t❤❡r✇✐s❡ ♦♥❡ ♦❢ t❤❡♠ ✇✐•• ♥♦t ❜❡ ❞❡✈❡•♦♣❡❞ ✭❝♦♥✢✐❝t tr❛♥s✐t✐♦♥s ❛r❡ ❝✉t ❞✉r✐♥❣ ❙❚P ❣❡♥❡r❛t✐♦♥✮✳ ✐✳❡✳✱ t❤❡ ❛♣♣r♦❛❝❤ ✐s ♦♥•② s✉✐t❛❜•❡ ❢♦r s✐♥❣•❡✲st✐♠✉•✐ ✐♦♣ t❡st✐♥❣✳ ✺ ❈♦♥❝•✉s✐♦♥ ❛♥❞ ❋✉t✉r❡ ❲♦r❦ ❚❤✐s r❡♣♦rt ♣r❡s❡♥ts ❛♥ ❛♣♣r♦❛❝❤ ♦❢ ❛✉t♦♠❛t✐❝ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❣❡♥❡r❛t✐♦♥✳ ❇❛s❡❞ ♦♥ ❢♦r♠❛• ✐♥t❡r♦♣❡r❛❜✐•✐t② s♣❡❝✐✜❝❛✲ t✐♦♥s✱ t❤❡ ❛♣♣r♦❛❝❤ ❛ss♦❝✐❛t❡s t❤❡ ❛s②♥❝❤r♦♥♦✉s ❝❛•❝✉•❛t✐♦♥ ♦❢ s♣❡❝✐✜❝❛t✐♦♥s ✇✐t❤ r❡s♣❡❝t t♦ ❛♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ♣✉r♣♦s❡✳ ❋♦r ❡❛❝❤ ✐♦♣ t❡st ♣✉r♣♦s❡✱ ❛♥ ✐♦♣ t❡st ❝❛s❡ ✐s ❞❡✈❡•♦♣❡❞✳ ❲❡ ❤❛✈❡ ❢♦r♠❛••② ❞❡✜♥❡❞ t❤❡ r✉•❡s ❛••♦✇✐♥❣ ❜✉✐•❞✐♥❣ ❛ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t △(ST P ) ♦❢ s♣❡❝✐✜❝❛t✐♦♥s ❛♥❞ t❤❡ ■❚P✱ ❢r♦♠ ✇❤✐❝❤ ❛♥ ✐♦♣ t❡st ❝❛s❡ ❝❛♥ ❜❡ ❞❡r✐✈❡❞✳ ❚♦ r❡•✐❡✈❡ st❛t❡ ❡①♣•♦r❛t✐♦♥✱ ✇❡ ❤❛✈❡ ❛♣♣•✐❡❞ ❛ s✉✐t❡ ♦❢ str❛t❡❣✐❡s✿ ✭✐✮ ❊❛❝❤ t❡st ♦❜•❡❝t✐✈❡ ✐s ❛ss✐❣♥❡❞ ✇✐t❤ ❆❝❝❡♣t ❛♥❞ |❡❢✉s❡ ❛ttr✐❜✉t❡s t♦ •✐♠✐t st❛t❡ ❡①♣•♦r❛t✐♦♥✳ ✭✐✐✮ ❉❡♣t❤✲✜rst △(ST P ) ❝♦♥str✉❝t✐♦♥ ❦❡❡♣s ♦♥•② t❤❡ ❡✈❡♥ts r❡•❡✈❛♥t t♦ t❤❡ t❡st ♦❜•❡❝t✐✈❡ ✭✐✐✐✮ ❙t❛t❡s ✇✐t❤ ❝♦♥✢✐❝ts ❛r❡ ❛♣♣•✐❡❞ r✉•❡s t♦ ❛✈♦✐❞ ❣❡♥❡r❛t✐♥❣ ❝❡rt❛✐♥ ❝♦♥✢✐❝t tr❛♥s✐t✐♦♥s✳ ❋✐♥❛••②✱ ✇❡ ❤❛✈❡ ❞❡✜♥❡❞ ✈❡r❞✐❝ts ❛ss✐❣♥♠❡♥t ❛♥❞ t❡st ❝❛s❡ ♠✐♥✐♠✐③❛t✐♦♥ r✉•❡s t♦ ❝♦♥str✉❝t ❛♥ ❡①❡❝✉t❛❜•❡ ✐♦♣ t❡st ❝❛s❡✳ ❇❡s✐❞❡s✱ t❤❡ ❝♦♥str✉❝t❡❞ ✐♦♣ t❡st ❝❛s❡ r❡s♣❡❝ts t❤❡ ✉♥❜✐❛s❡❞ ♣r♦♣❡rt②✳ ✐✳❡✳ ✈❡r❞✐❝t F ail ✐s r❛✐s❡❞ ✐✛ ¬✭I 1 iop G I 2 ✮✳ ❍♦✇❡✈❡r✱ t❤❡ ❛♣♣r♦❛❝❤ ✐s s✉✐t❛❜•❡ ❢♦r s✐♥❣•❡ st✐♠✉•✐ ✐♦♣ t❡st ❝❛s❡ ❣❡♥❡r❛t✐♦♥✳ ▼♦r❡♦✈❡r✱ ✐♥ t❤❡ ✇♦rst ❝❛s❡✱ t❤❡ st❛t❡✲s♣❛❝❡ ❡①♣•♦s✐♦♥ ♣r♦❜•❡♠ st✐•• ❡①✐sts✳ ❋✉t✉r❡ ✇♦r❦ ✇✐•• ❜❡ ❢♦❝✉s ♦♥ r❡s❡❛r❝❤✐♥❣ ❜❡tt❡r ♠❡t❤♦❞s t♦ s♦•✈❡ st❛t❡✲s♣❛❝❡ ❡①♣•♦s✐♦♥ ♣r♦❜•❡♠✱ ❛s ✇❡•• ❛s ♦♥ ❡①t❡♥❞✐♥❣ t❤✐s s♦•✉t✐♦♥ t♦ ♠✉•t✐✲❝♦♠♣♦♥❡♥t ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st✐♥❣✳ ❆♣♣❡♥❞✐① ❆ ❆✳✶ ❉❡♣t❤✲✜rst △(ST P ) ❝♦♥str✉❝t✐♦♥✿ • Current : ❚❤❡ ❝✉rr❡♥t st❛t❡ ✉♥❞❡r ❝♦♥str✉❝t✐♦♥✳ ■♥✐t✐❛••②✱ ❈✉rr❡♥t✿ ❂ q △(ST P ) 0 ✳ • |✉•❡s✭q✮✿ ❋✉♥❝t✐♦♥ |✉•
• ❆❝❝❡♣t❴♣❛t❤❴st❛t❡s ✴ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s✿ ❚❤❡ s❡t ♦❢ st❛t❡s ✴ tr❛♥s✐t✐♦♥s ✐♥ t❤❡ ♣❛t❤ tr❛✈❡rs✐♥❣ q △(ST P ) 0 ❛♥❞ Accept △(ST P ) ✳

• ❈r❡❛t❡❴tr❛♥s✐t✐♦♥ ✭❙❚P✱ ✭q✱ ♣✮✮✿ •❡♥❡r❛t❡ ❛ tr❛♥s✐t✐♦♥ ❢r♦♠ st❛t❡ q t♦ st❛t❡ ♣ ✐♥ ❙❚P✳

  ∃σ s✉❝❤ t❤❛t ❢♦r p ∈ ④P❛ss✱ ❋❛✐•✱ ■♥❝♦♥❝•✉s✐✈❡ ⑥✱q σ -→ △(IT C) p✳ ✷✳ ❆ t❡st ❝❛s❡ ✐s ♥♦♥✲❜✐❛s❡❞ ✇✳r✳t t❤❡ s♣❡❝✐✜❝❛t✐♦♥s ❛♥❞ ❣•♦❜❛• ✐♦♣ ❝r✐t❡r✐♦♥✿ ∀I1✱ I2 t✇♦ ■❯❚s✱ ✐❢ σ∈ ❙❚r❛❝❡s ✭I1 AI2✮ ✐s ♣r♦❞✉❝❡❞ ❜② ❙❯❚ ❞✉r✐♥❣ t❤❡ ❡①❡❝✉t✐♦♥ ♦❢ △(IT C)✱ ✈❡r❞✐❝t ❋❛✐• ✐s r❛✐s❡❞ ✐✛ ¬✭I1iopGI2✮✳ ❊①❛♠♣•❡ ✸ ❆♣♣•②✐♥❣ t❤❡ ✈❡r❞✐❝t ❛ss✐❣♥♠❡♥t r✉•❡s ❛♥❞ t❡st ❝❛s❡ ♠✐♥✐♠✐③❛t✐♦♥ ♦♥ ❋✐❣✳✹✲❜✱ ❛♥ ✐♦♣ t❡st ❝❛s❡ ✐s ❣❡♥❡r❛t❡❞✿ ❈♦♥✢✐❝t tr❛♥s✐t✐♦♥s t❤❛t ❝❛♥ ♥♦t •❡❛❞ t♦ t❤❡ ❆❝❝❡♣t ❛ttr✐❜✉t❡ ❛r❡ ♣r✉♥❡❞✱ ✇❤✐•❡ ✈❡r❞✐❝ts ❛r❡ ❛ss♦❝✐❛t❡❞✳ ❋✐❣✉r❡ ✺✿ ❆ s✐♠♣•✐✜❡❞ ❝♦♥♥❡❝t✐♦♥ ♣r♦t♦❝♦• ■❚❈ ✹ |❡s✉•ts •✐✈❡♥ ❛♥ ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ♣✉r♣♦s❡ ■❚P ❛♥❞ t✇♦ s✉s♣❡♥s✐♦♥ s♣❡❝✐✜❝❛t✐♦♥s △(S 1 )✱ △(S 2 )✳ ❚❤❡ ♣r♦♣♦s❡❞ ❛♣♣r♦❛❝❤ ❝❛•❝✉✲ •❛t❡s t❤❡ ❝♦♠♣♦s✐t❡ ♣r♦❞✉❝t △(ST P )❂△(S 1 )×△(S 2 )×■❚P✳ ▼❡❛♥✇❤✐•❡✱ t❤❡ ♦❜s❡r✈❛❜•❡ ❡①♣❡❝t❡❞ ❜❡❤❛✈✐♦r t♦ ❜❡ ✈❡r✐✜❡❞ ✐s ❡①tr❛❝t❡❞✳ ❆t •❛st✱ ❛♥ ✐♦♣ t❡st ❝❛s❡ ✐s ❞❡r✐✈❡❞ ❛♥❞ ♠✐♥✐♠✐③❡❞ ✇❤✐•❡ P❛ss✱ ■♥❝♦♥❝•✉s✐✈❡ ❛♥❞ ❋❛✐• ✈❡r❞✐❝ts ❛r❡ ❛ss✐❣♥❡❞✳ ❲❡ ❤❛✈❡ ♠❛❞❡ ❡①♣❡r✐♠❡♥ts ❜② ✐♠♣•❡♠❡♥t✐♥❣ ❛•• t❤❡ ❛•❣♦r✐t❤♠s✱ ✐♥❝•✉❞✐♥❣ ❙❚P ❝♦♥str✉❝t✐♦♥ r✉•❡s✱ ❛❝❝❡♣t ♣❛t❤s ❡①tr❛❝t✐♦♥✱ t❡st ❝❛s❡ ♠✐♥✐♠✐③❛t✐♦♥ ❛♥❞ ✈❡r❞✐❝ts ❛ss✐❣♥♠❡♥ts✳ ❆♣♣•②✐♥❣ t❤❡s❡ ❛•❣♦r✐t❤♠s ♦♥ ❊①❛♠♣•❡ ✶✱ ✇❡ ♦❜t❛✐♥ ❛♥ △(ST P ) ♦❢ ✶✷ st❛t❡s ❛♥❞ ✶✸ tr❛♥s✐t✐♦♥s✳ ❲❤❡r❡❛s ❜② r❡❛❝❤❛❜•❡ ❛♥❛•②s✐s✱ ✻✻ st❛t❡s ❛♥❞ ✼✾ tr❛♥s✐t✐♦♥s ❛r❡ ❣❡♥❡r❛t❡❞✳ ■♥ ❢❛❝t✱ ❛♥ ■❚P t❤❛t ❝♦♥str❛✐♥ts t❤❡ ❜❡❤❛✈✐♦rs ❜② t❤❡ ✉s❡ ♦❢ ❆❝❝❡♣t ❛♥❞ |❡❢✉s❡ ❛••♦✇s q✉✐❝❦•② s②♥t❤❡s✐③❡ ❛♥ ✐♦♣ t❡st ❝❛s❡ ✇✐t❤♦✉t ❝❛•❝✉•❛t✐♥❣ ❛•• t❤❡ ❣•♦❜❛• ❜❡❤❛✈✐♦r✳ ❇❡s✐❞❡s✱ ❜② ❝❛•❝✉•❛t✐♥❣ t❤❡ •♦✐♥t ❜❡❤❛✈✐♦r ♦❢ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s✱ ❞❡s✐❣♥ ❡rr♦rs s✉❝❤ ❛s ✉♥s♣❡❝✐✜❡❞ ✐♥♣✉ts✱ ❞❡❛❞•♦❝❦ st❛t❡s

  ❡s✭q✮ r❡t✉r♥s t✇♦ ✈❛•✉❡s q✳s✉❝❝ ❛♥❞ q✳♥❜❴s✉❝❝✳ q✳s✉❝❝ ✐s t❤❡ s❡t ♦❢ t❤❡ s✉❝❝❡ss♦r st❛t❡s ♦❢ st❛t❡ q t❤❛t ❝❛♥ ❜❡ ❣❡♥❡r❛t❡❞ ❛❝❝♦r❞✐♥❣ t♦ t❤❡ ❛s②♥❝❤r♦♥♦✉s ✐♥t❡r❛❝t✐♦♥ ♦♣❡r❛t✐♦♥ r✉•❡s❀ ❲❤✐•❡ q✳♥❜❴s✉❝❝ ✐s t❤❡ ♥✉♠❜❡r ♦❢ t❤❡ s✉❝❝❡ss♦r st❛t❡s ♦❢ q✳

•✱

  ❊♥❞❴❊①♣•♦r❛t✐♦♥✿ ❇♦♦•❡❛♥ ❡q✉❛• t♦ ❚|❯❊ ✐✛ ♥♦ ♠♦r❡ st❛t❡ ❝❛♥ ❜❡ ❡①♣•♦r❡❞✳ • ❈♦♥✢✐❝t✿ ❇♦♦•❡❛♥ ❡q✉❛• t♦ ❚|❯❊ ✐✛ t❤❡ ❝✉rr❡♥t•② ❡①❛♠✐♥❡❞ r✉•❡ ❛t st❛t❡ q ✐s ❝♦♥✢✐❝t ✇✐t❤ ❛♥② ♦❢ t❤❡ ❡①✐st✐♥❣ •❛❜❡•s ❛t q ✳ • ❇r❛♥❝❤✿ ❆ st❛❝❦ t♦ st♦r❡ ❜r❛♥❝❤✐♥❣ st❛t❡s✳ ❇r❛♥❝❤ ✐♥✈♦•✈❡s t❤❡ ❢♦••♦✇✐♥❣ ♦♣❡r❛t✐♦♥s✿ P✉s❤ ❛❞❞s ❛ ♥❡✇ ✐t❡♠ t♦ t❤❡ t♦♣ ♦❢ ❇r❛♥❝❤✳ P♦♣ r❡♠♦✈❡s ❛♥ ✐t❡♠ ❢r♦♠ t❤❡ t♦♣ ♦❢ ❇r❛♥❝❤✳ ❙t❛❝❦t♦♣ r❡t✉r♥ t❤❡ ✈❛•✉❡ ♦❢ t❤❡ ✐t❡♠ ❢r♦♠ t❤❡ t♦♣ ♠♦st ♣♦s✐t✐♦♥ ♦❢ ❇r❛♥❝❤ ✇✐t❤♦✉t ❞❡•❡t✐♥❣ ✐t✳ • ❛❞❞ ✭s❡t✱ ①✮✿ ❛❞❞ ❛♥ ✐t❡♠ ① t♦ t❤❡ s❡t • ❝•❡❛r s❡t✿ r❡♠♦✈❡ ❛•• ❡•❡♠❡♥ts ✐♥ ❛ s❡t ❈♦••❡❝t✐♦♥ ❞❡s P✉❜•✐❝❛t✐♦♥s ■♥t❡r♥❡s ❞❡ •✬■r✐s❛ ❝ ■|■❙❆ ✶✷ ◆✳ ❈❤❡♥ ❆•❣♦r✐t❤♠ ✶✿ ❉❡♣t❤✲✜rst ∆(ST P ) ❈♦♥str✉❝t✐♦♥ ■♥♣✉t✿ △(S 1 )✱ △(S 2 )✱IT P ❖✉t♣✉t✿ △(ST P ) ■♥✐t✐❛•✐③❛t✐♦♥✿ Current❂q ST P 0 Branch❂❬(✱ ❈✉rr❡♥t✳✈✐s✐t❡❞ ❂❬ (✱ ❊♥❞❴❊①♣•♦r❛t✐♦♥❂❋❛•s❡ ❀ ✇❤✐•❡ ♥♦t ❊♥❞❴❊①♣•♦r❛t✐♦♥ ❞♦ |✉•❡s ✭❈✉rr❡♥t✮ ❀ ✴✴ ■❢ ♦♥•② ♦♥❡ r✉•❡ ❝❛♥ ❜❡ ❛♣♣•✐❡❞ ✐❢ ❈✉rr❡♥t✳♥❜❴s✉❝❝ ❂❂✶ t❤❡♥ ❈r❡❛t❡❴tr❛♥s✐t✐♦♥ ✭ △(ST P )✱ ✭❈✉rr❡♥t✱ ◆❡①t✮✮ ✇❤❡r❡ ◆❡①t∈ ❈✉rr❡♥t✳s✉❝❝❀ ❈✉rr❡♥t ❂ ◆❡①t ❡♥❞ ✴✴ ■❢ ❛t •❡❛st t✇♦ r✉•❡s ❝❛♥ ❜❡ ❛♣♣•✐❡❞ ✐❢ ❈✉rr❡♥t✳♥❜❴s✉❝❝❃❂✷ t❤❡♥ ✐❢ Current / ∈ Branch t❤❡♥ P✉s❤✭❇r❛♥❝❤✱❈✉rr❡♥t✮ ❡♥❞ ✐❢ ∃ ◆❡①t ✇❤❡r❡ ◆❡①t ∈ ❈✉rr❡♥t✳s✉❝❝ ∧ ✭❈✉rr❡♥t✱ ◆❡①t✮ / ∈ ❈✉rr❡♥t✳✈✐s✐t❡❞ t❤❡♥ ❛❞❞ ✭❈✉rr❡♥t✳✈✐s✐t❡❞✱ ✭❈✉rr❡♥t✱ ◆❡①t✮✮ ❀ ✐❢ Γ✭❈✉rr❡♥t✮ ❂ Ø ♦r Γ✭❈✉rr❡♥t✮ =Ø ∧ ♥♦t ❈♦♥✢✐❝t ♦r ✭Γ✭❈✉rr❡♥t✮ =Ø ∧ ❈♦♥✢✐❝t ❛♥❞ ∃ ③∈Γ✭❈✉rr❡♥t✮ ∩❆❝❝❡♣t❴♣❛t❤❴st❛t❡s ✮ t❤❡♥ ❈r❡❛t❡❴tr❛♥s✐t✐♦♥ ✭ △(ST P )✱ ✭❈✉rr❡♥t✱ ◆❡①t✮✮❀ ❈✉rr❡♥t ❂ ◆❡①t ❡♥❞ ❡♥❞ ✴✴ ❆•• r✉•❡s ❛t ❝✉rr❡♥t st❛t❡s ❤❛✈❡ ❜❡❡♥ ❝❤❡❝❦❡❞✿ ❡•s❡ P♦♣✭❇r❛♥❝❤✱ ❈✉rr❡♥t✮❀ ❈•❡❛r ❈✉rr❡♥t✳✈✐s✐t❡❞ ❀ ✐❢ Branch = ❬ ( t❤❡♥ ❈✉rr❡♥t ❂❙t❛❝❦t♦♣ ✭❇r❛♥r✉•❡ ❝❛♥ ❜❡ ❛♣♣•✐❡❞❀ ❡•s❡ ✐❢ q IT P Current ∈ Accept IT P t❤❡♥ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦✐♥s❂❆❝❝❡♣t❴♣❛t❤❴❝❛•❝✉•❛t✐♦♥✭❈✉rr❡♥t✱△(ST P )✮❀ ❆❝❝❡♣t P❛t❤ ❙❡❛r❝❤ ❊❛❝❤ t✐♠❡ ❛ st❛t❡ q ∈ Accept ∆(ST P ) ✐s r❡❛❝❤❡❞✱ ❢✉♥❝t✐♦♥ ❆❝❝❡♣t❴♣❛t❤❴❝❛•❝✉•❛t✐♦♥ ✐s ❝❛••❡❞ t♦ s❡❛r❝❤ ❛♥❞ ♠❛r❦ t❤❡ ♣❛t❤ t❤❛t tr❛✈❡rs❡s t❤❡ ✐♥✐t✐❛• st❛t❡ ♦❢ ∆(ST P ✮ ❛♥❞ t❤❡ st❛t❡ q✳ ❆❝❝❡♣t❴♣❛t❤❴❝❛•❝✉•❛t✐♦♥ ✐s ❜❛s❡❞ ♦♥ ❜❛❝❦tr❛❝❦✐♥❣✳ ✐✳❡✳✱ ❢r♦♠ st❛t❡ q✱ ❛ ❜❛❝❦✇❛r❞ s❡❛r❝❤ ✐s ❝❛rr✐❡❞ ♦✉t t♦ ✜♥❞ ❛•• tr❛♥s✐t✐♦♥s tr❛✈❡rs✐♥❣ q △(ST P ) 0 ❛♥❞ q✳ ❚❤❡ ❝❛•❝✉•❛t✐♦♥ ♣•❛②s t✇♦ r♦•❡s✿ ✭✐✮ ■t ✐♥❤✐❜✐ts ❝♦♥✢✐❝t tr❛♥s✐t✐♦♥ ❣❡♥❡r❛t✐♦♥✳ ■❢ ❛t ❜r❛♥❝❤✐♥❣ st❛t❡ q✱ t❤❡r❡ ❛•r❡❛❞② ❡①✐st s♦♠❡ tr❛♥s✐t✐♦♥s t❤❛t •❡❛❞ t♦ Accept ∆(ST P ) ✱ t❤❡♥ t❤❡r❡ ✐s ♥♦ ♥❡❡❞ t♦ ❣❡♥❡r❛t❡ ♦t❤❡r tr❛♥s✐t✐♦♥s t❤❛t ❝♦♥✢✐❝t ✇✐t❤ t❤❡ ❡①✐st✐♥❣ ♦♥❡s✳ ✭✐✐✮ ❆❝❝❡♣t❴♣❛t❤❴tr❛♥s✐t✐♦♥s ❛r❡ ✐♠♣♦rt❛♥t ✐♥t❡r♦♣❡r❛❜✐•✐t② t❡st ❝❛s❡ ❣❡♥❡r❛t✐♦♥ ❜❡❝❛✉s❡ t❤❡② st❛♥❞ ❢♦r t❤❡ ❜❡❤❛✈✐♦r ♦❢ t❤❡ ❙❯❚ ✇❤✐❝❤ •❡❛❞s t♦ P❛ss ✈❡r❞✐❝t✳

❈♦••❡❝t✐♦♥ ❞❡s P✉❜•✐❝❛t✐♦♥s ■♥t❡r♥❡s ❞❡ •✬■r✐s❛ ❝ ■|■❙❆


Guillaume Colin

Patrick Lanusse

Abdellah Louzimi

Yann Chamaillard

Chao Deng

Dominique Nelson Gruel

D Nelson-Gruel

Multi-SISO Robust Crone Design for the Air Path Control of a Diesel Engine

Keywords: Engine control, Diesel engine, Robust control, MIMO system, Crone control design 

établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

More stringent standards are being imposed to reduce the fuel consumption and pollutant emissions of compression ignition (CI) engines. Modern automobile engines must therefore meet the challenging, and often conflicting, goals of minimizing pollutant emissions and fuel consumption while satisfying driving performance over a wide range of operating conditions. This requires an "optimal" coordination of injection, turbocharger, and Exhaust Gas Recirculation (EGR) system under stationary and dynamic operation [START_REF] Guzzella | Control of Diesel Engines[END_REF]. From a control's point of view there are two important paths which have to be considered, namely: the fuel path and the air path (including EGR and turbocharger). In this paper, only the air path will be considered.

System description

The air intake of a turbocharged diesel engine, represented in Figure 1 can be described as follows. The compressor (pressure p boost ) produces a flow Q air from the ambient air. The compressor flow is cooled down by an intercooler and goes through the throttle Th into the intake manifold (pressure p man ). At the exhaust side, the exhaust flow is split in three parts: the turbine flow, the wastegate flow and the EGR flow. The turbine flow powers up the turbine and through a shaft drives the compressor. Thus, the supercharging pressure p boost can be adjusted by the turbine flow which is controlled by the wastegate WG. The EGR flow which goes back into the intake manifold can be adjusted by the EGR valve. The classical diesel engine control structure, as shown in Fig. 2, is used here. The driver fixes the fuel mass (which is linked to the torque). From the fuel mass and the engine speed, the set points for boost pressure p boost_sp and air flow Q air_sp are then generated. In this paper, the throttle is statically controlled and will be taken into account in future works. Hence, considering the air path control, the manipulated variables are the wastegate and the EGR valve and the controlled variables are the supercharging pressure p boost and the air flow Q air . The actuators have saturations which must be taken into account for the controller design.

Control strategy

While considering EGR and turbocharger control (i.e. without throttle control), some works can be found for the air path control of a diesel engine. Without being exhaustive, one can find these control methods applied to a diesel engine: Control Lyapunov Functions [START_REF] Van Nieuwstadt | EGR-VGT control schemes: experimental comparison for a high-speed diesel engine[END_REF]Jankovic and Kolmanovsky, 2000;[START_REF] Wahlström | Robust Nonlinear EGR and VGT Control with Integral Action for Diesel Engines[END_REF] ; Robust control and uncertainty parameterisation type [START_REF] Jung | Comparison of uncertainty parameterisations for robust control of turbocharged diesel engines[END_REF]; Nonlinear Internal Model Control (Nitsche et al, 2006); Gain scheduled control [START_REF] Wei | Gain Scheduled Hinf Control for Air Path Systems of Diesel Engines Using LPV Techniques[END_REF]; Predictive control [START_REF] Ortner | Predictive Control of a Diesel Engine Air Path[END_REF][START_REF] García-Nieto | Nonlinear predictive control based on local model networks for air management in diesel engines[END_REF]; Motion planning of the air and burned gas masses in the cylinder [START_REF] Chauvin | Motion planning for experimental airpath control of a Diesel HCCI engine[END_REF]. In the literature, robustness, fast tuning and low computational cost are not always ensured all together while these points are crucial for automotive applications. That is why, in this paper, we propose a method to design a computationally inexpensive robust control obtained faster and more systematically than the usual look-up-table based control, for a turbocharged diesel engine. [START_REF] Van Nieuwstadt | Decentralized and multivariable designs for EGR-VGT control of a diesel engines[END_REF] show that multivariable control design gives better results than decentralized control design for the air path control of a diesel engine. Hence, the idea in this paper is to investigate the multi-SISO Crone design, which is the design of a decentralized control that takes into account interactions of the full MIMO system. Section 2 presents this multi-SISO Crone control design methodology. The system identification and the control design are detailed in Section 3. In the last part of the paper, controller implementation and results are shown on our calibrated simulation model.

MULTI-SISO CRONE CONTROL DESIGN METHODOLOGY

SISO Crone design methodology

The CRONE control-system design methodology is a frequency-domain approach developed since the eighties [START_REF] Oustaloup | Systèmes asservis linéaires d'ordre fractionnaire[END_REF][START_REF] Oustaloup | [END_REF][START_REF] Oustaloup | The CRONE control of resonant plants: application to a flexible transmission[END_REF][START_REF] Lanusse | De la commande CRONE de première génération à la commande CRONE de troisième generation[END_REF][START_REF] Åström | Model uncertainty and robust control design[END_REF]. It is based on the common unity-feedback configuration. The principle of the third generation CRONE control methodology is to optimize the parameter of a nominal open-loop transfer function  0 (s) that includes a band-limited complex fractional order integration:

        s s s s h m l 0      , (1)
-where  m (s) is a set of band-limited generalized templates:

          N N k k s s m m   , (2)
with:

      k k k k k b -q b k k k a k k k b k k s s e s s C s sign i 1 /i 1 sign m 1 1 1 1                                                      0 for 2 1 1    k k k k    and 2 1 2 1 r 2 0 r 0 1 1                                   (3)
-where  l (s) is an integer order n l proportional integrator and where  h (s) is a low-pass filter of integer order n h :

  l - 1 - l l n N s C s             ,   h 1 h h n N s C s               . (4)
Gains C x (C k, C l and C h ) are such that  r is the closed-loop resonant frequency. Order n l has to be set to manage the accuracy provided by the control-system. Order n h has to be set to obtain a proper or bi-proper control. When it is useful, Nand N + are different from 0 to increase the number of tuning parameters. The open loop parameters are optimized in order to reduce the variation of the resonant peak M T of the complementary sensitivity function T(s). The following robustness cost function can be minimized:

2 0 T T 2 T 0 T up nf                   M M s M i M J G G , ( 5
)
where M T0 is a required value of the nominal closed loop resonant peak (for the nominal plant G 0 ), while respecting the following set of inequality constraints for all plants G and for

  + :       l j inf T T G  ,     T T G   u j sup  ,     S S G   u j sup      KS KS G   u j sup  and     GS GS G   u j sup  , (6)
with

                                               s K s G s G s GS s K s G s K s KS s K s G s S s K s G s K s G s T 1 1 1 1 1 . (7)
It is easy to show that the multiplicative uncertainty  m (s) of the open-loop frequency response, which defines the frequency-domain uncertainty in the Nichols chart, is invariant and equal to that of the plant:

                s G s s C s G Δ s G s K s G s m 0 m 0      (8)
where G 0 (s) and  0 (s) are the nominal plant and open-loop transfer functions and where  m G(s) (or  m (s)) is a multiplicative uncertainty model. Thus, the uncertainty frequency-domains related to the Nichols locus of  0 (j) are defined by all the possible values of the ordered pair

      dB m m j , j arg   G Δ G Δ
. By minimizing J (5), the optimal parameters position the uncertainty frequency domains so that they overlap as little as possible the low stability margin areas of the Nichols chart. As the uncertainties are taken into account by the least conservative method, only a a non-linear optimization method can be used.

For N -= N + = 0, only four independent open-loop parameters have to be optimized. The parameterization of the open-loop transfer function by complex fractional orders, then simplifies the optimization considerably. During optimization a complex order has the same function as a whole set of parameters found in common rational controllers. Finally, the fractional controller K F (s) is defined by its frequency response:

          j j j 0 0 F G K  . ( 9
)
The parameters of a rational (i.e. with integer orders) transfer function K R (s) with a predefined low-order structure are tuned to fit the ideal frequency response K F (j). Any frequency-domain system-identification technique can be used. An advantage of this design method is that whatever the complexity of the control problem, it can be used low values of the controller order (usually around 6).

MIMO Crone design methodologies

LTI square MIMO uncertain plants are often, for the sake of simplicity, controlled using diagonal (or decentralized) MIMO controllers. Each element of the controllers is usually designed by taking into account only SISO uncertain behaviors of the MIMO plants. When these SISO controllers are designed to achieve rapid dynamics, a decrease of the stability margins of each closed-loop can often be seen. Several Crone MIMO extensions have been defined for MIMO plants [START_REF] Lanusse | Robust control of LTI square MIMO plants using two CRONE control design approaches[END_REF][START_REF] Nelson-Gruel | Decentralized CRONE control of mxn multivariable system with time-delay[END_REF]. The multi-SISO Crone control is defined as the SISO Crone control of each diagonal element of an uncertain nxn MIMO plant. The controller transfer matrix is diagonal and the coupling elements of plants are interpreted as an additional uncertainty on the plant diagonal elements.

A fully MIMO design approach may sometimes be necessary, for instance when the plant diagonal dominance degree is weak. Then, a MIMO Crone control design using diagonal or non-diagonal controllers has been proposed. The design of multi-SISO and MIMO Crone control relies on complementary approaches: the multi-SISO design is easy to use for MIMO plants, but is still a diagonal design; the MIMO design could be more efficient, but also more difficult to use. One or the other has to be chosen, depending on the multivariable degree of the plant, to optimize the ease-ofuse/performance trade-off. The multi-SISO Crone approach enables the design of a decentralized controller K(s) (Fig. 3). The open loop transfer

Multi-SISO Crone design methodology

function matrix (s) is                                  s G s K s G s K s G s K s G s K s K s G s nn n n n n      1 1 1 11 1  . ( 10
)
The Gershgorin theorem states that the closed loop is stable if the -1 point of the complex plane is never included in circles with  ii (j) as center and r ii () as radius with:

                               i j n j i j n j ji i ij j ii G K G K r and 1 and 1 j j , j j min      (11)
These circles can be taken into account as a new uncertainty that has to increase the uncertainty frequency-domains of  ii (j). They become ellipsoids on the chart if the plant is diagonal dominant. The corresponding multiplicative uncertainty is defined by:

                                  i j n j i j n j ii ji ii i ij j G G G K G K and 1 and 1 0 0 j j 1 , j j j j 1 min       (12)
The second element related to the off-diagonal column elements remains unchanged when the controller is designed. Using the common SISO Crone approach, the design of each controller diagonal element K i (s) is achieved by taking into account:

 the diagonal nominal transfer function G ii0 (s)  the structured uncertainty computed from all possible values G ii (s)  the unstructured uncertainty computed from the offdiagonal elements G ji (s) with 1 ≤ j ≤ n and j ≠ i.

This approach enables an independent tuning of each open loop transfer function  i (s) (thus of each K i (s)).

At each frequency, the construction of the multivariable uncertainty domains consists in the determination of the hull that takes into account both the uncertainty related to a perturbed diagonal element (SISO uncertainty domain) and the additional multivariable uncertainty (Fig. 4).

Fig. 4. Construction of multivariable uncertainty domains on the Nichols chart for 4 plant parametric states

Non column-diagonal dominant plant, decentralized controller and multi-SISO design

For non column-diagonal dominant plants (sum of off diagonal elements of each transfer function column which is not small compare to the diagonal element), the multivariable uncertainty presented by the previous section is large and cannot permit the design of a high-performing robust controller. Thus, a full MIMO design approach could be needed. Nevertheless if the plant is non diagonal dominant for one column only, the multi-SISO Crone approach can enables the design of a decentralized controller. For instance, let G 21 (s) of Fig. 3 be smaller than G 11 (s) (but G 12 (s) greater than G 22 (s). By using the multi-SISO approach, K 1 (s) can be designed by taking into account G 11 (s) and G 21 (s). Then, by using the SISO approach, K 2 (s) can be designed by taking into account the equivalent plant G 22 * (s) defined by:

G ii0 (j k ) G ii1 (j k ) G ii2 (j k ) G ii3 (j k ) Y 1 (s) Y 2 (s) G 11 (s) G 12 (s) G 21 (s) G 22 (s) U 1 (s) U 2 (s) + + K 1 (s) 0 0 K 2 (s) Y 1ref (s) Y 2ref (s) _ G(s) K(s) _               s G s K s G s K s G s G s G 11 1 12 1 21 22 * 22 1   . (14)

APPLICATION

The considered engine is a PSA DW10ATED, which is a 2.0L turbocharged 4 cylinders engine with direct injection. All the air path actuators are pneumatic (wastegate, EGR and throttle). The Mean Value Engine Model (MVEM) 0D simulation model used here has been calibrated on our engine test bench. The simulation model is a non linear model based on physical equations (e.g. thermodynamic principles for volumes, Barré de St Venant equations for restrictions) and on look-up tables (e.g. volumetric efficiency, turbocharger) [START_REF] Guzzella | Introduction to Modeling and Control of Internal Combustion Engine Systems[END_REF][START_REF] Eriksson | Modeling and Control of Turbocharged SI and DI Engines[END_REF]. All the simulation results shown here have been performed with LMS/AMESim.

System identification

Firstly, the operating points for identification must be chosen. The idea is to sweep operating point domain, and so the engine speed varies from 1000 rpm to 4000 rpm and the torque from minimum to maximum allowed in our engine test bench which corresponds to 54 operating points as shown in Fig. 5. Two excitations (EGR valve and wastegate) have been done to identify systems from EGR valve or wastegate to boost pressure or to air flow. Hence, four systems will be identified.

Fig. 5. Operating points used for identification

Secondly, the signal excitation must be chosen. Here, the sampling frequency is chosen to be of 1 kHz and the exciting frequency goes from 0.2 Hz to 40 Hz according to the system dynamic. As the idea is to determine a frequency domain behavior, a multi-sine (i.e. a sum of sinusoids at different frequencies) or a chirp must be preferred to the PRBS (Pseudo Random Binary Signal). The advantage of the multisine ( 15) is that only a set of selected frequencies is included in the excitation signal:

     F k k k t f A u t u 1 0 ) 2 cos( ) (   ( 15
)
where the Schroeder phases are θ k = -k(k-1)π/F and f k is l k f 0 with l k  and F is the number of cosines. Next, on each operating points of Fig. 5, signal excitation (with EGR valve and wastegate) is performed. The average u 0 and the amplitude A are chosen with respect to the system constraints (i.e. saturation level), compromise between small signal hypothesis and noise level, and nominal value of the outputs. Some measurements like boost pressure or air flow are then acquired.

Finally, Fast Fourier Transform is performed to compute the Bode diagram matrix of the real system (Fig. 6). Four SISO transfer functions are described:

 G 11 : from EGR valve (%) to air flow (g/s)  G 21 : from EGR valve (%) to boost pressure (bar)  G 12 : from wastegate (%) to air flow (g/s)  G 22 : from wastegate (%) to boost pressure (bar)

From these Bode diagrams, it can be noticed that the variation of frequency responses is important, so that the system is highly nonlinear. These nonlinearities will be taken into account in the controller design. It can be noticed that G 11 is greater than G 21 but also that G 22 is lower than G 12 . Thus, as explained by section 2.3, K 1 (s) will be designed by using the multi-SISO approach and then, K 2 (s) will be designed by using the SISO approach on the equivalent plant

G 22 * (s).
     G G G G G

Specifications

For both controlled outputs, the first frequency-domain specifications, which are directly derived from the desired system dynamic, are a resonant peak of T complementary sensitivity function lower than 1dB (overshoot of 10% in order to ensure a sufficient stability degree) and a modulus margin greater than 0.5 (resonant peak of S sensitivity lower than 6dB). The required value of the sensitivity function bandwidth is respectively 20 rad/s and 10 rad/s (response time < 0.15s and 0.3s) for the Q air and p boost outputs. The acceptation of 3% of control noise for respectively 0.3g/s and 5mbar of measurement noise needs to limit the KS control effort sensitivity function at respectively 20dB and 55.6dB. Note that a high frequency white noise is here considered. * (s)) have no integrator, so each controller must have an integrator to ensure zero steady state error (low gain at low frequency for GS and S sensitivity functions). Thus the low frequency order n li of each nominal fractional open loop needs to be 1. To limit the control effort sensitivity at high frequency and to obtain a strictly proper controller, the high frequency order n hi needs to be 4 for  10 (s) and 5 for  20 (s). Using ( 9), a frequency domain system identification method provides the decentralized controller defined by:

Control design

SIMULATION RESULTS

A classical Anti-Reset Windup (ARW) has been included to manage the saturation of the integrator as shown in Fig. 10. The range for the wastegate (resp. EGR) valve goes from 40% to 80% (resp. from 0% to 100%). The controller is split into two parts, an integrator with one real zero and a transfer function (which is the other part of the controller): 13 and15 show the performance in terms of boost pressure. A prefilter on the set point could be added to decrease the overshoot (e.g Fig. 14 and 15). A static feedforward (learned from identification data) has been tested, but it does not increase the performance (e.g Fig. 12 and 13).

        s a s KK s K 1 ) ( ) ( (17)
Finally, the proposed control scheme is compared to a decentralized linear Internal Model Control (IMC), as shown on Fig. 14 and 15. The internal model and the controller bandwidth are chosen the same as for the Crone design. The results show that the IMC is more oscillatory and has a behavior related to the nominal model chosen. Moreover, neither coupling, nor robustness and nor specifications (e.g. noise) are taken here into account with the IMC design.

CONCLUSION

In this paper, we propose a systematic method for designing a robust control, which we apply here to the air path of a diesel engine. The computationally inexpensive control is thus obtained faster than the usual look-up table based control. Indeed, after frequency-domain system identification, a multi-SISO Crone control is obtained ensuring all frequencydomain specifications. Good control performances of the proposed method have been demonstrated in simulation and compared to another control structure (Internal Model Control). Future works will extend this paper to more complex technologies (e.g. with throttle) and applied it on our engine test bench. Future works will have the global objective to obtain the best compromise NOx/PM.

  Fig. 1. Air path of a turbocharged diesel engine with ExhaustGas Recirculation (EGR)

Fig. 3 .

 3 Fig. 3. Decentralized control of a 2x2 MIMO plant

  Fig. 6. Bode diagram of        ) j ( ) j ( ) j ( ) j ( ) j ( 22 21 12 11

  Using the multi-SISO approach, the nominal open-loop transfer function  10 (s) = G 110 (s)K 1 (s) is designed by taking into account perturbated G 11 (j) plus the additional unstructured uncertainty defined from │G 21 (j)│. G 110 (s) is defined by an arbitrary transfer function whose frequency mg/cycle) response is within the range of all the possible frequency responses. Then, using the SISO approach,  20 (s) = G 220 * (s)K 2 (s) is designed by taking into account G 22 * (s). Both SISO systems (EGR→Q air G 110 (s) and equivalent WG→p boost G 220

Figure 7 Fig. 7 .

 77 Figure 7 presents the optimized and perturbed open loop frequency responses.

  the closed-loop sensitivity functions T and KS. Upper limits on the sensitivity functions are ensured.

Fig. 9 .

 9 Fig. 8. Complementary sensitivity function T

Fig. 10 .

 10 Fig. 10. Implementation of the Anti-Reset WindupThe control structure of Fig.2is used here, and the test scenario for the fuel mass is shown in Fig.11.

Fig. 12 .Fig. 14 .

 1214 Fig. 12. Air flow (top in g/s) and EGR valve (bottom in %) at 1500rpm with and without a feedforward

  Fig. 11. Test scenario for fuel mass at 1500rpm and 2500 rpm Both controllers are validated together in simulation on various transients. Figures 12 to 15 show two examples at two different engine speeds (1500 and 2500 rpm). The dynamic performance of both controllers is quite good. Indeed, only small overshoots are obtained and there is no steady state error. Figures 12 and 14 show the performance in terms of Air Flow and Figures


Caroline Prognon

Christian Dupuis

François Barbier

Jean-Yves Storme

Florence Quesnel

Paleomagnetic dating of in situ weathering profiles of Belgium and northern France: paleogeographic implications around the Paleocene-Eocene boundary

come

Paleomagnetic dating of in situ weathering profiles of Belgium and northern France: paleogeographic implications around the Paleocene-Eocene boundary

Caroline RICORDEL-PROGNON (1) , Christian DUPUIS (2) , François BARBIER (3) , Jean-Yves STORME (3) and Florence QUESNEL (1)

(1) BRGM, GEO/G2R, BP 36009, 45060 Orléans cedex 2, France

(2) UMONS, Géol. Fond. & Appl., Rue de Houdain 9, 7000 Mons, Belgium

(3) FUNDP, UCL-Namur, Rue de Bruxelles, 61, 5000 Namur, Belgium

The geological archives record "hyperthermic" crises, along with their consequences on the biota and physical environment. Among these, the PETM (Paleocene-Eocene Thermal Maximum) is often considered as the closest analogue to the current climate crisis due to its global character and the speeds at which the CO 2 rate and average temperatures increased.

The shallow to deep marine environments from various paleolatitudes have been studied intensively (e.g. Aubry et al, 2007), but apart notable paleontological studies, the PETM impact on the terrestrial realm at a regional scale has probably not been studied and integrated enough (Zachos et al,. 2008). Moreover very few studies aimed at checking if the drastic rises of greenhouse gases and temperature had a real impact on the weathering profiles development during the PETM. Such a regional study is proposed in the "Sparnacian" terrestrial and lagoonal units of the Paris Basin, which offers rich and diversified interconnected paleoenvironments, and on its emerged interfluves and borders.

The paleoweathering profiles here considered belong to the so-called "Landenian" quartzites, or "Sparnacian" silcretes, and are locally well correlated to the first terrestrial units of the Tienen and Mortemer Fm, between the Upper Thanetian and Lower Ypresian marine units. However some silcretes and ferruginous sandstones are sometimes dated no better than Early Paleogene. To improve the error bar from 25 Ma to 5 Ma would mark a significant progress. Paleomagnetism is one of the methods useful to improve the uncertainty being often the status of those geological objects. Goethite and hematite, main iron oxides formed in weathering profiles, acquire a chemical remanent magnetization (CRM) in the direction of the ambient geomagnetic field. Consequently paleomagnetism is often considered as the most suitable method for dating weathering profiles (e.g. Idnurm & Senior, 1978; Ricordel-Prognon et al, 2010). The fossil geomagnetic direction enables one to calculate the virtual magnetic pole (VMP) of the site where magnetic minerals were precipitated. Dating the minerals is then possible by comparing their recorded paleomagnetic poles (VGP) with the apparent polar wander path (APWP) of the continent in which the site is located.

In situ weathering profile formed upon the Upper Thanetian glauconitic sands from the Grandglise section (Belgium) have been sampled in details and various analyses have been performed: granulometry, XRD and magnetic mineralogy, petrography, paleomagnetism.

Haematite is the main magnetization carrier, directions are well clustered, with a low MAD (maximum angular deviation). However the dating obtained around the Paleocene-Eocene boundary is consistent with the stratigraphic position of the Grandglise paleosol and gives evidence of a fossil weathering, instead of a recent one related to a Neogene to Quaternary re-exposure often invoked for such red and variegated sandstones. Our results and others recently obtained in the neighboring Avesnois help to decipher the correlation between the Grandglise paleosol and surroundings silcretes and to precise the terrestrial paleogeographic evolution on the emerged areas during this critical interval.


Pierre Boullier
email: pierre.boullier@inria.fr

Benoît Sagot Alpage

Parsing Directed Acyclic Graphs with Range Concatenation Grammars

Range Concatenation Grammars (RCGs) are a syntactic formalism which possesses many attractive properties. It is more powerful than Linear Context-Free Rewriting Systems, though this power is not reached to the detriment of efficiency since its sentences can always be parsed in polynomial time. If the input, instead of a string, is a Directed Acyclic Graph (DAG), only simple RCGs can still be parsed in polynomial time. For non-linear RCGs, this polynomial parsing time cannot be guaranteed anymore. In this paper, we show how the standard parsing algorithm can be adapted for parsing DAGs with RCGs, both in the linear (simple) and in the non-linear case.

Introduction

The Range Concatenation Grammar (RCG) formalism has been introduced by Boullier ten years ago.

A complete definition can be found in (Boullier, 2004), together with some of its formal properties and a parsing algorithm (qualified here of standard) which runs in polynomial time. In this paper we shall only consider the positive version of RCGs which will be abbreviated as PRCG. 1 PRCGs are very attractive since they are more powerful than the Linear Context-Free Rewriting Systems (LCFRSs) by (Vijay-Shanker et al., 1987). In fact LCFRSs are equivalent to simple PRCGs which are a subclass of PRCGs. Many Mildly Context-Sensitive (MCS) formalisms, including Tree Adjoining Grammars (TAGs) and various kinds of Multi-Component TAGs, have already been 1 Negative RCGs do not add formal power since both versions exactly cover the class PTIME of languages recognizable in deterministic polynomial time (see (Boullier, 2004) for an indirect proof and (Bertsch and Nederhof, 2001) for a direct proof). translated into their simple PRCG counterpart in order to get an efficient parser for free (see for example (Barthélemy et al., 2001)).

However, in many Natural Language Processing applications, the most suitable input for a parser is not a sequence of words (forms, terminal symbols), but a more complex representation, usually defined as a Direct Acyclic Graph (DAG), which correspond to finite regular languages, for taking into account various kinds of ambiguities. Such ambiguities may come, among others, from the output of speech recognition systems, from lexical ambiguities (and in particular from tokenization ambiguities), or from a nondeterministic spelling correction module.

Yet, it has been shown by (Bertsch and Nederhof, 2001) that parsing of regular languages (and therefore of DAGs) using simple PRCGs is polynomial. In the same paper, it is also proven that parsing of finite regular languages (the DAG case) using arbitrary RCGs is NP-complete.

This papers aims at showing how these complexity results can be made concrete in a parser, by extending a standard RCG parsing algorithm so as to handle input DAGs. We will first recall both some basic definitions and their notations. Afterwards we will see, with a slight modification of the notion of ranges, how it is possible to use the standard PRCG parsing algorithm to get in polynomial time a parse forest with a DAG as input.2 However, the resulting parse forest is valid only for simple PRCGs. In the non-linear case, and consistently with the complexity results mentioned above, we show that the resulting parse forest needs further processing for filtering out inconsistent parses, which may need an exponential time. The proposed filtering algorithm allows for parsing DAGs in practice with any PRCG, including non-linear ones.

Basic notions and notations

Positive Range Concatenation Grammars

A positive range concatenation grammar (PRCG) G = (N, T, V, P, S) is a 5-tuple in which:

• T and V are disjoint alphabets of terminal symbols and variable symbols respectively.

• N is a non-empty finite set of predicates of fixed arity (also called fan-out). We write k = arity(A) if the arity of the predicate A is k. A predicate A with its arguments is noted A( α) with a vector notation such that

| α| = k and α[j] is its j th argument. An argument is a string in (V ∪ T ) * .
• S is a distinguished predicate called the start predicate (or axiom) of arity 1.

• P is a finite set of clauses. A clause c is a rewriting rule of the form A 0 ( α 0 ) → A 1 ( α 1 ) . . . A r ( α r ) where r, r ≥ 0 is its rank, A 0 ( α 0 ) is its left-hand side or LHS, and A 1 ( α 1 ) . . . A r ( α r ) its right-hand side or RHS. By definition c[i] = A i ( α i ), 0 ≤ i ≤ r
where A i is a predicate and α i its arguments; we note c

[i][j] its j th argument; c[i][j] is of the form X 1 . . . X n ij (the X k 's are terminal or variable symbols), while c[i][j][k], 0 ≤ k ≤ n ij is a position within c[i][j].
For a given clause c, and one of its predicates c[i] a subargument is defined as a substring of an argument c

[i][j] of the predicate c[i]. It is denoted by a pair of positions (c[i][j][k], c[i][j][k ′ ]), with k ≤ k ′ .
Let w = a 1 . . . a n be an input string in T * , each occurrence of a substring a l+1 . . . a u is a pair of positions (w[l], w[u]) s.t. 0 ≤ l ≤ u ≤ n called a range and noted l..u w or l..u when w is implicit. In the range l..u , l is its lower bound while u is its upper bound. If l = u, the range l..u is an empty range, it spans an empty substring. If ρ 1 = l 1 ..u 1 , . . . and ρ m = l m ..u m are ranges, the concatenation of ρ 1 , . . . , ρ m noted ρ 1 . . . ρ m is the range ρ = l..u if and only if we have

u i = l i+1 , 1 ≤ i < m, l = l 1 and u = u m . If c = A 0 ( α 0 ) → A 1 ( α 1 ) . . . A r ( α r ) is a clause, each of its sub- arguments (c[i][j][k], c[i][j][k ′ ]
) may take a range ρ = l..u as value: we say that it is instantiated by ρ. However, the instantiation of a subargument is subjected to the following constraints.

• If the subargument is the empty string (i.e., k = k ′ ), ρ is an empty range.

• If the subargument is a terminal symbol (i.e., k + 1 = k ′ and X k ′ ∈ T ), ρ is such that l + 1 = u and a u = X k ′ . Note that several occurrences of the same terminal symbol may be instantiated by different ranges.

• If the subargument is a variable symbol (i.e., k

+ 1 = k ′ and X k ′ ∈ V ), any occurrence (c[i ′ ][j ′ ][m], c[i ′ ][j ′ ][m ′ ]) of X k ′ is instantiated by ρ.
Thus, each occurrence of the same variable symbol must be instantiated by the same range.

• If the subargument is the string X k+1 . . . X k ′ , ρ is its instantiation if and only if we have ρ = ρ k+1 . . . ρ k ′ in which ρ k+1 , . . . , ρ k ′ are respectively the instantiations of X k+1 , . . . ,

X k ′ .
If in c we replace each argument by its instantiation, we get an instantiated clause noted

A 0 ( ρ 0 ) → A 1 ( ρ 1 ) . . . A r ( ρ r ) in which each A i ( ρ i ) is an instantiated predicate.
A binary relation called derive and noted ⇒ G,w is defined on strings of instantiated predicates. If Γ 1 and Γ 2 are strings of instantiated predicates, we have

Γ 1 A 0 ( ρ 0 ) Γ 2 ⇒ G,w Γ 1 A 1 ( ρ 1 ) . . . A m ( ρ m ) Γ 2 if and only if A 0 ( ρ 0 ) → A 1 ( ρ 1 ) . . . A m ( ρ m ) is an instantiated clause. The (string) language of a PRCG G is the set L(G) = {w | S( 0..|w| w ) + ⇒ G,w
ε}. In other words, an input string w ∈ T * , |w| = n is a sentence of G if and only there exists a complete derivation which starts from S( 0..n ) (the instantiation of the start predicate on the whole input text) and leads to the empty string (of instantiated predicates). The parse forest of w is the CFG whose axiom is S( 0..n ) and whose productions are the instantiated clauses used in all complete derivations. 3 We say that the arity of a PRCG is k, and we call it a k-PRCG, if and only if k is the maximum arity of its predicates (k = max A∈N arity(A)). We say that a k-PRCG is simple, we have a simple k-PRCG, if and only if each of its clause is

• non-combinatorial: the arguments of its RHS predicates are single variables;

• non-erasing: each variable which occur in its LHS (resp. RHS) also occurs in its RHS (resp. LHS);

• linear: there are no variables which occur more than once in its LHS and in its RHS.

The subclass of simple PRCGs is of importance since it is MCS and is the one equivalent to LCFRSs.

Finite Automata

A non-deterministic finite automaton (NFA) is the 5-tuple A = (Q, Σ, δ, q 0 , F ) where Q is a non empty finite set of states, Σ is a finite set of terminal symbols, δ is the ternary transition relation δ = {(q i , t, q j )|q i , q j ∈ Q ∧ t ∈ Σ ∪ {ε}}, q 0 is a distinguished element of Q called the initial state and F is a subset of Q whose elements are called final states. The size of A, noted |A|, is its number of states (|A| = |Q|).

We define the ternary relation δ * on Q × Σ * × Q as the smallest set s.t. δ * = {(q, ε, q) | q ∈ Q} ∪ {(q 1 , xt, q 3 ) | (q 1 , x, q 2 ) ∈ δ * ∧ (q 2 , t, q 3 ) ∈ δ}. If (q, x, q ′ ) ∈ δ * , we say that x is a path between q and q ′ . If q = q 0 and q ′ ∈ F , x is a complete path.

The language L(A) defined (generated, recognized, accepted) by the NFA A is the set of all its complete paths.

We say that a NFA is empty if and only if its language is empty. Two NFAs are equivalent if and only if they define the same language. A NFA is ε-free if and only if its transition relation does not contain a transition of the form (q 1 , ε, q 2 ). Every NFA can be transformed into an equivalent ε-free NFA (this classical result and those recalled below can be found, e.g., in (Hopcroft and Ullman, 1979)).

As usual, a NFA is drawn with the following conventions: a transition (q 1 , t, q 2 ) is an arrow labelled t from state q 1 to state q 2 which are printed with a surrounded circle. Final states are doubly circled while the initial state has a single unconnected, unlabelled input arrow.

A deterministic finite automaton (DFA) is a NFA in which the transition relation δ is a transition function, δ : Q × Σ → Q. In other words, there are no ε-transitions and if (q 1 , t, q 2 ) ∈ δ, t = ε and ∄(q 1 , t, q ′ 2 ) ∈ δ with q ′ 2 = q 2 . Each NFA can be transformed by the subset construction into an equivalent DFA. Moreover, each DFA can be transformed by a minimization algorithm into an equivalent DFA which is minimal (i.e., there is no other equivalent DFA with fewer states).

Directed acyclic graphs

Formally, a directed acyclic graph (DAG) D = (Q, Σ, δ, q 0 , F ) is an NFA for which there exists a strict order relation < on Q such that (p, t, q) ∈ δ ⇒ p < q. Without loss of generality we may assume that < is a total order.

Of course, as NFAs, DAGs can be transformed into equivalent deterministic or minimal DAGs.

DAGs and PRCGs

A DAG D is recognized (accepted) by a PRCG G if and only if L(D) ∩ L(G) = ∅.
A trivial way to solve this recognition (or parsing) problem is to extract the complete paths of L(D) (which are in finite number) one by one and to parse each such string with a standard PRCG parser, the (complete) parse forest for D being the union of each individual forest. 4 However since DAGs may define an exponential number of strings w.r.t. its own size,5 the previous operation would take an exponential time in the size of D, and the parse forest would also have an exponential size.

The purpose of this paper is to show that it is possible to directly parse a DAG (without any unfolding) by sharing identical computations. This sharing may lead to a polynomial parse time for an exponential number of sentences, but, in some cases, the parse time remains exponential.

DAGs and Ranges

In many NLP applications the source text cannot be considered as a sequence of terminal symbols, but rather as a finite set of finite strings. As mentioned in th introduction, this non-unique string could be used to encode not-yet-solved ambiguities in the input. DAGs are a convenient way to represent these finite sets of strings by factorizing their common parts (thanks to the minimization algorithm).

In order to use DAGs as inputs for PRCG parsing we will perform two generalizations.

The first one follows. Let w = t 1 . . . t n be a string in some alphabet Σ and let Q = {q i | 0 ≤ i ≤ n} be a set of n + 1 bounds with a total order relation <, we have q 0 < q 1 < . . . < q n . The sequence π = q 0 t 1 q 1 t 2 q 2 . . . t n q n ∈ Q×(Σ×Q) n is called a bounded string which spells w. A range is a pair of bounds (q i , q j ) with q i < q j noted p i ..p j π and any triple of the form (q i-1 t i q i ) is called a transition. All the notions around PRCGs defined in Section 2.1 easily generalize from strings to bounded strings. It is also the case for the standard parsing algorithm of (Boullier, 2004). Now the next step is to move from bounded strings to DAGs. Let D = (Q, Σ, δ, q 0 , F ) be a DAG. A string x ∈ Σ * s.t. we have (q 1 , x, q 2 ) ∈ δ * is called a path between q 1 and q 2 and a string

π = qt 1 q 1 . . . t p q p ∈ Q × (Σ ∪ {ε} × Q) * is a
bounded path and we say that π spells t 1 t 2 . . . t p . A path x from q 0 to f ∈ F is a complete path and a bounded path of the form q 0 t 1 . . . t n f with f ∈ F is a complete bounded path. In the context of a DAG D, a range is a pair of states (q i , q j ) with q i < q j noted q i ..q j D . A range q i ..q j D is valid if and only if there exists a path from q i to q j in D. Of course, any range p..q D defines its associated sub-DAG D p..q = (Q p..q , Σ p..q , δ p..q , p, {q}) as follows. Its transition relation is

δ p..q = {(r, t, s) | (r, t, s) ∈ δ ∧ (p, x ′ , r), (s, x ′′ , q) ∈ δ * }. If δ p..q = ∅ (i.e.
, there is no path between p and q), D p..q is the empty DAG, otherwise Q p..q (resp. Σ p..q ) are the states (resp. terminal symbols) of the transitions of δ p..q . With this new definition of ranges, the notions of instantiation and derivation easily generalize from bounded strings to DAGs.

The language of a PRCG G for a DAG D is defined by

• L (G, D) = f ∈F {x | S( q 0 ..f D ) + ⇒ G,D ε}. Let x ∈ L(D), it is not very difficult to show that if x ∈ L(G) then we have x ∈ • L (G, D).
However, the converse is not true

(see Example 1), a sentence of L(D)∩ • L (G, D)
may not be in L(G). To put it differently, if we use the standard RCG parser, with the ranges of a DAG, we produce the shared parse-forest for the language

• L (G, D) which is a superset of L(D) ∩ L(G).
However, if G is a simple PRCG, we have

the equality L(G) = D is a DAG • L (G, D).
Note that the subclass of simple PRCGs is of importance since it is MCS and it is the one equivalent to LCFRSs. The informal reason of the equality is the following. If an instantiated predicate A i ( ρ i ) succeeds in some RHS, this means that each of its ranges ρ i [j] = k..l D has been recognized as being a component of A i , more precisely their exists a path from k to l in D which is a component of A i . The range k..l D selects in D a set δ k..l D of transitions (the transitions used in the bounded paths from k to l). Because of the linearity of G, there is no other range in that RHS which selects a transition in δ k..l D . Thus the bounded paths selected by all the ranges of that RHS are disjoints. In other words, any occurrence of a valid instantiated range i..j D selects a set of paths which is a subset of L(D i..j ). Now, if we consider a non-linear PRCG, in some of its clauses, there is a variable, say X, which has several occurrences in its RHS (if we consider a top-down non-linearity). Now assume that for some input DAG D, an instantiation of that clause is a component of some complete derivation. Let p..q D be the instantiation of X in that instantiated clause. The fact that a predicate in which X occurs succeeds means that there exist paths from p to q in D p..q . The same thing stands for all the other occurrences of X but nothing force these paths to be identical or not.

a n b n c n (X) → a * b n c n (X) a n b n c * (X) a * b n c n (aX) → a * b n c n (X) a * b n c n (X) → b n c n (X) b n c n (bXc) → b n c n (X) b n c n (ε) → ε a n b n c * (Xc) → a n b n c * (X) a n b n c * (X) → a n b n (X) a n b n (aXb) → a n b n (X) a n b n (ε) → ε
If we use this PRCG to parse the DAG of Figure 1 which defines the language {ab, bc}, we (erroneously) get the non-empty parse forest of Figure 2 though neither ab nor bc is in a n b n c n . 6 It is not difficult to see that the problem comes from the non-linear instantiated variable X 1..4 in the start node, and more precisely from the actual (wrong) meaning of the three different occurrences of X 1..4 in a n b n c n (X 1..4 ) → a * b n c n (X 1..4 ) a n b n c * (X 1..4 ). The first occurrence in its RHS says that there exists a path in the input DAG from state 1 to state 4 which is an a * b n c n . The second occurrence says that there exists a path from state 1 to state 4 which is an a n b n c * . While the LHS occurrence (wrongly) says that there exists a path from state 1 to state 4 which is an a n b n c n . However, if the two X 1..4 's in the RHS had selected common paths (this is not possible here) between 1 and 4, a valid interpretation could have been proposed.

With this example, we see that the difficulty of DAG parsing only arises with non-linear PRCGs.

If we consider linear PRCGs, the sub-class of the PRCGs which is equivalent to LCFRSs, the 6 In this forest oval nodes denote different instantiated predicates, while its associated instantiated clauses are presented as its daughter(s) and are denoted by square nodes. The LHS of each instantiated clause shows the instantiation of its LHS symbols. The RHS is the corresponding sequence of instantiated predicates. The number of daughters of each square node is the number of its RHS instantiated predicates.

standard algorithm works perfectly well with input DAGs, since a valid instantiation of an argument of a predicate in a clause by some range p..q means that there exists (at least) one path between p and q which is recognized.

The paper will now concentrate on non-linear PRCGs, and will present a new valid parsing algorithm and study its complexities (in space and time).

In order to simplify the presentation we introduce this algorithm as a post-processing pass which will work on the shared parse-forest output by the (slightly modified) standard algorithm which accepts DAGs as input.

Parsing DAGs with non-linear PRCGs

The standard parsing algorithm of (Boullier, 2004) working on a string w can be sketched as follows.

It uses a single memoized boolean function predicate(A, ρ) where A is a predicate and ρ is a vector of ranges whose dimension is arity(A). The initial call to that function has the form predicate (S, 0..|w| ). Its purpose is, for each A 0 -clause, to instantiate each of its symbols in a consistant way. For example if we assume that the i th argument of the LHS of the current A 0 -clause is α ′ i XaY α ′′ i and that the i th component of ρ 0 is the range p i ..q i an instantiation of X, a an Y by the ranges p X ..q X , p a ..q a and p Y ..q Y is such that we have p i ≤ p X ≤ q X = p a < q a = p a + 1 = p Y ≤ q Y ≤ q i and w = w ′ aw ′′ with |w ′ | = p a . Since the PRCG is non bottom-up erasing, the instantiation of all the LHS symbols implies that all the arguments of the RHS predicates A i are also instantiated and gathered into the vector of ranges ρ i . Now, for each i (1 ≤ i ≤ |RHS|), we can call predicate (A i , ρ i ). If all these calls succeed, the instantiated clause can be stored as a component of the shared parse forest. 7 In the case of a DAG D = (Q, Σ, δ, q 0 , F ) as input, there are two slight modifications, the initial call is changed by the conjunctive call predicate(S, q 0 ..f 1 ) ∨ . . . ∨ predicate (S, q 0 ..f |F | ) with f i ∈ F8 and the terminal symbol a can be instantiated by the range p a ..q a D only if (p a , a, q a ) is a transition in δ. The variable symbol X can be instantiated by the range p X ..q X D only if p X ..q X D is valid.

a n b n c n 1..4 a n b n c n (X 1..4 ) → a * b n c n 1..4 a n b n c * 1..4 a * b n c n 1..4 a * b n c n (X 1..4 ) → b n c n 1..4 a n b n c * 1..4 a n b n c * (X 1..4 ) → a n b n 1..4 b n c n 1..4 b n c n (b 1..3 X 3..3 c 3..4 ) → b n c n 3..3 a n b n 1..4 a n b n (a 1..2 X 2..2 b 2..4 ) → a n b n 2..2 b n c n 3..3 b n c n (ε 3..3 ) → ε a n b n 2..2 a n b n (ε 2..2 ) → ε

Forest Filtering

We assume here that for a given PRCG G we have built the parse forest of an input DAG D as explained above and that each instantiated clause of that forest contains the range p X ..q X D of each of its instantiated symbols X. We have seen in Example 1 that this parse forest is valid if G is linear but may well be unvalid if G is non-linear.

In that latter case, this happens because the range p X ..q X D of each instantiation of the non-linear variable X selects the whole sub-DAG D p X ..q X while each instantiation should only select a sublanguage of L(D p X ..q X ). For each occurrence of X in the LHS or RHS of a non-linear clause, its sub-languages could of course be different from the others. In fact, we are interested in their intersections: If their intersections are non empty, this is the language which will be associated with p X ..q X D , otherwise, if their intersections are empty, then the instantiation of the considered clause fails and must thus be removed from the forest. Of course, we will consider that the language (a finite number of strings) associated with each occurrence of each instantiated symbol is represented by a DAG.

The idea of the forest filtering algorithm is to first compute the DAGs associated with each argument of each instantiated predicate during a bottom-up walk. These DAGs are called decorations. This processing will perform DAG compositions (including intersections, as suggested above), and will erase clauses in which empty intersections occur. If the DAG associated with the single argument of the super-root is empty, then parsing failed.

Otherwise, a top-down walk is launched (see below), which may also erase non-valid instantiated clauses. If necessary, the algorithm is completed by a classical CFG algorithm which erase non productive and unreachable symbols leaving a reduced grammar/forest.

In order to simplify our presentation we will assume that the PRCGs are non-combinatorial and bottom-up non-erasing.

However, we can note that the following algorithm can be generalized in order to handle combinatorial PRCGs and in particular with overlapping arguments. 9 Moreover, we will assume that the forest is non cyclic (or equivalently that all cycles have previously been removed). 10 9 For example the non-linear combinatorial clause A(XY Z) → B(XY ) B(Y Z) has overlapping arguments.

10 By a classical algorithm from the CFG technology.

The Bottom-Up Walk

For this principle algorithm, we assume that for each instantiated clause in the forest, a DAG will be associated with each occurrence of each instantiated symbol. More precisely, for a given instantiated A 0 -clause, the DAGs associated with the RHS symbol occurrences are composed (see below) to build up DAGs which will be associated with each argument of its LHS predicate. For each LHS argument, this composition is directed by the sequence of symbols in the argument itself.

The forest is walked bottom-up starting from its leaves. The constraint being that an instantiated clause is visited if and only if all its RHS instantiated predicates have already all been visited (computed).

This constraint can be satisfied for any non-cyclic forest.

To be more precise, consider an instantiation

c ρ = A 0 ( ρ 0 ) → A 1 ( ρ 1 ) . . . A p ( ρ p ) of the clause c = A 0 ( α 0 ) → A 1 ( α 1 ) . . . A m ( α m )
, we perform the following sequence:

1. If the clause is not top-down linear (i.e., there exist multiple occurrences of the same variables in its RHS arguments), for such variable X let the range p X ..q X be its instantiation (by definition, all occurrences are instantiated by the same range), we perform the intersection of the DAGs associated with each instantiated predicate argument X. If one intersection results in an empty DAG, the instantiated clause is removed from the forest. Otherwise, we perform the following steps.

2. If a RHS variable Y is linear, it occurs once in the j th argument of predicate A i . We perform a brand new copy of the DAG associated with the j th argument of the instantiation of A i .

3. At that moment, all instantiated variables which occur in c ρ are associated with a DAG.

For each occurrence of a terminal symbol t in the LHS arguments we associate a (new) DAG whose only transition is (p, t, q) where p and q are brand new states with, of course, p < q.

4. Here, all symbols (terminals or variables) are associated with disjoints DAGs. For each LHS argument α 0 [i] = X i 1 . . . X i j . . . X i p i , we associate a new DAG which is the concatenation of the DAGs associated with the symbols X i 1 , . . . , X i j , . . . and X i p i .

5.

Here each LHS argument of c ρ is associated with a non empty DAG, we then report the individual contribution of c ρ into the (already computed) DAGs associated with the arguments of its LHS A 0 ( ρ 0 ). The DAG associated with the i th argument of A 0 ( ρ 0 ) is the union (or a copy if it is the first time) of its previous DAG value with the DAG associated with the i th argument of the LHS of c ρ .

This bottom-up walk ends on the super-root with a final decoration say R. In fact, during this bottomup walk, we have computed the intersection of the languages defined by the input DAG and by the PRCG (i.e., we have

L(R) = L(D) ∩ L(G)).
Example 2. With the PRCG of Example 1 and the input DAG of Figure 3, we get the parse forest of Figure 4 whose transitions are decorated by the DAGs computed by the bottom-up algorithm. 11 The crucial point to note here is the intersection which is performed between {abc, bc} and {abc, ab} on

a n b n c n (X 1..4 ) → a * b n c n 1..4 a n b n c * 1..4
. The non-empty set {abc} is the final result assigned to the instantiated start symbol. Since this result is non empty, it shows that the input DAG D is recognized by G. More precisely, this shows that the sub-language of D which is recognized by G is {abc}.

However, as shown in the previous example, the (undecorated) parse forest is not the forest built for the DAG L(D) ∩ L(G) since it may contain non-valid parts (e.g., the transitions labelled {bc} or {ab} in our example). In order to get the 11 For readability reasons these DAGs are represented by their languages (i.e., set of strings). Bottom-up transitions from instantiated clauses to instantiated predicates reflects the computations performed by that instantiated clause while bottom-up transitions from instantiated predicates to instantiated clauses are the union of the DAGs entering that instantiated predicate. right forest (i.e., to get a PRCG parser -not a recognizer -which accepts a DAG as input) we need to perform another walk on the previous decorated forest.

a n b n c n 1..4 a n b n c n (X 1..4 ) → a * b n c n 1..4 a n b n c * 1..4 a * b n c n 1..4 a * b n c n (X 1..4 ) → b n c n 1..4 a * b n c n (a 1..2 X 2..4 ) → a * b n c n 2..4 a n b n c * 1..4 a n b n c * (X 1..4 ) → a n b n 1..4 a n b n c * (X 1..3 c 3..4 ) → a n b n c * 1..3 b n c n 1..4 b n c n (b 2..3 X 3..3 c 3..4 ) → b n c n 3..3 a * b n c n 2..4 a * b n c n (X 2..4 ) → b n c n 2..4 a n b n 1..4 a n b n (a 1..2 X 2..2 b 2..4 ) → a n b n 2..2 a n b n c * 1..3 a n b n c * (X 1..3 ) → a n b n 1..3 b n c n 3..3 b n c n (ε 3..3 ) → ε b n c n 2..4 b n c n (b 2..3 X 3..3 c 3..4 ) → b n c n 3..3 a n b n 2..2 a n b n (ε 2..2 ) → ε a n b n 1..3 a n b n (a 1..2 X 2..2 b 2..3 ) → a n b n 2..2

The Top-Down Walk

The idea of the top-down walk on the parse forest decorated by the bottom-up walk is to (re)compute all the previous decorations starting from the bottom-up decoration associated with the instantiated start predicate. It is to be noted that (the language defined by) each top-down decoration is a subset of its bottom-up counterpart. However, when a top-down decoration becomes empty, the corresponding subtree must be erased from the forest. If the bottom-up walk succeeds, we are sure that the top-down walk will not result in an empty forest. Moreover, if we perform a new bottom-up walk on this reduced forest, the new bottom-up decorations will denote the same language as their top-down decorations counterpart.

The forest is walked top-down starting from the super-root. The constraint being that an instantiated A( ρ)-clause is visited if and only if all the occurrences of A( ρ) occurring in the RHS of instantiated clauses have all already been visited. This constraint can be satisfied for any non-cyclic forest.

Initially, we assume that each argument of each instantiated predicate has an empty decoration, except for the argument of the super-root which is decorated by the DAG R computed by the bottomup pass. Now, assume that a top-down decoration has been (fully) computed for each argument of the instantiated predicate A 0 ( ρ 0 ).

For each instantiated clause of the form which are changed both to {abc} instead of {abc, bc} and {abc, ab}. These two changes induce the indicated erasings.

c ρ = A 0 ( ρ 0 ) → A 1 ( ρ 1 ) . . . A i ( ρ i ) . . . A m ( ρ m ),
13 Assume that ρ0[k] = p..q D , that the decoration DAG associated with the k th argument of A0( ρ0) is D ′ p..q = (Q ′ p..q , Σ p..q , δ ′ p..q , p ′ , F ′ p..q ) (we have L(D ′ p..q ) ⊆ L(D p..q )) and that α0[k] = α 1 k Xα 2 k and that i..j D is the instantiation of the symbol X in cρ. Our goal is to extract from D ′ p..q the decoration DAG D ′ i..j associated with that instantiated occurrence of X. This computation can be helped if we maintain, associated with each decoration DAG a function, say d, which maps each state of the decoration DAG to a set of states (bounds) of the input DAG D. If, as we have assumed, D is minimal, each set of states is a singleton, we can write d(p ′ ) = p, d(f ′ ) = q for all f ′ ∈ F ′ p..q and more generally

d(i ′ ) ∈ Q if i ′ ∈ Q ′ . Let I ′ = {i ′ | i ′ ∈ Q ′ p..q ∧ d(i ′ ) = i} and J ′ = {j ′ | j ′ ∈ Q ′ p..q ∧ d(j ′ ) = j}. The decoration DAG D ′ i..j is such that L(D ′ i..j ) = i ′ ∈I ′ ,j ′ ∈J ′ {x | x is a path from i ′ to j ′ }.
Of course, together with the construction of D ′ i..j , its associated function d must also be built.

a n b n c n 1..4 a n b n c n (X 1..4 ) → a * b n c n 1..4 a n b n c * 1..4 a * b n c n 1..4 a * b n c n (X 1..4 ) → b n c n 1..4 a * b n c n (a 1..2 X 2..4 ) → a * b n c n 2..4 a n b n c * 1..4 a n b n c * (X 1..4 ) → a n b n 1..4 a n b n c * (X 1..3 c 3..4 ) → a n b n c * 1..3 b n c n 1..4 b n c n (b 2..3 X 3..3 c 3..4 ) → b n c n 3..3 a * b n c n 2..4 a * b n c n (X 2..4 ) → b n c n 2..4 a n b n 1..4 a n b n (a 1..2 X 2..2 b 2..4 ) → a n b n 2..2 a n b n c * 1..3 a n b n c * (X 1..3 ) → a n b n 1..3 b n c n 3..3 b n c n (ε 3..3 ) → ε b n c n 2..4 b n c n (b 2..3 X 3..3 c 3..4 ) → b n c n 3..3 a n b n 2..2 a n b n (ε 2..2 ) → ε a n b n 1..3 a n b n (a 1..2 X 2..2 b 2..3 ) → a n b n 2

Time and Space Complexities

In this Section we study the time and size complexities of the forest filtering algorithm.

Let us consider the sub-DAG D p..q of the minimal input DAG D and consider any (finite) regular language L ⊆ L(D p..q ), and let D L be the minimal DAG s.t. L(D L ) = L. We show, on an example, that |D L | may be an exponential w.r.t. |D p..q |.

Consider, for a given h > 0, the language (a|b) h . We know that this language can be represented by the minimal DAG with h + 1 states of Figure 6.

Assume that h = 2k and consider the sub-language L 2k of (a|b) 2k (nested wellparenthesized strings) which is defined by

1. L 2 = {aa, bb} ; 2. k > 1, L 2k = {axa, bxb | x ∈ L 2k-2 },
It is not difficult to see that the DAG in Figure 7 defines L 2k and is minimal, but its size 2 k+2 -2 is an exponential in the size 2k + 1 of the minimal DAG for the language (a|b) 2k .

This results shows that, there exist cases in which some minimal DAGs D ′ that define sublanguages of minimal DAGs D may have a exponential size (i.e., |D ′ | = O(2 |D| ). In other words, when, during the bottom-up or top-down walk, we compute union of DAGs, we may fall on these pathologic DAGs that will induce a combinatorial explosion in both time and space.

Implementation Issues

Of course, many improvements may be brought to the previous principle algorithms in practical implementations. Let us cite two of them. First it is possible to restrict the number of DAG copies: a DAG copy is not useful if it is the last reference to that DAG.

We shall here develop the second point on a little more: if an argument of a predicate is never used in an clause involving non-linearity, it is only a waste of time to compute its decoration. We say that A k , the k th argument of the predicate A is a non-linear predicate argument if there exists a clause c in which A occurs in the RHS and whose k th argument has at least one common variable another argument B h of some predicate B of the RHS (if B = A, then of course k and h must be different). It is clear that B h is then non-linear as well. It is not difficult to see that decorations needs only to be computed if they are associated with a non-linear predicate argument. It is possible to compute those non-linear predicate arguments statically (when building the parser) when the PRCG is defined within a single module. However, if the PRCG is given in several modules, this full static computation is no longer possible. The non-linear predicate arguments must thus be identified at parse time, when the whole grammar is available. This rather trivial algorithm will not be described here, but it should be noted that it is worth doing since in practice it prevents decoration computations which can take an exponential time.

Conclusion

In this paper we have shown how PRCGs can handle DAGs as an input. If we consider the linear PRCG, the one equivalent to LCFRS, the parsing time remains polynomial. Moreover, input DAGs necessitate only rather cosmetic modifications in the standard parser.

In the non-linear case, the standard parser may produce illegal parses in its output shared parse forest. It may even produce a (non-empty) shared parse forest though no sentences of the input DAG are in the language defined by our non-linear PRCG. We have proposed a method which uses the (slightly modified) standard parser but prunes, within extra passes, its output forest and leaves all and only valid parses. During these extra bottomup and top-down walks, this pruning involves the computation of finite languages by means of concatenation, union and intersection operations. The sentences of these finite languages are always substrings of the words of the input DAG D. We choose to represent these intermediate finite languages by DAGs instead of sets of strings because the size of a DAG is, at worst, of the same order as the size of a set of strings but it could, in some cases, be exponentially smaller.

However, the time taken by this extra pruning pass cannot be guaranteed to be polynomial, as expected from previously known complexity results (Bertsch and Nederhof, 2001). We have shown an example in which pruning takes an exponential time and space in the size of D. The deep reason comes from the fact that if L is a finite (regular) language defined by some minimal DAG D, there are cases where a sub-language of L may require to be defined by a DAG whose size is an exponential in the size of D. Of course this combinatorial explosion is not a fatality, and we may wonder whether, in the particular case of NLP it will practically occur?

Figure 1 :

 1 Figure 1: Input DAG associated with ab|bc.

Figure 2 :

 2 Figure 2: Parse forest for the input DAG ab|bc.

Figure 3 :

 3 Figure 3: Input DAG associated with abc|ab|bc.

Figure 4 :

 4 Figure 4: Bottom-up decorated parse forest for the input DAG abc|ab|bc.

  b n c n (X 1..4 ) → a * b n c n 1..4 a n b n c *

Figure 5 :

 5 Figure 5: Top-down decorated parse forest for the input DAG abc|ab|bc.

Figure 6 :Figure 7 :

 67 Figure6: Input DAG associated with the language (a|b) h , h > 0.

The notion of parse forest is reminiscent of the work of[START_REF] Lang | Recognition can be harder than parsing[END_REF].

Note that this parse forest has no terminal symbols (its language is the empty string).

These forests do not share any production (instantiated clause) since ranges in a particular forest are all related to the corresponding source string w (i.e., are all of the form i..j w ). To be more precise the union operation on individual forests must be completed in adding productions which connect the new (super) axiom (say S ′ ) with each root and which are, for each w of the form S ′ → S( 0..|w| w ).

For example the language (a|b) n , n > 0 which contains 2 n strings can be defined by a minimal DAG whose size is n + 1.

Note that such an instantiated clause could be unreachable from the (future) instantiated start symbol which will be the axiom of the shared forest considered as a CFG.

Technically, each of these calls produces a forest. These individual forests may share subparts but their roots are all different. In order to have a true forest, we introduce a new root, the super-root whose daughters are the individual forests.

The decoration of each argument of Ai( ρi) is either initially empty or has already been partially computed.