D 2005

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

ESPARZA, Javier, Antonín KUČERA a Richard MAYR

Základní údaje

Originální název

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Název česky

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

Autoři

ESPARZA, Javier (724 Španělsko), Antonín KUČERA (203 Česká republika, garant) a Richard MAYR (276 Německo)

Vydání

Los Alamitos, California, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), od s. 117-126, 10 s. 2005

Nakladatel

IEEE Computer Society

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/05:00012515

Organizační jednotka

Fakulta informatiky

ISBN

0-7695-2266-1

UT WoS

000230786500013

Klíčová slova anglicky

Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 17:28, prof. RNDr. Antonín Kučera, Ph.D.

Anotace

ORIG CZ

V originále

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 accumulated reward 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.

Česky

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.

Návaznosti

GA201/03/1161, projekt VaV
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky