All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Model Checking Probabilistic Pushdown Automata

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010191" target="_blank" >RIV/00216224:14330/04:00010191 - isvavai.cz</a>

  • Result on the web

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    Model Checking Probabilistic Pushdown Automata

  • Original language description

    We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove thatboth qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant modelchecking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

  • Czech name

    Ověřování platnosti formulí temporálních logik pro procesy zásobníkových automatů

  • Czech description

    V práci je rozebrána problematika automatického ověřování platnosti formulí temporálních logik pro procesy pravděpodobnostních zásobníkových automatů. Nejprve je uvažována třída vlastností, která je formulovatelná jako zobecněný problém náhodné procházky. Je dokázáno, že kvalitativní i kvantitativní varianta tohoto problému je rozhodnutelná. Pak je dokázána rozhodnutelnost problému platnosti dané formule kvalitativního fragmentu logiky PCTL pro daný zásobníkový proces. Jsou také uvažovány vlastnosti popsatelné pomocí deterministických Buchiho automatů a ukázána rozhodnutelnost příslušných problémů.

Classification

  • Type

    D - Article in proceedings

  • CEP classification

    IN - Informatics

  • OECD FORD branch

Result continuities

  • Project

    <a href="/en/project/GA201%2F03%2F1161" target="_blank" >GA201/03/1161: Verification of infinite-state systems</a><br>

  • Continuities

    Z - Vyzkumny zamer (s odkazem do CEZ)

Others

  • Publication year

    2004

  • Confidentiality

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

Data specific for result type

  • Article name in the collection

    Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)

  • ISBN

    0-7695-2192-4

  • ISSN

  • e-ISSN

  • Number of pages

    10

  • Pages from-to

    12-21

  • Publisher name

    IEEE Computer Society

  • Place of publication

    Los Alamitos (California)

  • Event location

    Turku, Finland

  • Event date

    Jul 13, 2004

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article