Interuniversity Attraction Poles program MoVES; Grant 2.4530.02; ANR-06-SETI-001 AVERISS
Funders :
BELSPO - SPP Politique scientifique - Service Public Fédéral de Programmation Politique scientifique F.R.S.-FNRS - Fonds de la Recherche Scientifique [BE] ANR - Agence Nationale de la Recherche [FR]
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves, Warsaw, pp. 92-101 (1929)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Methodoloy and Philosophy of Science, pp. 1-12. Stanford University Press, Stanford (1962)
Bruyère, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society 1(2), 191-238 (1994)
Boigelot, B.: Symbolic methods for exploring infinite state spaces. PhD thesis, Universitéde Liège (1998)
Cobham, A.: On the base-dependence of sets of numbers recognizable by finite automata. Mathematical Systems Theory 3, 186-192 (1969)
Semenov, A.: Presburgerness of predicates regular in two number systems. Siberian Mathematical Journal 18, 289-299 (1977)
Boigelot, B., Bronne, L., Rassart, S.: An improved reachability analysis method for strongly linear hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 167-177. Springer, Heidelberg (1997)
The Liège Automata-based Symbolic Handler (LASH), http://www.montefiore.ulg.ac.be/̃boigelot/research/lash/
Becker, B., Dax, C., Eisinger, J., Klaedtke, F.: LIRA: Handling constraints of linear arithmetics over the integers and the reals. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 307-310. Springer, Heidelberg (2007)
Boigelot, B., Brusten, J., Bruyère, V.: On the sets of real numbers recognized by finite automata in multiple bases. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 112-123. Springer, Heidelberg (2008)
Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Transactions on Computational Logic 6(3), 614-633 (2005)
van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B. Elsevier and MIT Press (1990)
Vardi, M.: The Büchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12-22. Springer, Heidelberg (2007)
Löding, C.: Efficient minimization of deterministic weak ω-automata. Information Processing Letters 79(3), 105-109 (2001)
Boigelot, B., Rassart, S., Wolper, P.: On the expressiveness of real and integer arithmetic automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 152-163. Springer, Heidelberg (1998)
Perrin, D., Pin, J.: Infinite words. Pure and Applied Mathematics, vol. 141. Elsevier, Amsterdam (2004)
Boigelot, B., Brusten, J.: A generalization of Cobham's theorem to automata over real numbers. Theoretical Computer Science (2009) (in press)
Ferrante, J., Rackoff, C.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer, Heidelberg (1979)
Hardy, G.H., Wright, E.M.: An introduction to the theory of numbers, 5th edn. Oxford University Press, Oxford (1985)
Wilke, T.: Locally threshold testable languages of infinite words. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, pp. 607-616. Springer, Heidelberg (1993)
Bryant, R.: Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys 24(3), 293-318 (1992)
Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: Proc. ACM SIGSAM ISSAC, Vancouver, pp. 129-136. ACM Press, New York (1999)
Eisinger, J., Klaedtke, F.: Don't care words with an application to the automata-based approach for real addition. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 67-80. Springer, Heidelberg (2006)
Latour, L.: Presburger arithmetic: from automata to formulas. PhD thesis, UniversitédeLiège (2005)
Leroux, J.: A polynomial time Presburger criterion and synthesis for number decision diagrams. In: Proc. 20th LICS, Chicago, pp. 147-156. IEEE Computer Society, Los Alamitos (2005)
