## Associative-Commutative Deducibility Constraints

Sergiu Bursuc, Hubert Comon-Lundh, and Stéphanie Delaune. Associative-Commutative Deducibility Constraints. In * Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science (STACS'07)*, pp. 634–645, Lecture Notes in Computer Science 4393, Springer, Aachen, Germany, February 2007.

### Download

[PDF]

### Abstract

We consider deducibility constraints, which are equivalent to particular Diophantine systems, arising in the automatic verification of security protocols, in presence of associative and commutative symbols. We show that deciding such Diophantine systems is, in general, undecidable. Then, we consider a simple subclass, which we show decidable. Though the solutions of these problems are not necessarily semi-linear sets, we show that there are (computable) semi-linear sets whose minimal solutions are not too far from the minimal solutions of the system. Finally, we consider a small variant of the problem, for which there is a much simpler decision algorithm.

### BibTeX

@inproceedings{BCD-stacs2007,
abstract = {We consider deducibility constraints, which are
equivalent to particular Diophantine systems, arising
in the automatic verification of security protocols,
in presence of associative and commutative symbols.
We show that deciding such Diophantine systems is, in
general, undecidable. Then, we consider a simple
subclass, which we show decidable. Though the
solutions of these problems are not necessarily
semi-linear sets, we show that there are (computable)
semi-linear sets whose minimal solutions are not too
far from the minimal solutions of the system.
Finally, we consider a small variant of the problem,
for which there is a much simpler decision
algorithm.},
address = {Aachen, Germany},
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 24th {A}nnual {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'07)},
OPTDOI = {10.1007/978-3-540-70918-3_54},
editor = {Thomas, Wolfgang and Weil, Pascal},
month = feb,
pages = {634-645},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Associative-Commutative Deducibility Constraints},
volume = {4393},
year = {2007},
acceptrate = {56/400},
acronym = {{STACS}'07},
nmonth = {2},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}