. . "DE - Spolkov\u00E1 republika N\u011Bmecko" . "0302-9743" . . . "2011" . . . "Advanced Ramsey-based B\u00FCchi Automata Inclusion Testing"@en . "Abdulla, Parosh" . "6901" . "Advanced Ramsey-based B\u00FCchi Automata Inclusion Testing"@en . "Hol\u00EDk, Luk\u00E1\u0161" . "2"^^ . . "Mayr, Richard" . "Advanced Ramsey-based B\u00FCchi Automata Inclusion Testing" . "Advanced Ramsey-based B\u00FCchi Automata Inclusion Testing" . "Clemente, Lorenzo" . "RIV/00216305:26230/11:PU96126" . . "Checking language inclusion between two nondeterministic B\u00FCchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from" . "Lecture Notes in Computer Science (IF 0,513)" . . "P(GAP103/10/0306), P(GD102/09/H042), P(OC10009), S, Z(MSM0021630528)" . . "184741" . . . . "16"^^ . . "[06A777AF9607]" . . "Hong, Chih-Duo" . . . . "B\u00FCchi automata, inclusion checking, Ramsey theorem, simulation relations"@en . "Vojnar, Tom\u00E1\u0161" . . "RIV/00216305:26230/11:PU96126!RIV12-MSM-26230___" . . . "7"^^ . "26230" . "Chen, Yu-Fang" . . "Checking language inclusion between two nondeterministic B\u00FCchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from"@en . .