Solving classes of set constraints with tree automata
Set constraints is a suitable formalism for static analysis of programs. However, it is known that the complexity of set constraint problems in the most general cases is very high (NEXPTIME-completeness of the satisfiability test). Lots of works are involved in finding more tractable subclasses.
In this paper, we investigate two classes of set constraints shown to be useful for program analysis: the first one is an extension of definite set constraints including the main feature of quantified set expressions. We will show that the satisfiability problem for this class is EXPTIME-complete.
The second one concerns constraints of the form Xexp, where exp is built with function symbols, the intersection and union connectives and projection operators.
The dual aspects of those two classes allows to find a common approach for solving both of them. This approach uses as basic tool tree automata, which axe suitable both for computation and representing the solution of those solving problems. It leads also to simple algorithms and an easy characterization of complexity.
KeywordsInference Rule Function Symbol Transition Rule Reachable State Great Solution
Unable to display preview. Download preview PDF.
- [AM91]A. Aiken and B. Murphy. Implementing Regular Trees. In Proceedings of the 5 th ACM Conference on Functional Programming and Computer Architecture, LNCS 523, pages 427–447, aug 1991.Google Scholar
- [AW92]A. Aiken and E.L. Wimmers. Solving Systems of Set Constraints. In Proceedings of the 7 th IEEE Symposium on Logic in Computer Science, pages 329–340, 1992.Google Scholar
- [BGW92]L. Bachmair, H. Ganzinger, and U. Waldmann. Set Constraints are the Monadic Class. Technical Report MPI-I-92-240, Max-Planck-Institut für Informatik, dec 1992.Google Scholar
- [CP94]W. Charatonik and L. Pacholski. Set Constraints with Projections are in NEXPTIME. In Proceedings of the 35 th Symposium on Foundations of Computer Science, pages 642–653, 1994.Google Scholar
- [CP97a]W. Charatonik and A. Podelski. Set Constraints with Intersection. In Proceedings of the 12 th IEEE Symposium on Logic in Computer Science, 1997.Google Scholar
- [CP97b]W. Charatonik and A. Podelski. Solving Set Constraints for Greatest Models. Technical Report MPI-I-2-004, Max-Planck-Institut für Informatik, 1997.Google Scholar
- [GS84]F. Gécseg and M. Steinby. Tree Automata. Akadémiai Kiadó, Budapest, 1984.Google Scholar
- [GTT93]R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. In Proceedings of the 34 th Symp. on Foundations of Computer Science, pages 372–380, 1993.Google Scholar
- [Hei92a]N. Heintze. Practical Aspects of Set Based Analysis. In Proceedings of the Joint International Conference and Symposium on Logic Programming. MIT-Press, nov 1992.Google Scholar
- [Hei92b]N. Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, sep 1992.Google Scholar
- [Hei94]N. Heintze. Set-based Analysis of ML Programs. In Lisp and Functional Programming, pages 306–317. ACM, 1994.Google Scholar
- [MN97]M. Müller and J. Niehren. Entailment of Set Constraints is not Feasible. Technical report, Universität des Saarlandes, Programming Systems Lab, 1997. Available at http://www.ps.uni-sb.de/ mmueller/papers/conp.ps.Z.Google Scholar
- [MNP97]M. Müller, J. Niehren, and A. Podelski. Inclusion Constraints over Non-Empty Sets of Trees. In Proceedings of 7 th International Joint Conference CAAP/FASE — (TAPSOFT'97), LNCS 1214, pages 345–356, apr 1997.Google Scholar
- [Ste94]K. Stefansson. Systems of Set Constraints with Negative Constraints are NEXPTIME-Complete. In Proceedings of the 9 th IEEE Symposium on Logic in Computer Science, 1994.Google Scholar
- [Tom94]M. Tommasi. Automates et Contraintes Ensemblistes. PhD thesis, Université des Sciences et Technologies de Lille, 1994.Google Scholar