Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the Complexity of Pointer Arithmetic in Separation Logic (an extended version)
95
0
0.0
(
0
)
Added by
Max Kanovich
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation logic with various forms of Presburger arithmetic constraints. Most significantly, we find that, even in the minimal case when we allow only conjunctions of simple difference constraints (xleq x+k) where k is an integer, polynomial-time decidability is already impossible: satisfiability becomes NP-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes P2-complete (P2 is the second class in the polynomial-time hierarchy) In fact we prove that the upper bound is the same, P2, even for the full pointer arithmetic but with a fixed pointer offset, where we allow any Boolean combinations of the elementary formulas (x=x+k0), (xleq x+k0), and (x<x+k0), and, in addition to the points-to formulas, we allow spatial formulas of the arrays the length of which is bounded by k0 and lists which length is bounded by k0, etc, where k0 is a fixed integer. However, if we allow a significantly more expressive form of pointer arithmetic - namely arbitrary Boolean combinations of elementary formulas over arbitrary pointer sums - then the complexity increase is relatively modest for satisfiability and quantifier-free entailment: they are still NP-complete and coNP-complete respectively, and the complexity appears to increase drastically for quantified entailments.
rate research
Read More
We present a ke-based procedure for the main TBox and ABox reasoning tasks for the description logic $dlssx$, in short $shdlssx$. The logic $shdlssx$, representable in the decidable multi-sorted quantified set-theoretic fragment $flqsr$, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics. %In fact it supports, among other features, Boolean operations on concepts and roles, role constructs such as the product of concepts and role chains on the left hand side of inclusion axioms, and role properties such as transitivity, symmetry, reflexivity, and irreflexivity. Our algorithm is based on a variant of the kespace system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the $gamma$-rule. The novel system, called keg, turns out to be an improvement of the system introduced in cite{RR2017} and of standard first-order ke x cite{dagostino94}. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the keg-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set-theory.
We present a ke-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $dlssx$ ($shdlssx$, for short). Our application solves the main TBox and ABox reasoning problems for $shdlssx$. In particular, it solves the consistency problem for $shdlssx$-knowledge bases represented in set-theoretic terms, and a generalization of the emph{Conjunctive Query Answering} problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and optimizes a previous prototype for the consistency checking of $shdlssx$-knowledge bases (see cite{cilc17}), is implemented in textsf{C++}. It supports $shdlssx$-knowledge bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).
We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be constructive in some sense, whereas proofs of classical propositions proceed by contradiction. The system, in natural deduction style, is shown to be sound and complete with respect to a Kripke semantics. We develop the system from the perspective of the propositions-as-types correspondence by deriving a term assignment system with confluent reduction. The proof of strong normalization relies on a translation to System F with Mendler-style recursion.
We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpretations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probability theory and, most importantly, of representing every recursive random function. Moreover, we introduce a realizability interpretation of this logic in which programs have access to an oracle from the Cantor space.
Description logics are knowledge representation languages that have been designed to strike a balance between expressivity and computational tractability. Many different description logics have been developed, and numerous computational problems for these logics have been studied for their computational complexity. However, essentially all complexity analyses of reasoning problems for description logics use the one-dimensional framework of classical complexity theory. The multi-dimensional framework of parameterized complexity theory is able to provide a much more detailed image of the complexity of reasoning problems. In this paper we argue that the framework of parameterized complexity has a lot to offer for the complexity analysis of description logic reasoning problems---when one takes a progressive and forward-looking view on parameterized complexity tools. We substantiate our argument by means of three case studies. The first case study is about the problem of concept satisfiability for the logic ALC with respect to nearly acyclic TBoxes. The second case study concerns concept satisfiability for ALC concepts parameterized by the number of occurrences of union operators and the number of occurrences of full existential quantification. The third case study offers a critical look at data complexity results from a parameterized complexity point of view. These three case studies are representative for the wide range of uses for parameterized complexity methods for description logic problems.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
