Set Constraints with Intersection

Charatonik, Witold; Podelski, Andreas

Local TagsRelease HistoryDetailsSummary

Set Constraints with Intersection

Charatonik, W., & Podelski, A. (2002). Set Constraints with Intersection. Information and Computation, 179, 213-229.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3070-7 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3071-5

Genre: Journal Article

Files

show Files

Locators

show

Creators

show

hide

Creators:
Charatonik, Witold¹, Author
Podelski, Andreas¹, Author

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

Abstract: Set constraints are inclusions between expressions denoting sets of trees (over a given alphabet of constructor symbols). The efficiency of their satisfiability test is a central issue in set-based program analysis, their main application domain. We introduce the class of {\em set constraints with intersection}\/ (the only operators forming the expressions are constructors and intersection) and show that its satisfiability problem is DEXPTIME-complete. This is the first class of set constraints (over a general constructor alphabet) that falls into this complexity class. The solved form in our algorithm represents the least solution as a tree automaton and exhibits which variables denote the empty set. We furthermore prove that set constraints with intersection are equivalent to {\em definite set constraints}\/ (in expressive power, and the satisfiability problems are linearly inter-reducible). The class of definite set constraints was the first one for which the decidability question was solved; we hereby settle also the complexity question.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2003-05-09Date issued: 2002

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: Peer

Identifiers: eDoc: 202134
Other: Local-ID: C1256104005ECAFC-079D7DD74FCAD6F6412566FD0057B689-CPintersectionJ

Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show

hide

Title: Information and Computation

Source Genre: Journal

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 179 Sequence Number: - Start / End Page: 213 - 229 Identifier: ISSN: 0890-5401