An effective decision procedure for linear arithmetic over the integers and reals

ABSTRACT

This article considers finite-automata-based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on infinite words, but this involves some difficult and delicate to implement algorithms. The contribution of this article is to show, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms, which have been successfully implemented.

REFERENCES

• 1: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 2: Boigelot, B. 1998. Symbolic methods for exploring infinite state spaces. Ph.D. dissertation. Université de Liège, Liège, Belgium.
• 3: Bernard Boigelot , Louis Bronne , Stéphane Rassart, An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract), Proceedings of the 9th International Conference on Computer Aided Verification, p.167-178, June 22-25, 1997
• 4: Bernard Boigelot , Sébastien Jodogne , Pierre Wolper, On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables, Proceedings of the First International Joint Conference on Automated Reasoning, p.611-625, June 18-23, 2001
• 5: Bernard Boigelot , Louis Latour, Counting the Solutions of Presburger Equations without Enumerating Them, Revised Papers from the 6th International Conference on Implementation and Application of Automata, p.40-51, July 23-25, 2001
• 6: Bernard Boigelot , Stéphane Rassart , Pierre Wolper, On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract), Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.152-163, July 13-17, 1998
• 7: Alexandre Boudet , Hubert Comon, Diophantine Equations, Presburger Arithmetic and Finite Automata, Proceedings of the 21st International Colloquium on Trees in Algebra and Programming, p.30-43, April 22-24, 1996
• 8: Bruyère, V., Hansel, G., Michaux, C., and Villemaire, R. 1994. Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc. 1, 2 (Mar.), 191--238.
• 9: Büchi, J. R. 1960. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66--92.
• 10: Büchi, J. R. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Method, and Philosophy of Science. Stanford University Press, Stanford, CA, 1--12.
• 11: Jan Chomicki , Tomasz Imieliński, Temporal deductive databases and infinite objects, Proceedings of the seventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.61-73, March 1988, Austin, Texas, United States [doi>10.1145/308386.308416]
• 12: Cobham, A. 1969. On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theor. 3, 186--192.
• 13: Costas Courcoubetis , Moshe Y. Vardi , Pierre Wolper , Mihalis Yannakakis, Memory Efficient Algorithms for the Verification of Temporal Properties, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.233-242, June 18-21, 1990
• 14: Ferrante, J. and Rackoff, C. W. 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer-Verlag, Berlin and Heidelberg, Germany/New York, NY.
• 15: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 16: Hopcroft, J. E. 1971. An n log n algorithm for minimizing states in a finite automaton. Theor. Mach. Computat. 189--196.
• 17: Helmut Jürgensen , Ludwig Staiger, Finite Automata Encoding Geometric Figures, Revised Papers from the 4th International Workshop on Automata Implementation, p.101-108, July 17-19, 1999
• 18: F. Kabanza , J.-M. Stevenne , P. Wolper, Handling infinite temporal data, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.392-403, April 02-04, 1990, Nashville, Tennessee, United States [doi>10.1145/298514.298590]
• 19: Nils Klarlund, Progress measures for complementation of &ohgr;-automata with applications to temporal logic, Proceedings of the 32nd annual symposium on Foundations of computer science, p.358-367, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185391]
• 20: Orna Kupferman , Moshe Vardi, Weak Alternating Automata Are Not That Weak, Proceedings of the Fifth Israel Symposium on the Theory of Computing Systems (ISTCS '97), p.147, June 17-19, 1997
• 21: Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000 [doi>10.1145/333979.333987]
• 22: Landweber, L. H. 1969. Decision problems for ω-automata. Math. Syst. Theor. 3, 4, 376--384.
• 23: Efficient minimization of deterministic weak &ohgr;-automata, Information Processing Letters, v.79 n.3, p.105-109, 07/31/2001 [doi>10.1016/S0020-0190(00)00183-6]
• 24: Oded Maler , Ludwig Staiger, On syntactic congruences for &ohgr;-languages, Theoretical Computer Science, v.183 n.1, p.93-112, Aug. 30, 1997 [doi>10.1016/S0304-3975(96)00312-X]
• 25: Miyano, S. and Hayashi, T. 1984. Alternating finite automata on ω-words. Theoret. Comput. Sci. 32, 321--330.
• 26: D E Muller , A Saoudi , P E Schupp, Alternating automata, the weak monadic theory of the tree, and its complexity, International Colloquium on Automata, Languages and Programming on Automata, languages and programming, p.275-283, September 1986, Rennes, France
• 27: Rabin, M. O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1--35.
• 28: Safra, S. 1988. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 319--327.
• 29: Semenov, A. L. 1977. Presburgerness of predicates regular in two number systems. Siberian Math. J. 18, 289--299.
• 30: Thomas R. Shiple , James H. Kukula , Rajeev K. Ranjan, A Comparison of Presburger Engines for EFSM Reachability, Proceedings of the 10th International Conference on Computer Aided Verification, p.280-292, June 28-July 02, 1998
• 31: A. Prasad Sistla , M. Y. Vardi , P. Wolper, The complementation problem for Bu¨chi automata with applications to temporal logic, Theoretical Computer Science, v.49 n.2-3, p.217-237, January 1987 [doi>10.1016/0304-3975(87)90008-9]
• 32: Staiger, L. 1983. Finite-state ω-languages. J. Comput. Syst. Sci. 27, 3, 434--448.
• 33: Staiger, L. and Wagner, K. 1974. Automaten theoretische und automatenfreie charakterisierungen topologischer klassen regulärer folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK 10, 379--392.
• 34: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 35: Vardi, M. Y. and Wolper, P. 1986a. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 322--331.
• 36: Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
• 37: Moshe Y. Vardi , Pierre Wolper, Reasoning about infinite computations, Information and Computation, v.115 n.1, p.1-37, Nov. 15, 1994 [doi>10.1006/inco.1994.1092]
• 38: Wagner, K. 1979. On ω-regular sets. Inform. Contr. 43, 2 (Nov.), 123--177.
• 39: Volker Weispfenning, Mixed real-integre linear quantifier elimination, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.129-136, July 28-31, 1999, Vancouver, British Columbia, Canada [doi>10.1145/309831.309888]
• 40: Pierre Wolper , Bernard Boigelot, An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract), Proceedings of the Second International Symposium on Static Analysis, p.21-32, September 25-27, 1995
• 41: Pierre Wolper , Bernard Boigelot, On the Construction of Automata from Linear Arithmetic Constraints, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.1-19, March 25-April 02, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Algorithms, Theory

Keywords:
Decision procedure, finite-state representations, integer and real arithmetic, weak ω-automata