Detail publikace

Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing

HOLÍK, L. VOJNAR, T. CHEN, Y. MAYR, R. HONG, C. ABDULLA, P. CLEMENTE, L.

Originální název

Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing

Anglický název

Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing

Jazyk

en

Originální abstrakt

There are two main classes of methods for checking universality and language inclusion of Büchi-automata: Rank-based methods and Ramsey-based methods. While rank-based methods have a better worst-case complexity, Ramsey-based methods have been shown to be quite competitive in practice. Previously, it was also shown (for universality checking) that a simple subsumption technique, which avoids exploration of certain cases, greatly improves the performance of the Ramsey-based method. Here, we present a much more general subsumption technique for the Ramsey-based method, which is based on using simulation preorder on the states of the Büchi-automata. This technique applies to both universality and inclusion checking, yielding a  substantial performance gain over the previously known simple subsumption approach.

Anglický abstrakt

There are two main classes of methods for checking universality and language inclusion of Büchi-automata: Rank-based methods and Ramsey-based methods. While rank-based methods have a better worst-case complexity, Ramsey-based methods have been shown to be quite competitive in practice. Previously, it was also shown (for universality checking) that a simple subsumption technique, which avoids exploration of certain cases, greatly improves the performance of the Ramsey-based method. Here, we present a much more general subsumption technique for the Ramsey-based method, which is based on using simulation preorder on the states of the Büchi-automata. This technique applies to both universality and inclusion checking, yielding a  substantial performance gain over the previously known simple subsumption approach.

Dokumenty

BibTex


@inproceedings{BUT34732,
  author="Lukáš {Holík} and Tomáš {Vojnar} and Yu-Fang {Chen} and Richard {Mayr} and Chih-Duo {Hong} and Parosh {Abdulla} and Lorenzo {Clemente}",
  title="Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing",
  annote="There are two main classes of methods for checking universality
and language inclusion of Büchi-automata: Rank-based methods
and Ramsey-based methods. While rank-based methods have a better
worst-case complexity, Ramsey-based methods have been shown to be
quite competitive in practice. Previously, it was also shown (for universality
checking) that a simple subsumption technique, which avoids exploration of
certain cases, greatly improves the performance of the Ramsey-based method. Here,
we present a much more general subsumption technique for the Ramsey-based method,
which is based on using simulation preorder on the states of the Büchi-automata.
This technique applies to both universality and inclusion checking, yielding a 
substantial performance gain over the previously known simple subsumption
approach.",
  address="Springer Verlag",
  booktitle="Computer Aided Verification",
  chapter="34732",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2010",
  month="july",
  pages="132--147",
  publisher="Springer Verlag",
  type="conference paper"
}