PV1 QuIPcomparator of two weighted automata

BCV-based solver for DS-inclusion.

Application domain/field

Type of tool

Property checker (DS-inclusion)

Expected input

Expected output

Whether PdQ

Internals

BCV is an algorithm for solving DS-inclusion. The name BCV is derived from the name of the authors. DS-inclusion is about determining the quantitative inclusion for nondeterministic discounted-sum (DS) automata. Uses RABIT to check language inclusion and Reduce for minimizing Büchi automata.
Automaton

Links

Possibly the following repository from the first author's github: https://github.com/suguman/QIP/ (not linked in the paper or on the first author's website)

Last commit date

26 September 2018

Related papers

https://doi.org/10.1007/978-3-319-96142-2_9

Last publication date

18 July 2018

Related tools

DetLP

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.