|
|||||
|
|
Tarskian Set Constraints |
|
| Authors: | Robert Givan David McAllester Carl Witty Dexter Kozen |
| Affiliation: | Department of Electrical & Computer Engineering, Purdue University, 1285 EE Building, West Lafayette, Indiana, 47907, f1, http://www.ece.purdue.edu/˜givan/;AT&T Labs Research, P.O. Box 971, 180 Park Avenue, Florham Park, New Jersey, 07932, , f2, http://www.research.att.com/˜dmac/;Newton Research Labs, 4140 Lind Avenue SW, Renton, Washington, 98055, , f3;Computer Science Department, Cornell University, Upson Hall, Ithaca, New York, 14853-7501, , f4, http://www.cs.cornell.edu/kozen/ |
| Abstract: | We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning of a Tarskian function symbol is interpreted in an arbitrary first order structure. We show that satisfiability of Tarskian set constraints is decidable in nondeterministic doubly exponential time. We also give complexity results and open problems for various extensions and restrictions of the language. |
| Keywords: | Abbreviations: set constraintsAbbreviations: decision proceduresAbbreviations: dynamic logicAbbreviations: mu-calculus |
| 本文献已被 ScienceDirect 等数据库收录！ | |