Dense Counter Machines and Verification Problems

We generalize the traditional definition of a multicounter machine (where the counters, which can only assume nonnegative integer values, can be incremented/decremented by 1 and tested for zero) by allowing the machine the additional ability to increment/decrement the counters by a nondeterministically chosen fractional amount

• Type: Conference
• Year: 2003
• Where: CAV
• Authors: Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro
• Keywords: Binary Reachability Set, CAV 2003, Hardware, Nonnegative Integer Values, Semilinear Language