BELSPO - Belgian Federal Science Policy Office F.R.S.-FNRS - Fonds de la Recherche Scientifique
Funding text :
Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office; Grant 2.4530.02 of the Belgian Fund for Scientific Research (F.R.S.-FNRS)
Avigad J., and Yin Y. Quantifier elimination for the reals with a predicate for the powers of two. Theoretical Computer Science 370 (2007) 48-59
B. Boigelot, Symbolic methods for exploring infinite state spaces, Ph.D. Thesis, Université de Liège, 1998
Boigelot B., Bronne L., and Rassart S. An improved reachability analysis method for strongly linear hybrid systems. Proc. 9th CAV. Lecture Notes in Computer Science vol. 1254 (June 1997), Springer, Haifa 167-177
Boigelot B., Jodogne S., and Wolper P. An effective decision procedure for linear arithmetic over the integers and reals. ACM Transactions on Computational Logic 6 3 (2005) 614-633
Boigelot B., and Latour L. Counting the solutions of Presburger equations without enumerating them. Theoretical Computer Science 313 (2004) 17-29
Boigelot B., Rassart S., and Wolper P. On the expressiveness of real and integer arithmetic automata. Proc. 25th ICALP. Lecture Notes in Computer Science vol. 1443 (July 1998), Springer, Aalborg 152-163
J. Brusten, Etude des propriétés des RVA, Graduate Thesis, Université de Liège, May 2006
Bruyère V., Hansel G., Michaux C., and Villemaire R. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society 1 2 (1994) 191-238
Büchi J.R. On a decision method in restricted second order arithmetic. Proc. International Congress on Logic, Methodology and Philosophy of Science (1962), Stanford University Press, Stanford 1-12
Cobham A. On the base-dependence of sets of numbers recognizable by finite automata. Mathematical Systems Theory 3 (1969) 186-192
Kupferman O., and Vardi M.Y. Complementation constructions for nondeterministic automata on infinite words. Proc. 11th TACAS. Lecture Notes in Computer Science vol. 3440 (April 2005), Springer, Edinburgh 206-221
L. Latour, Presburger arithmetic: From automata to formulas, Ph.D. Thesis, Université de Liège, 2005
Leroux J. A polynomial time Presburger criterion and synthesis for number decision diagrams. Proc. 20th LICS (June 2005), IEEE Computer Society, Chicago 147-156
Löding C. Efficient minimization of deterministic weak ω-automata. Information Processing Letters 79 3 (2001) 105-109
Presburger M. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves (1929), Warsaw 92-101
Safra S. On the complexity of ω-automata. Proc. 29th Symposium on Foundations of Computer Science (October 1988), IEEE Computer Society 319-327
Semenov A.L. Presburgerness of predicates regular in two number systems. Siberian Mathematical Journal 18 (1977) 289-299
van den Dries L. The field of reals with a predicate for the powers of two. Manuscripta Mathematica 54 (1985) 187-195
Villemaire R. The theory of 〈 N, +, Vk, Vl 〉 is undecidable. Theoretical Computer Science 106 2 (1992) 337-349
Wilke T. Locally threshold testable languages of infinite words. Proc. 10th STACS. Lecture Notes in Computer Science vol. 665 (1993), Springer, Würzburg 607-616
Wolper P., and Boigelot B. An automata-theoretic approach to Presburger arithmetic constraints. Proc. 2nd SAS. Lecture Notes in Computer Science vol. 983 (September 1995), Springer, Glasgow
Wolper P., and Boigelot B. Verifying systems with infinite but regular state spaces. Proc. 10th CAV. Lecture Notes in Computer Science vol. 1427 (June 1998), Springer, Vancouver 88-97
