Cardinality constraints for arrays (decidability results and applications)

Enriching logic formalisms with counting capabilities is an important task in view of the needs of many application areas, ranging from database theory to formal verification. In this paper, we consider a very expressive language obtained by enriching linear integer arithmetic with free function symbols and cardinality constraints for interpreted sets. We obtain positive results for a flat fragment via a reduction to decidability of Presburger arithmetic with unary counting quantifiers (Schweikhart in Arithmetic, first-order logic, and counting quantifiers, ACM TOCL, New York, 2004). We isolate also an easier simple flat subfragment, whose satisfiability is in NP, and we show that this subfragment is adequate to formalize problems arising in the area of the verification of fault-tolerant distributed algorithms. We finally discuss our first implementation, the related experimental results, as well as further algorithmic problems suggested by model-checking applications.