This HTML5 document contains 42 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n13http://localhost/temp/predkladatel/
n20http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n8http://linked.opendata.cz/resource/domain/vavai/projekt/
n14http://linked.opendata.cz/resource/domain/vavai/subjekt/
n3http://linked.opendata.cz/ontology/domain/vavai/
shttp://schema.org/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/
rdfshttp://www.w3.org/2000/01/rdf-schema#
skoshttp://www.w3.org/2004/02/skos/core#
n7http://bibframe.org/vocab/
n16http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F61989100%3A27240%2F13%3A86088903%21RIV14-GA0-27240___/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n11http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n10http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n21http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n18http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n15http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F61989100%3A27240%2F13%3A86088903%21RIV14-GA0-27240___
rdf:type
n3:Vysledek skos:Concept
rdfs:seeAlso
http://www.lmcs-online.org/ojs/viewarticle.php?id=1216
dcterms:description
Burkart, Caucal, Steffen (1995) showed a procedure deciding bisimulation equivalence of processes in Basic Process Algebra (BPA), i.e. of sequential processes generated by context-free grammars. They improved the previous decidability result of Christensen, Hüttel, Stirling (1992), since their procedure has obviously an elementary time complexity and the authors claim that a close analysis would reveal a double exponential upper bound. Here a self-contained direct proof of the membership in 2-ExpTime is given. This is done via a Prover-Refuter game which shows that there is an alternating Turing machine deciding the problem in exponential space. The proof uses similar ingredients (size-measures, decompositions, bases) as the previous proofs, but one new simplifying factor is an explicit addition of infinite regular strings to the state space. An auxiliary claim also shows an explicit exponential upper bound on the equivalence level of nonbisimilar normed BPA processes. The importance of clarifying the 2-ExpTime upper bound for BPA bisimilarity has recently increased due to the shift of the known lower bound from PSpace (Srba, 2002) to ExpTime (Kiefer, 2012). Burkart, Caucal, Steffen (1995) showed a procedure deciding bisimulation equivalence of processes in Basic Process Algebra (BPA), i.e. of sequential processes generated by context-free grammars. They improved the previous decidability result of Christensen, Hüttel, Stirling (1992), since their procedure has obviously an elementary time complexity and the authors claim that a close analysis would reveal a double exponential upper bound. Here a self-contained direct proof of the membership in 2-ExpTime is given. This is done via a Prover-Refuter game which shows that there is an alternating Turing machine deciding the problem in exponential space. The proof uses similar ingredients (size-measures, decompositions, bases) as the previous proofs, but one new simplifying factor is an explicit addition of infinite regular strings to the state space. An auxiliary claim also shows an explicit exponential upper bound on the equivalence level of nonbisimilar normed BPA processes. The importance of clarifying the 2-ExpTime upper bound for BPA bisimilarity has recently increased due to the shift of the known lower bound from PSpace (Srba, 2002) to ExpTime (Kiefer, 2012).
dcterms:title
Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof) Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)
skos:prefLabel
Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof) Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)
skos:notation
RIV/61989100:27240/13:86088903!RIV14-GA0-27240___
n3:predkladatel
n14:orjk%3A27240
n6:aktivita
n21:P
n6:aktivity
P(ED1.1.00/02.0070), P(GAP202/11/0340)
n6:cisloPeriodika
1:10
n6:dodaniDat
n15:2014
n6:domaciTvurceVysledku
n20:6026508
n6:druhVysledku
n19:J
n6:duvernostUdaju
n10:S
n6:entitaPredkladatele
n16:predkladatel
n6:idSjednocenehoVysledku
63597
n6:idVysledku
RIV/61989100:27240/13:86088903
n6:jazykVysledku
n18:eng
n6:klicovaSlova
complexity; basic process algebra; bisimulation equivalence
n6:klicoveSlovo
n11:complexity n11:bisimulation%20equivalence n11:basic%20process%20algebra
n6:kodStatuVydavatele
DE - Spolková republika Německo
n6:kontrolniKodProRIV
[FFFDD15A01FB]
n6:nazevZdroje
Logical Methods in Computer Science
n6:obor
n12:IN
n6:pocetDomacichTvurcuVysledku
1
n6:pocetTvurcuVysledku
1
n6:projekt
n8:GAP202%2F11%2F0340 n8:ED1.1.00%2F02.0070
n6:rokUplatneniVysledku
n15:2013
n6:svazekPeriodika
9
n6:tvurceVysledku
Jančar, Petr
n6:wos
000317894100005
s:issn
1860-5974
s:numberOfPages
19
n7:doi
10.2168/LMCS-9(1:10)2013
n13:organizacniJednotka
27240