Kvantitativní analýza pravděpodobnostních zásobníkových automatů: střední hodnoty a rozptyl

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F05%3A00012515" target="_blank" >RIV/00216224:14330/05:00012515 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Popis výsledku v původním jazyce

Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulatedreward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.

Název v anglickém jazyce

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Popis výsledku anglicky

Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulatedreward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2005

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 statě ve sborníku

Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005)

ISBN

0-7695-2266-1

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

117-126

Název nakladatele

IEEE Computer Society

Místo vydání

Los Alamitos, California

Místo konání akce

Chicago, Illinois, USA

Datum konání akce

26. 7. 2005

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—