Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Original language description

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.

Czech name

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

Czech description

Pravděpodobnostní zásobníkové automaty jsou přirozeným modelem pro pravděpodobnostní programy obsahující rekurzivní procedury. V článku se soustředíme na výpočet středních hodnot a rozptylu jistých náhodných proměnných definovaných na bězích daného zásbníkového automatu. Pomocí těchto výsledků lze dále vypočítat různé kvantitativní charakteristiky pravděpodobnostních zásobníkových automatů, které nelze vyjádřit v běžných temporálních logikách.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2005

Confidentiality

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

Article name in the collection

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

ISBN

0-7695-2266-1

ISSN

—

e-ISSN

—

Number of pages

10

Pages from-to

117-126

Publisher name

IEEE Computer Society

Place of publication

Los Alamitos, California

Event location

Chicago, Illinois, USA

Event date

Jul 26, 2005

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—