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 P⊆dQ

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

Related papers

Automata vs Linear-Programming Discounted-Sum Inclusion

Last publication date

18 July 2018

Related tools

DetLP

ProVerB specific


ProVerB is a part of SLEBoK. Last updated: February 2023.