English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Burkart, Caucal, Steffen (1995) showed a procedure deciding bisimulationequivalence of processes in Basic Process Algebra (BPA), i.e. of sequentialprocesses generated by context-free grammars. They improved the previousdecidability result of Christensen, H\"uttel, Stirling (1992), since theirprocedure has obviously an elementary time complexity and the authors claimthat a close analysis would reveal a double exponential upper bound. Here aself-contained direct proof of the membership in 2-ExpTime is given. This isdone via a Prover-Refuter game which shows that there is an alternating Turingmachine deciding the problem in exponential space. The proof uses similaringredients (size-measures, decompositions, bases) as the previous proofs, butone new simplifying factor is an explicit addition of infinite regular stringsto the state space. An auxiliary claim also shows an explicit exponential upperbound on the equivalence level of nonbisimilar normed BPA processes. Theimportance of clarifying the 2-ExpTime upper bound for BPA bisimilarity hasrecently increased due to the shift of the known lower bound from PSpace (Srba,2002) to ExpTime (Kiefer, 2012).

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