Automatic generation of optimal reductions of distributions

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F19%3A00502163" target="_blank" >RIV/67985840:_____/19:00502163 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1109/TAC.2018.2828105" target="_blank" >http://dx.doi.org/10.1109/TAC.2018.2828105</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/TAC.2018.2828105" target="_blank" >10.1109/TAC.2018.2828105</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Automatic generation of optimal reductions of distributions

Popis výsledku v původním jazyce

A reduction of a source distribution is a collection of smaller sized distributions that are collectively equivalent to the source distribution with respect to the property of decomposability. That is, an arbitrary language is decomposable with respect to the source distribution if and only if it is decomposable with respect to each smaller sized distribution (in the reduction). The notion of reduction of distributions has previously been proposed to improve the complexity of decomposability verification. In this paper, we address the problem of generating (optimal) reductions of distributions automatically. A (partial) solution to this problem is provided, which consists of an incremental algorithm for the production of candidate reductions and a reduction validation procedure. In the incremental production stage, backtracking is applied whenever a candidate reduction that cannot be validated is produced. A strengthened substitution-based proof technique is used for reduction validation, while a fixed template of candidate counter examples is used for reduction refutation, put together, they constitute our (partial) solution to the reduction verification problem. In addition, we show that a recursive approach for the generation of (small) reductions is easily supported.

Název v anglickém jazyce

Automatic generation of optimal reductions of distributions

Popis výsledku anglicky

A reduction of a source distribution is a collection of smaller sized distributions that are collectively equivalent to the source distribution with respect to the property of decomposability. That is, an arbitrary language is decomposable with respect to the source distribution if and only if it is decomposable with respect to each smaller sized distribution (in the reduction). The notion of reduction of distributions has previously been proposed to improve the complexity of decomposability verification. In this paper, we address the problem of generating (optimal) reductions of distributions automatically. A (partial) solution to this problem is provided, which consists of an incremental algorithm for the production of candidate reductions and a reduction validation procedure. In the incremental production stage, backtracking is applied whenever a candidate reduction that cannot be validated is produced. A strengthened substitution-based proof technique is used for reduction validation, while a fixed template of candidate counter examples is used for reduction refutation, put together, they constitute our (partial) solution to the reduction verification problem. In addition, we show that a recursive approach for the generation of (small) reductions is easily supported.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

20205 - Automation and control systems

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

IEEE Transactions on Automatic Control

ISSN

0018-9286

e-ISSN

—

Svazek periodika

64

Číslo periodika v rámci svazku

3

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

16

Strana od-do

896-911

Kód UT WoS článku

000460415600002

EID výsledku v databázi Scopus

2-s2.0-85045751913