@article{JANCAR2021,
    Abstract = {The main aim of this paper is to give a simple transparent proof of the result showing that the problem of bisimulation equivalence on the class of Basic Parallel Processes (BPP), denoted by BPP-Bisim, can be decided by a polynomial-space algorithm. This result (by the author) has been previously only presented in a conference version, in a rather technical form that is not easily readable and verifiable. Since the result has clarified the complexity of the problem BPP-Bisim, namely its PSPACE-completeness (using the lower bound by Srba), and the problem deals with a fundamental behavioural equivalence and with one of the simplest models that naturally extend finite-state systems into infinite-state ones, it seems appropriate to have a transparent version of the proof.},
    Author = {Jan{\v c}ar, Petr},
    File = {Bisimilarity on Basic Parallel Processes - 1-s2.0-S0304397521007027-main.pdf},
    ISSN = {0304-3975},
    Journal = {Theoretical Computer Science},
    Keywords = {Verification, Concurrency, Equivalence checking, Bisimulation equivalence, Basic parallel processes},
    Title = {Bisimilarity on Basic Parallel Processes},
    URL = {https://www.sciencedirect.com/science/article/pii/S0304397521007027},
    Year = {2021},
    bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397521007027},
    bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2021.11.027},
    date-added = {2021-12-14 15:35:00 +0100},
    date-modified = {2021-12-14 15:35:00 +0100},
    doi = {10.1016/j.tcs.2021.11.027}
}

@article{JANCAR2021, Abstract = {The main aim of this paper is to give a simple transparent proof of the result showing that the problem of bisimulation equivalence on the class of Basic Parallel Processes (BPP), denoted by BPP-Bisim, can be decided by a polynomial-space algorithm. This result (by the author) has been previously only presented in a conference version, in a rather technical form that is not easily readable and verifiable. Since the result has clarified the complexity of the problem BPP-Bisim, namely its PSPACE-completeness (using the lower bound by Srba), and the problem deals with a fundamental behavioural equivalence and with one of the simplest models that naturally extend finite-state systems into infinite-state ones, it seems appropriate to have a transparent version of the proof.}, Author = {Jan{\v c}ar, Petr}, File = {Bisimilarity on Basic Parallel Processes - 1-s2.0-S0304397521007027-main.pdf}, ISSN = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {Verification, Concurrency, Equivalence checking, Bisimulation equivalence, Basic parallel processes}, Title = {Bisimilarity on Basic Parallel Processes}, URL = {https://www.sciencedirect.com/science/article/pii/S0304397521007027}, Year = {2021}, bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397521007027}, bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2021.11.027}, date-added = {2021-12-14 15:35:00 +0100}, date-modified = {2021-12-14 15:35:00 +0100}, doi = {10.1016/j.tcs.2021.11.027} }