|
Evènement pour le groupe Modélisation et Verification
Date | 2010-02-18 11:30-12:45 |
Titre | On non-deterministic automata for Presburger arithmetic. |
Résumé | A well-known decision procedure for Presburger arithmetic (PA)
uses deterministic finite-state automata. While the complexity
of the decision procedure for PA based on quantifier elimination
is known (triple-exponential), the exact complexity of the
automata-based procedure was unknown. We show that it is triple-exponential
as well by analysing the structure of the non-deterministic automata
obtained during the construction building on results from Klaedtke.
Furthermore, we analyse the sizes of deterministic and non-deterministic
automata built for several subclasses of Presburger arithmetic.
To retain a canonical representation which is one of the strengths of
the use of automata we use a class of non-deterministic automata
called residual finite-state automata introduced by Denis, Lemay and Terlutte. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Peter Habermehl |
Email | peter.habermehl@liafa.jussieu.fr |
Url | LIAFA |
Aucun document lié à cet événement. RetourRetour à l'index
| |