Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

paper ps   
We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unknown size) to a subset of rational numbers specified by user-defined constraints in mixed linear integer-rational arithmetic. Our logic supports standard operators such as union, intersection, difference, or any operation defined pointwise using mixed linear integer-rational arithmetic. Moreover, it supports the notion of cardinality of the collection. Deciding formulas in such logic has application in verification of data structures. Our decision procedure reduces satisfiability of formulas with collections to satisfiability of formulas in an extension of mixed linear integer-rational arithmetic with an “unbounded sum” operator. Such extension is also interesting in its own right because it can encode reachability problems for a simple class of transition systems. We present a decision procedure for the resulting extension, using a satisfiability-preserving transformation that eliminates the unbounded sum operator. Our decidability result subsumes previous special cases for sets and multisets.

Citation

Ruzica Piskac and Viktor Kuncak. Fractional collections with cardinality bounds, and mixed integer linear arithmetic with stars. In Computer Science Logic (CSL), 2008.

BibTex Entry

@inproceedings{PiskacKuncak08FractionalCollections,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Fractional Collections with Cardinality Bounds, 
and Mixed Integer Linear Arithmetic with Stars},
  booktitle = {Computer Science Logic (CSL)},
  year = 2008,
  abstract = {
We present decision procedures for logical constraints that
support reasoning about collections of elements such as
sets, multisets, and fuzzy sets.  Element membership in such
collections is given by a characteristic function from a
finite universe (of unknown size) to a subset of rational
numbers specified by user-defined constraints in mixed
linear integer-rational arithmetic.  Our logic supports
standard operators such as union, intersection, difference,
or any operation defined pointwise using mixed linear
integer-rational arithmetic.  Moreover, it supports the
notion of cardinality of the collection.  Deciding formulas
in such logic has application in verification of data
structures.
Our decision procedure reduces satisfiability of formulas
with collections to satisfiability of formulas in an
extension of mixed linear integer-rational arithmetic with
an ``unbounded sum'' operator.  Such extension is also
interesting in its own right because it can encode
reachability problems for a simple class of transition
systems.  We present a decision procedure for the resulting
extension, using a satisfiability-preserving transformation
that eliminates the unbounded sum operator.  Our
decidability result subsumes previous special cases for sets
and multisets.
}
}