Output details
11 - Computer Science and Informatics
University of Edinburgh
Decidability of Weak Simulation on One-Counter Nets
<10> Originality: Solution of two long-standing open problems on semantic preorders.
Significance: Due to the difficulties of handling infinite branching induced by weak internal actions, there are hardly any algorithms for checking weak semantic preorders/equivalences on infinite-state systems. This paper describes a major new technique for computing approximants to weak simulation preorder and shows its decidability on one-counter nets, thus settling a question that has been open for more than 15 years. The result is very surprising, since both finer and coarser preorders are undecidable.
Rigour: The paper (24p with electronic appendices) provides full formal details of all proofs.