[ list |
abstracts |
bib ]

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

paper pdf
paper ps
### 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.

### 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,
localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08FractionalCollections.pdf}
}

[ list |
abstracts |
bib ]