A note on Presburger arithmetic with array segments, permutation and equality

DOI10.1016/0020-0190(86)90039-6MaRDI QIDQ1073009zbMATH OpenOpenAlexFDO

Authors Louis E. Rosier

Publication date 1986

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(86)90039-6

zbMATH Keywords

satisfiability problemsecond order predicatesvalidity problem

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

In this paper, we examine the validity (satisfiability) problem for a language containing Presburger arithmetic, finite length array segments and some fixed second order predicates. In particular, we consider the predicates: PERM, which is used to assert that two array segments contain the same multiset of elements, and \(=\) (equality), which is used to assert that two array segments are identical (i.e., contain the same sequence of elements and have equivalent upper and lower array bounds). It is known that the afore-mentioned (unquantified) language has a decidable validity problem. (In fact, the satisfiability problem is NP- complete.) We consider the case when equality is defined in a seemingly weaker fashion. Let \(Y\simeq B\) be true if and only if array segments A and B contain the same sequence of elements. This definition of equality is more useful in the verification conditions of programs that manipulate queues and/or strings. However, we show that when this form of equality replaces the earlier variety in the previously mentioned language, the validity problem becomes undecidable.

Recommendations

• What's decidable about sequences?
• Verification, Model Checking, and Abstract Interpretation
• What Else Is Decidable about Integer Arrays?
• Decision procedures for extensions of the theory of arrays
• Schemata of formulæ in the theory of arrays

Cites work

• A Decision Procedure for the Correctness of a Class of Programs
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• Presburger arithmetic with array segments
• Reasoning about arrays
• Verification Decidability of Presburger Array Programs

Cited in

(1)

• Constructing fully symmetric cubature formulae for the sphere

This page was built for publication: A note on Presburger arithmetic with array segments, permutation and equality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1073009)