Publication result detail

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.

Original Title

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

English Title

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

Type

Paper in proceedings outside WoS and Scopus

Original Abstract

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.

English abstract

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.

Keywords

Büchi automata, universality, language inclusion, Ramsey-based methods, simulation subsumption

Key words in English

Büchi automata, universality, language inclusion, Ramsey-based methods, simulation subsumption

Authors

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

RIV year

2012

Released

28.07.2010

Publisher

Springer Verlag

Location

Berlín

ISBN

978-3-642-14294-9

Book

Computer Aided Verification

Edition

Lecture Notes in Computer Science

Volume

6174

Pages from

132

Pages to

147

Pages count

16

URL

http://www.springerlink.com/content/n81060p2685rl46v/

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",
  booktitle="Computer Aided Verification",
  year="2010",
  series="Lecture Notes in Computer Science",
  volume="6174",
  pages="132--147",
  publisher="Springer Verlag",
  address="Berlín",
  isbn="978-3-642-14294-9",
  url="http://www.springerlink.com/content/n81060p2685rl46v/"
}