Abstract | ||
---|---|---|
We study the problem of bisimilarity-checking between processes of one-counter au- tomata and finite-state processes. We show that deciding weak bisimilarity between processes of one-counter nets (which are 'restricted' one-counter automata where the counter cannot be tested for zero) and finite-state processes is DP-hard. In particular, this means that the problem is both NP and co-NP hard. The same technique is used to demonstrate co-NP-hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for a large subclass of instances, giving a kind of charac- terization of all hard instances as a byproduct. Moreover, we show how to efficiently estimate the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in P. |
Year | DOI | Venue |
---|---|---|
2003 | 10.1016/S0304-3975(03)00081-1 | Theoretical Computer Science |
Keywords | DocType | Volume |
one-counter net,large subclass,one-counter automata,weak bisimilarity,bisimilarity,one-counter automaton,hard instance,strong bisimilarity,finite-state process,one-counter nets,one-counter process | Journal | 304 |
Issue | ISSN | Citations |
1 | Theoretical Computer Science | 4 |
PageRank | References | Authors |
0.46 | 31 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Antonín Kučera | 1 | 262 | 18.04 |