Ranker: A Tool for Complementing Büchi Automata

Ranker: A Tool for Complementing Büchi Automata

Software

Ranker is a tool for complementing Büchi automata, necessary, e.g., in automata-based model checking of reactive systems. It uses rank-based complementation as its basic procedure, but enriches it with many optimizations and heuristics. Moreover, for automata of specific types (e.g., inherently weak automata, semi-deterministic automata), it contains specialized constructions with novel optimizations.

Ranker is a tool for complementing Büchi automata, necessary, e.g., in automata-based model checking of reactive systems. It uses rank-based complementation as its basic procedure, but enriches it with many optimizations and heuristics. Moreover, for automata of specific types (e.g., inherently weak automata, semi-deterministic automata), it contains specialized constructions with novel optimizations.

Buchi automata
complementation
rank-based complementation
language inclusion
model checking

Buchi automata
complementation
rank-based complementation
language inclusion
model checking

https://github.com/vhavlena/ranker

Use of the result by another entity is possible without acquiring a license (the result is not licensed)

https://github.com/vhavlena/ranker