The Complexity of Bisimilarity-Checking for One-Counter Processes

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	KUČERA Antonín
Year of publication	2003
Type	Article in Periodical
Magazine / Source	Theoretical Computer Science
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	concurrency; one-counter automata; bisimilarity
Description	We study the problem of bisimilarity-checking between processes of one-counter automata and finite-state processes. We show that deciding weak bisimilarity between processes of one-counter nets and finite-state processes is DP-hard. 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 characterization of all hard instances as a byproduct.
Related projects:	Verification of infinite-state systems Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing