Stéphanie Delaune: Associative-Commutative Deducibility Constraints

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},
}