RIV/61989100:27240/12:86084986 - Bisimilarity of Probabilistic Pushdown Automata (2012)

Údaje o výsledku
Identifikační kódRIV/61989100:27240/12:86084986
Název v původním jazyceBisimilarity of Probabilistic Pushdown Automata
DruhD - Článek ve sborníku
Jazykeng - angličtina
OborIN - Informatika
Rok uplatnění2012
Kód důvěrnosti údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Počet výskytů výsledku2
Údaje z Hodnocení výsledků výzkumných organizací 2014
Výsledek byl hodnocen v Pilíři I
Rozsah vyřazení výsledkuTento výskyt výsledku není vyřazen
Zařazení výsledku v hodnoceníD - Článek ve sborníku
Skupina oboru v hodnocení04 - Technické a informatické vědy
Konkrétní způsob(y) hodnocení výsledkuVýsledek hodnocený již v předchozím hodnocení, body se přebírají
Bodové ohodnocení8,000
Faktor korekce77,6 %
Body (upravené podle přílohy č. 8 Metodiky)6,205
Rozdělení výsledku mezi předkladatele
OrganizaceVýzkumná organizace?PodílBodyBody (upravené podle přílohy č. 8 Metodiky)
Masarykova univerzita / Fakulta informatikyano33,3 %2,6672,068
Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatikyano33,3 %2,6672,068
Tvůrci výsledku
Počet tvůrců celkem4
Počet domácích tvůrců1
TvůrceForejt Vojtěch (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska)
TvůrceJančar Petr (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 6026508)
TvůrceKiefer Stefan (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska)
TvůrceWorrell James (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska)
Údaje blíže specifikující výsledek
Popis v původním jazyceWe study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata (without epsilon-transitions). Our first contribution is a general construction that reduces checking bisimilarity of probabilistic transition systems to checking bisimilarity of non-deterministic transition systems. This construction directly yields decidability of bisimilarity for pPDA, as well as an elementary upper bound for the bisimilarity problem on the subclass of probabilistic basic process algebras, i.e., single-state pPDA. We further show that, with careful analysis, the general reduction can be used to prove an EXPTIME upper bound for bisimilarity of probabilistic visibly pushdown automata. Here we also provide a matching lower bound, establishing EXPTIME-completeness. Finally we prove that deciding bisimilarity of probabilistic one-counter automata, another subclass of pPDA, is PSPACE-complete. Here we use a more specialised argument to obtain optimal complexity bounds.
Klíčová slovapushdown automata; probabilistic systems; bisimilarity
Rozsah stran448-460
Název sborníkuIARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Forma vydáníE - Elektronická verze „online“
ISSN1868-8969
Počet stran výsledku13
ISBN978-3-939897-47-7
Název nakladateleSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Místo vydáníWadern
Místo konání akceHyderabad
Datum zahájení akce15.12.2012
Typ akce podle státní příslušnoti účastníkůWRD - Světová
Adresa www stránky s výsledkemhttp://drops.dagstuhl.de/opus/volltexte/2012/3880/
DOI výsledku10.4230/LIPIcs.FSTTCS.2012.448
Údaje o tomto záznamu o výsledku
PředkladatelVysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky
DodavatelGA0 - Grantová agentura České republiky (GA ČR)
Rok sběru2013
Systémové označení dodávky datRIV13-GA0-27240___/02:2
SpecifikaceRIV/61989100:27240/12:86084986!RIV13-GA0-27240___
Kontrolní kód[5474D823967A]
Další výskyty tohoto výsledku od jiných předkladatelů
Další předkladatelMasarykova univerzita / Fakulta informatiky
Dodáno MŠMT v roce 2013Záznam s identifikačním kódem RIV/00216224:14330/12:00064716 v dodávce dat RIV13-MSM-14330___/02:2
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
ProjektGAP202/11/0340 - Modelování a verifikace paralelních systémů (2011-2014, GA0/GA)
ProjektLA09016 - Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (2009-2012, MSM/LA)
I - Instit. podpora na rozvoj výzkumné organizace