D 2005

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

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

Basic information

Original name

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

Name in Czech

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

Authors

ESPARZA, Javier (724 Spain), Antonín KUČERA (203 Czech Republic, guarantor) and Richard MAYR (276 Germany)

Edition

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

Publisher

IEEE Computer Society

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/05:00012515

Organization unit

Faculty of Informatics

ISBN

0-7695-2266-1

UT WoS

000230786500013

Keywords in English

Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis

Tags

Tags

International impact, Reviewed
Změněno: 22/11/2006 17:28, prof. RNDr. Antonín Kučera, Ph.D.

Abstract

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.

In Czech

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.

Links

GA201/03/1161, research and development project
Name: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Verification of infinite-state systems
MSM0021622419, plan (intention)
Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1M0545, research and development project
Name: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science