Detail publikace

Advanced Ramsey-based Büchi Automata Inclusion Testing

Originální název

Advanced Ramsey-based Büchi Automata Inclusion Testing

Anglický název

Advanced Ramsey-based Büchi Automata Inclusion Testing

Jazyk

en

Originální abstrakt

Checking language inclusion between two nondeterministic Büchi 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 real-world model checking benchmarks, and on the Tabakov-Vardi random model, thus showing the usefulness of the proposed techniques.

Anglický abstrakt

Checking language inclusion between two nondeterministic Büchi 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 real-world model checking benchmarks, and on the Tabakov-Vardi random model, thus showing the usefulness of the proposed techniques.

BibTex


@article{BUT76413,
  author="Parosh {Abdulla} and Yu-Fang {Chen} and Lorenzo {Clemente} and Lukáš {Holík} and Chih-Duo {Hong} and Richard {Mayr} and Tomáš {Vojnar}",
  title="Advanced Ramsey-based Büchi Automata Inclusion Testing",
  annote="Checking language inclusion between two nondeterministic Büchi 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 real-world
model checking benchmarks, and on the Tabakov-Vardi random model, thus showing
the usefulness of the proposed techniques.",
  address="NEUVEDEN",
  chapter="76413",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="6901",
  volume="2011",
  year="2011",
  month="july",
  pages="187--202",
  publisher="NEUVEDEN",
  type="journal article - other"
}