Lowerbounds for Bisimulation by Partition Refinement
We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $\Omega((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $\Omega(n...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2023-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/9212/pdf |
| _version_ | 1797268430044266496 |
|---|---|
| author | Jan Friso Groote Jan Martens Erik. P. de Vink |
| author_facet | Jan Friso Groote Jan Martens Erik. P. de Vink |
| author_sort | Jan Friso Groote |
| collection | DOAJ |
| description | We provide time lower bounds for sequential and parallel algorithms deciding
bisimulation on labeled transition systems that use partition refinement. For
sequential algorithms this is $\Omega((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu
\log \mkern-1mu n)$ and for parallel algorithms this is $\Omega(n)$, where $n$
is the number of states and $m$ is the number of transitions. The lowerbounds
are obtained by analysing families of deterministic transition systems,
ultimately with two actions in the sequential case, and one action for parallel
algorithms. For deterministic transition systems with one action, bisimilarity
can be decided sequentially with fundamentally different techniques than
partition refinement. In particular, Paige, Tarjan, and Bonic give a linear
algorithm for this specific situation. We show, exploiting the concept of an
oracle, that this approach is not of help to develop a faster generic algorithm
for deciding bisimilarity. For parallel algorithms there is a similar situation
where these techniques may be applied, too. |
| first_indexed | 2024-04-25T01:32:21Z |
| format | Article |
| id | doaj.art-6b289ff7214a4708babba44f72ce5fd7 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:32:21Z |
| publishDate | 2023-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-6b289ff7214a4708babba44f72ce5fd72024-03-08T10:59:15ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742023-05-01Volume 19, Issue 210.46298/lmcs-19(2:10)20239212Lowerbounds for Bisimulation by Partition RefinementJan Friso Grootehttps://orcid.org/0000-0003-2196-6587Jan Martenshttps://orcid.org/0000-0003-4797-7735Erik. P. de VinkWe provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $\Omega((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $\Omega(n)$, where $n$ is the number of states and $m$ is the number of transitions. The lowerbounds are obtained by analysing families of deterministic transition systems, ultimately with two actions in the sequential case, and one action for parallel algorithms. For deterministic transition systems with one action, bisimilarity can be decided sequentially with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that this approach is not of help to develop a faster generic algorithm for deciding bisimilarity. For parallel algorithms there is a similar situation where these techniques may be applied, too.https://lmcs.episciences.org/9212/pdfcomputer science - logic in computer science |
| spellingShingle | Jan Friso Groote Jan Martens Erik. P. de Vink Lowerbounds for Bisimulation by Partition Refinement Logical Methods in Computer Science computer science - logic in computer science |
| title | Lowerbounds for Bisimulation by Partition Refinement |
| title_full | Lowerbounds for Bisimulation by Partition Refinement |
| title_fullStr | Lowerbounds for Bisimulation by Partition Refinement |
| title_full_unstemmed | Lowerbounds for Bisimulation by Partition Refinement |
| title_short | Lowerbounds for Bisimulation by Partition Refinement |
| title_sort | lowerbounds for bisimulation by partition refinement |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/9212/pdf |
| work_keys_str_mv | AT janfrisogroote lowerboundsforbisimulationbypartitionrefinement AT janmartens lowerboundsforbisimulationbypartitionrefinement AT erikpdevink lowerboundsforbisimulationbypartitionrefinement |