Evènement pour le groupe Modélisation et Verification


Date 2010-02-18  11:30-12:45
TitreOn 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. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurPeter Habermehl 
Emailpeter.habermehl@liafa.jussieu.fr 
UrlLIAFA 



Aucun document lié à cet événement.

Retour
Retour à l'index