Decision Procedures for Multisets with Cardinality Constraints

paper ps   
Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the content of linked data structure with duplicate elements leads to multisets. Interactive theorem provers such as Isabelle specify theories of multisets and prove a number of theorems about them to enable their use in interactive verification. However, the decidability and complexity of constraints on multisets is much less understood than for constraints on sets. The first contribution of this paper is a polynomial-space algorithm for deciding expressive quantifier-free constraints on multisets with cardinality operators. Our decision procedure reduces in polynomial time constraints on multisets to constraints in an extension of quantifier-free Presburger arithmetic with certain “unbounded sum” expressions. We prove bounds on solutions of resulting constraints and describe a polynomial-space decision procedure for these constraints. The second contribution of this paper is a proof that adding quantifiers to a constraint language containing subset and cardinality operators yields undecidable constraints. The result follows by reduction from Hilbert's 10th problem.

Citation

Ruzica Piskac and Viktor Kuncak. Decision procedures for multisets with cardinality constraints. In 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, 2008.

BibTex Entry

@inproceedings{PiskacKuncak08DecisionProceduresMultisetsCardinality,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Decision Procedures for Multisets with Cardinality Constraints},
  booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  series = {LNCS},
  year = 2008,
  abstract = { Applications in software verification and interactive
theorem proving often involve reasoning about sets of
objects.  Cardinality constraints on such collections also
arise in these scenarios.  Multisets arise
for analogous reasons as sets: abstracting the
content of linked data structure with duplicate elements
leads to multisets.  Interactive theorem provers such as
Isabelle specify theories of multisets and prove a number of
theorems about them to enable their 
use in interactive verification.  
However, the decidability and
complexity of constraints on multisets is much less understood
than for constraints on sets.
The first contribution of this paper is a polynomial-space
algorithm for deciding expressive quantifier-free
constraints on multisets with cardinality operators.  Our
decision procedure reduces in polynomial time constraints on
multisets to constraints in an extension of quantifier-free
Presburger arithmetic with certain ``unbounded sum'' expressions.  We
prove bounds on solutions of resulting constraints and
describe a polynomial-space decision procedure for these
constraints.
The second contribution of this paper is a proof that adding
quantifiers to a constraint language containing subset and
cardinality operators yields undecidable constraints.  The
result follows by reduction from Hilbert's 10th problem.
}
}