Matching Items (26)
Description
Answer Set Programming (ASP) is one of the most prominent and successful knowledge representation paradigms. The success of ASP is due to its expressive non-monotonic modeling language and its efficient computational methods originating from building propositional satisfiability solvers. The wide adoption of ASP has motivated several extensions to its modeling language in order to enhance expressivity, such as incorporating aggregates and interfaces with ontologies. Also, in order to overcome the grounding bottleneck of computation in ASP, there are increasing interests in integrating ASP with other computing paradigms, such as Constraint Programming (CP) and Satisfiability Modulo Theories (SMT). Due to the non-monotonic nature of the ASP semantics, such enhancements turned out to be non-trivial and the existing extensions are not fully satisfactory. We observe that one main reason for the difficulties rooted in the propositional semantics of ASP, which is limited in handling first-order constructs (such as aggregates and ontologies) and functions (such as constraint variables in CP and SMT) in natural ways. This dissertation presents a unifying view on these extensions by viewing them as instances of formulas with generalized quantifiers and intensional functions. We extend the first-order stable model semantics by by Ferraris, Lee, and Lifschitz to allow generalized quantifiers, which cover aggregate, DL-atoms, constraints and SMT theory atoms as special cases. Using this unifying framework, we study and relate different extensions of ASP. We also present a tight integration of ASP with SMT, based on which we enhance action language C+ to handle reasoning about continuous changes. Our framework yields a systematic approach to study and extend non-monotonic languages.
ContributorsMeng, Yunsong (Author) / Lee, Joohyung (Thesis advisor) / Ahn, Gail-Joon (Committee member) / Baral, Chitta (Committee member) / Fainekos, Georgios (Committee member) / Lifschitz, Vladimir (Committee member) / Arizona State University (Publisher)
Created2013
Description
A central concept of combinatorics is partitioning structures with given constraints. Partitions of on-line posets and on-line graphs, which are dynamic versions of the more familiar static structures posets and graphs, are examined. In the on-line setting, vertices are continually added to a poset or graph while a chain partition or coloring (respectively) is maintained. %The optima of the static cases cannot be achieved in the on-line setting. Both upper and lower bounds for the optimum of the number of chains needed to partition a width $w$ on-line poset exist. Kierstead's upper bound of $\frac{5^w-1}{4}$ was improved to $w^{14 \lg w}$ by Bosek and Krawczyk. This is improved to $w^{3+6.5 \lg w}$ by employing the First-Fit algorithm on a family of restricted posets (expanding on the work of Bosek and Krawczyk) . Namely, the family of ladder-free posets where the $m$-ladder is the transitive closure of the union of two incomparable chains $x_1\le\dots\le x_m$, $y_1\le\dots\le y_m$ and the set of comparabilities $\{x_1\le y_1,\dots, x_m\le y_m\}$. No upper bound on the number of colors needed to color a general on-line graph exists. To lay this fact plain, the performance of on-line coloring of trees is shown to be particularly problematic. There are trees that require $n$ colors to color on-line for any positive integer $n$. Furthermore, there are trees that usually require many colors to color on-line even if they are presented without any particular strategy. For restricted families of graphs, upper and lower bounds for the optimum number of colors needed to maintain an on-line coloring exist. In particular, circular arc graphs can be colored on-line using less than 8 times the optimum number from the static case. This follows from the work of Pemmaraju, Raman, and Varadarajan in on-line coloring of interval graphs.
ContributorsSmith, Matthew Earl (Author) / Kierstead, Henry A (Thesis advisor) / Colbourn, Charles (Committee member) / Czygrinow, Andrzej (Committee member) / Fishel, Susanna (Committee member) / Hurlbert, Glenn (Committee member) / Arizona State University (Publisher)
Created2012
Description
This research describes software based remote attestation schemes for obtaining the integrity of an executing user application and the Operating System (OS) text section of an untrusted client platform. A trusted external entity issues a challenge to the client platform. The challenge is executable code which the client must execute, and the code generates results which are sent to the external entity. These results provide the external entity an assurance as to whether the client application and the OS are in pristine condition. This work also presents a technique where it can be verified that the application which was attested, did not get replaced by a different application after completion of the attestation. The implementation of these three techniques was achieved entirely in software and is backward compatible with legacy machines on the Intel x86 architecture. This research also presents two approaches to incorporating software based "root of trust" using Virtual Machine Monitors (VMMs). The first approach determines the integrity of an executing Guest OS from the Host OS using Linux Kernel-based Virtual Machine (KVM) and qemu emulation software. The second approach implements a small VMM called MIvmm that can be utilized as a trusted codebase to build security applications such as those implemented in this research. MIvmm was conceptualized and implemented without using any existing codebase; its minimal size allows it to be trustworthy. Both the VMM approaches leverage processor support for virtualization in the Intel x86 architecture.
ContributorsSrinivasan, Raghunathan (Author) / Dasgupta, Partha (Thesis advisor) / Colbourn, Charles (Committee member) / Shrivastava, Aviral (Committee member) / Huang, Dijiang (Committee member) / Dewan, Prashant (Committee member) / Arizona State University (Publisher)
Created2011
Description
Finding the optimal solution to a problem with an enormous search space can be challenging. Unless a combinatorial construction technique is found that also guarantees the optimality of the resulting solution, this could be an infeasible task. If such a technique is unavailable, different heuristic methods are generally used to improve the upper bound on the size of the optimal solution. This dissertation presents an alternative method which can be used to improve a solution to a problem rather than construct a solution from scratch. Necessity analysis, which is the key to this approach, is the process of analyzing the necessity of each element in a solution. The post-optimization algorithm presented here utilizes the result of the necessity analysis to improve the quality of the solution by eliminating unnecessary objects from the solution. While this technique could potentially be applied to different domains, this dissertation focuses on k-restriction problems, where a solution to the problem can be presented as an array. A scalable post-optimization algorithm for covering arrays is described, which starts from a valid solution and performs necessity analysis to iteratively improve the quality of the solution. It is shown that not only can this technique improve upon the previously best known results, it can also be added as a refinement step to any construction technique and in most cases further improvements are expected. The post-optimization algorithm is then modified to accommodate every k-restriction problem; and this generic algorithm can be used as a starting point to create a reasonable sized solution for any such problem. This generic algorithm is then further refined for hash family problems, by adding a conflict graph analysis to the necessity analysis phase. By recoloring the conflict graphs a new degree of flexibility is explored, which can further improve the quality of the solution.
ContributorsNayeri, Peyman (Author) / Colbourn, Charles (Thesis advisor) / Konjevod, Goran (Thesis advisor) / Sen, Arunabha (Committee member) / Stanzione Jr, Daniel (Committee member) / Arizona State University (Publisher)
Created2011
Description
Different logic-based knowledge representation formalisms have different limitations either with respect to expressivity or with respect to computational efficiency. First-order logic, which is the basis of Description Logics (DLs), is not suitable for defeasible reasoning due to its monotonic nature. The nonmonotonic formalisms that extend first-order logic, such as circumscription and default logic, are expressive but lack efficient implementations. The nonmonotonic formalisms that are based on the declarative logic programming approach, such as Answer Set Programming (ASP), have efficient implementations but are not expressive enough for representing and reasoning with open domains. This dissertation uses the first-order stable model semantics, which extends both first-order logic and ASP, to relate circumscription to ASP, and to integrate DLs and ASP, thereby partially overcoming the limitations of the formalisms. By exploiting the relationship between circumscription and ASP, well-known action formalisms, such as the situation calculus, the event calculus, and Temporal Action Logics, are reformulated in ASP. The advantages of these reformulations are shown with respect to the generality of the reasoning tasks that can be handled and with respect to the computational efficiency. The integration of DLs and ASP presented in this dissertation provides a framework for integrating rules and ontologies for the semantic web. This framework enables us to perform nonmonotonic reasoning with DL knowledge bases. Observing the need to integrate action theories and ontologies, the above results are used to reformulate the problem of integrating action theories and ontologies as a problem of integrating rules and ontologies, thus enabling us to use the computational tools developed in the context of the latter for the former.
ContributorsPalla, Ravi (Author) / Lee, Joohyung (Thesis advisor) / Baral, Chitta (Committee member) / Kambhampati, Subbarao (Committee member) / Lifschitz, Vladimir (Committee member) / Arizona State University (Publisher)
Created2012
Description
Thanks to continuous technology scaling, intelligent, fast and smaller digital systems are now available at affordable costs. As a result, digital systems have found use in a wide range of application areas that were not even imagined before, including medical (e.g., MRI, remote or post-operative monitoring devices, etc.), automotive (e.g., adaptive cruise control, anti-lock brakes, etc.), security systems (e.g., residential security gateways, surveillance devices, etc.), and in- and out-of-body sensing (e.g., capsule swallowed by patients measuring digestive system pH, heart monitors, etc.). Such computing systems, which are completely embedded within the application, are called embedded systems, as opposed to general purpose computing systems. In the design of such embedded systems, power consumption and reliability are indispensable system requirements. In battery operated portable devices, the battery is the single largest factor contributing to device cost, weight, recharging time, frequency and ultimately its usability. For example, in the Apple iPhone 4 smart-phone, the battery is $40\%$ of the device weight, occupies $36\%$ of its volume and allows only $7$ hours (over 3G) of talk time. As embedded systems find use in a range of sensitive applications, from bio-medical applications to safety and security systems, the reliability of the computations performed becomes a crucial factor. At our current technology-node, portable embedded systems are prone to expect failures due to soft errors at the rate of once-per-year; but with aggressive technology scaling, the rate is predicted to increase exponentially to once-per-hour. Over the years, researchers have been successful in developing techniques, implemented at different layers of the design-spectrum, to improve system power efficiency and reliability. Among the layers of design abstraction, I observe that the interface between the compiler and processor micro-architecture possesses a unique potential for efficient design optimizations. A compiler designer is able to observe and analyze the application software at a finer granularity; while the processor architect analyzes the system output (power, performance, etc.) for each executed instruction. At the compiler micro-architecture interface, if the system knowledge at the two design layers can be integrated, design optimizations at the two layers can be modified to efficiently utilize available resources and thereby achieve appreciable system-level benefits. To this effect, the thesis statement is that, ``by merging system design information at the compiler and micro-architecture design layers, smart compilers can be developed, that achieve reliable and power-efficient embedded computing through: i) Pure compiler techniques, ii) Hybrid compiler micro-architecture techniques, and iii) Compiler-aware architectures''. In this dissertation demonstrates, through contributions in each of the three compiler-based techniques, the effectiveness of smart compilers in achieving power-efficiency and reliability in embedded systems.
ContributorsJeyapaul, Reiley (Author) / Shrivastava, Aviral (Thesis advisor) / Vrudhula, Sarma (Committee member) / Clark, Lawrence (Committee member) / Colbourn, Charles (Committee member) / Arizona State University (Publisher)
Created2012
Description
Gray codes are perhaps the best known structures for listing sequences of combinatorial objects, such as binary strings. Simply defined as a minimal change listing, Gray codes vary greatly both in structure and in the types of objects that they list. More specific types of Gray codes are universal cycles and overlap sequences. Universal cycles are Gray codes on a set of strings of length n in which the first n-1 letters of one object are the same as the last n-1 letters of its predecessor in the listing. Overlap sequences allow this overlap to vary between 1 and n-1. Some of our main contributions to the areas of Gray codes and universal cycles include a new Gray code algorithm for fixed weight m-ary words, and results on the existence of universal cycles for weak orders on [n]. Overlap cycles are a relatively new structure with very few published results. We prove the existence of s-overlap cycles for k-permutations of [n], which has been an open research problem for several years, as well as constructing 1- overlap cycles for Steiner triple and quadruple systems of every order. Also included are various other results of a similar nature covering other structures such as binary strings, m-ary strings, subsets, permutations, weak orders, partitions, and designs. These listing structures lend themselves readily to some classes of combinatorial objects, such as binary n-tuples and m-ary n-tuples. Others require more work to find an appropriate structure, such as k-subsets of an n-set, weak orders, and designs. Still more require a modification in the representation of the objects to fit these structures, such as partitions. Determining when and how we can fit these sets of objects into our three listing structures is the focus of this dissertation.
ContributorsHoran, Victoria E (Author) / Hurlbert, Glenn H. (Thesis advisor) / Czygrinow, Andrzej (Committee member) / Fishel, Susanna (Committee member) / Colbourn, Charles (Committee member) / Sen, Arunabha (Committee member) / Arizona State University (Publisher)
Created2012
Description
Medium access control (MAC) is a fundamental problem in wireless networks.
In ad-hoc wireless networks especially, many of the performance and scaling issues
these networks face can be attributed to their use of the core IEEE 802.11 MAC
protocol: distributed coordination function (DCF). Smoothed Airtime Linear Tuning
(SALT) is a new contention window tuning algorithm proposed to address some of the
deficiencies of DCF in 802.11 ad-hoc networks. SALT works alongside a new user level
and optimized implementation of REACT, a distributed resource allocation protocol,
to ensure that each node secures the amount of airtime allocated to it by REACT.
The algorithm accomplishes that by tuning the contention window size parameter
that is part of the 802.11 backoff process. SALT converges more tightly on airtime
allocations than a contention window tuning algorithm from previous work and this
increases fairness in transmission opportunities and reduces jitter more than either
802.11 DCF or the other tuning algorithm. REACT and SALT were also extended
to the multi-hop flow scenario with the introduction of a new airtime reservation
algorithm. With a reservation in place multi-hop TCP throughput actually increased
when running SALT and REACT as compared to 802.11 DCF, and the combination of
protocols still managed to maintain its fairness and jitter advantages. All experiments
were performed on a wireless testbed, not in simulation.
In ad-hoc wireless networks especially, many of the performance and scaling issues
these networks face can be attributed to their use of the core IEEE 802.11 MAC
protocol: distributed coordination function (DCF). Smoothed Airtime Linear Tuning
(SALT) is a new contention window tuning algorithm proposed to address some of the
deficiencies of DCF in 802.11 ad-hoc networks. SALT works alongside a new user level
and optimized implementation of REACT, a distributed resource allocation protocol,
to ensure that each node secures the amount of airtime allocated to it by REACT.
The algorithm accomplishes that by tuning the contention window size parameter
that is part of the 802.11 backoff process. SALT converges more tightly on airtime
allocations than a contention window tuning algorithm from previous work and this
increases fairness in transmission opportunities and reduces jitter more than either
802.11 DCF or the other tuning algorithm. REACT and SALT were also extended
to the multi-hop flow scenario with the introduction of a new airtime reservation
algorithm. With a reservation in place multi-hop TCP throughput actually increased
when running SALT and REACT as compared to 802.11 DCF, and the combination of
protocols still managed to maintain its fairness and jitter advantages. All experiments
were performed on a wireless testbed, not in simulation.
ContributorsMellott, Matthew (Author) / Syrotiuk, Violet (Thesis advisor) / Colbourn, Charles (Committee member) / Tinnirello, Ilenia (Committee member) / Arizona State University (Publisher)
Created2018
Description
Since the seminal work of Tur ́an, the forbidden subgraph problem has been among the central questions in extremal graph theory. Let ex(n;F) be the smallest number m such that any graph on n vertices with m edges contains F as a subgraph. Then the forbidden subgraph problem asks to find ex(n; F ) for various graphs F . The question can be further generalized by asking for the extreme values of other graph parameters like minimum degree, maximum degree, or connectivity. We call this type of question a Tura ́n-type problem. In this thesis, we will study Tura ́n-type problems and their variants for graphs and hypergraphs.
Chapter 2 contains a Tura ́n-type problem for cycles in dense graphs. The main result in this chapter gives a tight bound for the minimum degree of a graph which guarantees existence of disjoint cycles in the case of dense graphs. This, in particular, answers in the affirmative a question of Faudree, Gould, Jacobson and Magnant in the case of dense graphs.
In Chapter 3, similar problems for trees are investigated. Recently, Faudree, Gould, Jacobson and West studied the minimum degree conditions for the existence of certain spanning caterpillars. They proved certain bounds that guarantee existence of spanning caterpillars. The main result in Chapter 3 significantly improves their result and answers one of their questions by proving a tight minimum degree bound for the existence of such structures.
Chapter 4 includes another Tur ́an-type problem for loose paths of length three in a 3-graph. As a corollary, an upper bound for the multi-color Ramsey number for the loose path of length three in a 3-graph is achieved.
Chapter 2 contains a Tura ́n-type problem for cycles in dense graphs. The main result in this chapter gives a tight bound for the minimum degree of a graph which guarantees existence of disjoint cycles in the case of dense graphs. This, in particular, answers in the affirmative a question of Faudree, Gould, Jacobson and Magnant in the case of dense graphs.
In Chapter 3, similar problems for trees are investigated. Recently, Faudree, Gould, Jacobson and West studied the minimum degree conditions for the existence of certain spanning caterpillars. They proved certain bounds that guarantee existence of spanning caterpillars. The main result in Chapter 3 significantly improves their result and answers one of their questions by proving a tight minimum degree bound for the existence of such structures.
Chapter 4 includes another Tur ́an-type problem for loose paths of length three in a 3-graph. As a corollary, an upper bound for the multi-color Ramsey number for the loose path of length three in a 3-graph is achieved.
ContributorsYie, Jangwon (Author) / Czygrinow, Andrzej (Thesis advisor) / Kierstead, Henry (Committee member) / Colbourn, Charles (Committee member) / Fishel, Susanna (Committee member) / Spielberg, John (Committee member) / Arizona State University (Publisher)
Created2018
Description
As an example of "big data," we consider a repository of Arctic sea ice concentration data collected from satellites over the years 1979-2005. The data is represented by a graph, where vertices correspond to measurement points, and an edge is inserted between two vertices if the Pearson correlation coefficient between them exceeds a threshold. We investigate new questions about the structure of the graph related to betweenness, closeness centrality, vertex degrees, and characteristic path length. We also investigate whether an offset of weeks and years in graph generation results in a cosine similarity value that differs significantly from expected values. Finally, we relate the computational results to trends in Arctic ice.
ContributorsDougherty, Ryan Edward (Author) / Syrotiuk, Violet (Thesis director) / Colbourn, Charles (Committee member) / Barrett, The Honors College (Contributor) / School of Mathematical and Statistical Sciences (Contributor) / Computer Science and Engineering Program (Contributor)
Created2015-05