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.

Cardinality constraints for arrays (decidability results and applications) / F. Alberti, S. Ghilardi, E. Pagani. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - (2017). [Epub ahead of print]

Cardinality constraints for arrays (decidability results and applications)

S. Ghilardi;E. Pagani
2017

Abstract

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.
Arrays; Cardinality constraints; Fault-tolerant systems
Settore INF/01 - Informatica
21-apr-2017
FORMAL METHODS IN SYSTEM DESIGN
Article (author)
File in questo prodotto:
File Dimensione Formato  
FMSD_apr17_PREPRINT.pdf

non disponibili

Descrizione: Articolo completo - versione online su sito editore
745 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/491185
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 2
social impact