# Variations on Parallel Explicit Emptiness Checks
for Generalized Buchi Automata

This paper is an extension of our previous TACAS
paper. Detailled results about this paper can be found
[here].
Since this page only meant to present new experiments, the
interested reader will refer this previous page to understand the whole setup for
the comparison with other tools such as DiVine (owcty) or
LTSmin (cndfs).

## Description

This benchmark provides a set of 3268 random formulas over 10 models extracted from the BEEM benchmark
(http://anna.fi.muni.cz/models/). We
compute formula such that for each models the NDFS of Gaiser and
Schwoon takes 2 hours of
computation for verified formula and 2 hours for violated
formulas. All formulas where selected such that they take between
10 seconds and 30 minutes (for violated formula there exist a
transition ordering that satisfies this constraint).

- adding.4.dve
- bridge.3.dve
- brp.4.dve
- collision.4.dve
- cyclic_scheduler.3.dve
- elevator2.3.dve
- elevator.4.dve
- exit.3.dve
- leader-election.3.dve
- production-cell.3.dve

### Replay

Warning! We plan to integrate all
these algorithms into the latest version of Spot. Before
downloading and using this fork, checkout if there is a more
recent version of Spot that integrates all these algorithms.

The fork of Spot used to develop these parallel emptiness checks [here].

The CSV can can be found [here].

The full logs can be found [here].