No description available.

No description available.

No description available.

Artificial neural networks (ANN) have found extensive use in solving real-world problems in recent years, where their exceptional information processing is the main advantage. Facing increasingly complex problems, there is a need to improve their information processing. In this thesis, we explore new ways of synthesizing ANNs by reducing the synthesis problem to the Boolean satisfiability problem (SAT) that is, the problem of determining whether a given Boolean formula is satisfiable. Also known as the SAT problem, it aims to determine if there exists such a combination of Boolean variables in a propositional formula for which the formula evaluates to true. We derived a general formula in conjunctive normal form (CNF) representing the synthesis of a neural network. Given randomly generated datasets, we were able to construct CNF formulas whose satisfying assignments encode neural networks consistent with the datasets. These formulas were run through an off-the-shelf SAT solver, where the outputted models simulated the synthesis of neural networks consistent with the datasets. The experiments conducted in this thesis showed that our method had the ability to produce feed-forward neural networks of varying sizes consistent with randomly generated datasets of binary strings.

Automated trust negotiation is the process of establishing trust between entities with no prior relationship through the iterative disclosure of digital credentials. One approach to negotiating trust is for the participants to exchange access control policies to inform each other of the requirements for establishing trust. When a policy is received at runtime, a compliance checker determines which credentials satisfy the policy so they can be disclosed. In situations where several sets of credentials satisfy a policy and some of the credentials are sensitive, a compliance checker that generates all the sets is necessary to insure that the negotiation succeeds whenever possible. Compliance checkers designed for trust management do not usually generate all the satisfying sets. In this thesis, we present two practical algorithms for generating all satisfying sets given a compliance checker that generates only one set. The ability to generate all of the combinations provides greater flexibility in how the system or user establishes trust. For example, the least sensitive credential combination could be disclosed first. These ideas have been implemented in TrustBuilder, our prototype system for trust negotiation.

Expressiveness, and more recently, succinctness, are two central concerns of finite model theory and descriptive complexity theory. Succinctness is particularly interesting because it is closely related to the complexity-theoretic trade-off between parallel time and the amount of hardware. We develop new bounds on the expressiveness and succinctness of first-order logic with two variables on finite words, present a related result about the complexity of the satisfiability problem for this logic, and explore a new approach to the generalized star-height problem from the perspective of logical expressiveness. We give a complete characterization of the expressive power of first-order logic with two variables on finite words. Our main tool for this investigation is the classical Ehrenfeucht-Fra¨ıss´e game. Using our new characterization, we prove that the quantifier alternation hierarchy for this logic is strict, settling the main remaining open question about the expressiveness of this logic. A second important question about first-order logic with two variables on finite words is about the complexity of the satisfiability problem for this logic. Previously it was only known that this problem is NP-hard and in NEXP. We prove a polynomialsize small-model property for this logic, leading to an NP algorithm and thus proving that the satisfiability problem for this logic is NP-complete. Finally, we investigate one of the most baffling open problems in formal language theory: the generalized star-height problem. As of today, we do not even know whether there exists a regular language that has generalized star-height larger than 1. This problem can be phrased as an expressiveness question for first-order logic with a restricted transitive closure operator, and thus allows us to use established tools from finite model theory to attack the generalized star-height problem. Besides our contribution to formalize this problem in a purely logical form, we have developed several example languages as candidates for languages of generalized star-height at least 2. While some of them still stand as promising candidates, for others we present new results that prove that they only have generalized star-height 1.

No description available.

Because of the importance of undecidability and the concern with the high complexity of automated reasoning, a few interval-based temporal description logics (ITDLs) have been designed. Moreover, most existing ITDLs are not able to specify the lengths of intervals. In other words, they are not metric. On the other hand, some domains (e.g., medicine) are inherently interval-based, and require a metric logic in order to formalize defined processes and to check process consistency. Hence, a metric interval-based temporal description logic is required. In this thesis, we introduce such a logic (MITDL) along with two algorithms for the satisfiability checking of its formulas. We first introduce an interval-based temporal logic, called IMPNL, inspired by Metric Propositional Neighbourhood Logic. We also present a sound, com- plete and terminating tableau-based algorithm for checking the satisfiability of IMPNL formulas. Afterwards, we combine a restricted version of IMPNL (IMPNL without a negation operator) with the ALC description logic to form a MITDL. We propose two tableau-based algorithms for checking the satisfia- bility of MITDL formulas. We show and prove they are sound, complete and terminate. These algorithms have PSpace and 2NExp-Time complexities. As a proof of concept, we use IMPNL and MITDL to model some clinical practice guidelines (CPG) and check their consistency. We compare MITDL with several languages commonly used for modeling CPGs. / Thesis / Doctor of Science (PhD)

No description available.

As complementary metal-oxide semiconductor (CMOS) technology faces more and more severe physical barriers down the path of continuously feature size scaling, innovative nano-scale devices and other post-CMOS technologies have been developed to enhance future circuit design and computation. These nanotechnologies have shown promising potentials to achieve magnitude improvement in performance and integration density. The substitution of CMOS transistors with nano-devices is expected to not only continue along the exponential projection of Moore's Law, but also raise significant challenges and opportunities, especially in the field of electronic design automation. The major obstacles that the designers are experiencing with emerging nanotechnology design include: i) the existing computer-aided design (CAD) approaches in the context of conventional CMOS Boolean design cannot be directly employed in the nanoelectronic design process, because the intrinsic electrical characteristics of many nano-devices are not best suited for Boolean implementations but demonstrate strong capability for implementing non-conventional logic such as threshold logic and reversible logic; ii) due to the density and size factors of nano-devices, the defect rate of nanoelectronic system is much higher than conventional CMOS systems, therefore existing design paradigms cannot guarantee design quality and lead to even worse result in high failure ratio. Motivated by the compelling potentials and design challenges of emerging post-CMOS technologies, this dissertation work focuses on fundamental design methodologies to effectively and efficiently achieve high quality nanoscale design. A novel programmable logic element (PLE) is first proposed to explore the versatile functionalities of threshold gates (TGs) and multi-threshold threshold gates (MTTGs). This PLE structure can realize all three- or four-variable logic functions through configuring binary control bits. This is the first single threshold logic structure that provides complete Boolean logic implementation. Based on the PLEs, a reconfigurable architecture is constructed to offer dynamic reconfigurability with little or no reconfiguration overhead, due to the intrinsic self-latching property of nanopipelining. Our reconfiguration data generation algorithm can further reduce the reconfiguration cost. To fully take advantage of such threshold logic design using emerging nanotechnologies, we also developed a combinational equivalence checking (CEC) framework for threshold logic design. Based on the features of threshold logic gates and circuits, different techniques of formulating a given threshold logic in conjunctive normal form (CNF) are introduced to facilitate efficient SAT-based verification. Evaluated with mainstream benchmarks, our hybrid algorithm, which takes into account both input symmetry and input weight order of threshold gates, can efficiently generate CNF formulas in terms of both SAT solving time and CNF generating time. Then the reversible logic synthesis problem is considered as we focus on efficient synthesis heuristics which can provide high quality synthesis results within a reasonable computation time. We have developed a weighted directed graph model for function representation and complexity measurement. An atomic transformation is constructed to associate the function complexity variation with reversible gates. The efficiency of our heuristic lies in maximally decreasing the function complexity during synthesis steps as well as the capability to climb out of local optimums. Thereafter, swarm intelligence, one of the machine learning techniques is employed in the space searching for reversible logic synthesis, which achieves further performance improvement. To tackle the high defect-rate during the emerging nanotechnology manufacturing process, we have developed a novel defect-aware logic mapping framework for nanowire-based PLA architecture via Boolean satisfiability (SAT). The PLA defects of various types are formulated as covering and closure constraints. The defect-aware logic mapping is then solved efficiently by using available SAT solvers. This approach can generate valid logic mapping with a defect rate as high as 20%. The proposed method is universally suitable for various nanoscale PLAs, including AND/OR, NOR/NOR structures, etc. In summary, this work provides some initial attempts to address two major problems confronting future nanoelectronic system designs: the development of electronic design automation tools and the reliability issues. However, there are still a lot of challenging open questions remain in this emerging and promising area. We hope our work can lay down stepstones on nano-scale circuit design optimization through exploiting the distinctive characteristics of emerging nanotechnologies. / Ph. D.