Sciweavers

LICS
2009
IEEE

On the Computational Complexity of Verifying One-Counter Processes

14 years 5 months ago
On the Computational Complexity of Verifying One-Counter Processes
—One-counter processes are pushdown systems over a singleton stack alphabet (plus a stack-bottom symbol). We study the complexity of two closely related verification problems over one-counter processes: model checking with the temporal logic EF, where formulas are given as directed acyclic graphs, and weak bisimilarity checking against finite systems. We show that both problems are PNP -complete. This is achieved by establishing a close correspondence with the membership problem for a natural fragment of Presburger Arithmetic, which we show to be PNP -complete. This fragment is also a suitable representation for the global versions of the problems. We also show that there already exists a fixed EF formula (resp. a fixed finite system) such that model checking (resp. weak bisimulation) over one-counter processes is hard for PNP[log] . However, the complexity drops to P if the onecounter process is fixed. Keywords-Complexity theory, Logic
Stefan Göller, Richard Mayr, Anthony Widjaja
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where LICS
Authors Stefan Göller, Richard Mayr, Anthony Widjaja To
Comments (0)