About: Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof) Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://www.lmcs-online.org/ojs/viewarticle.php?id=1216
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). (en)
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) (en)
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) (en)
skos:notation	RIV/61989100:27240/13:86088903!RIV14-GA0-27240___
http://linked.open...avai/predkladatel	Fakulta elektrotechniky a informatiky
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(ED1.1.00/02.0070), P(GAP202/11/0340)
http://linked.open...iv/cisloPeriodika	1:10
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Jančar, Petr
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoká škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky
http://linked.open...dnocenehoVysledku	63597
http://linked.open...ai/riv/idVysledku	RIV/61989100:27240/13:86088903
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	complexity; basic process algebra; bisimulation equivalence (en)
http://linked.open.../riv/klicoveSlovo	basic process algebra bisimulation equivalence complexity
http://linked.open...odStatuVydavatele	DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV	[FFFDD15A01FB]
http://linked.open...i/riv/nazevZdroje	Logical Methods in Computer Science
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	1 (xsd:int)
http://linked.open...vavai/riv/projekt	IT4Innovations Centre of Excellence Modelling and verification of parallel systems
http://linked.open...UplatneniVysledku	2013
http://linked.open...v/svazekPeriodika	9
http://linked.open...iv/tvurceVysledku	Jančar, Petr
http://linked.open...ain/vavai/riv/wos	000317894100005
issn	1860-5974
number of pages	19 (xsd:int)
http://bibframe.org/vocab/doi	10.2168/LMCS-9(1:10)2013
http://localhost/t...ganizacniJednotka	27240

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 47 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software