We consider decidability question for simulation preorder (and equivalence) for processes generated by one-counter machines. We sketch a proof of decidability inthe case when testing for zero is not possible, and demonstrate the undecidability in the general case.
展开▼