Some people believe that IC densities are approaching the fundamental limits inherent to semiconductor technologies. One alternative to semiconductors is Quantum-dot Cellular Automata (QCA); QCA is a nanotechnology that offers the potential to build denser IC's that switch at higher frequencies and run on lower power. QCA's most basic building block, the QCA cell, is inherently binary; digital circuits are implemented by arranging these QCA cells in pre-defined configurations on a two dimensional plane. This paper proposes a logic formulation that describes arranging QCA cells on a two dimensional plane; it is presented as a set of rules that can be implemented with basic Boolean variables and operators. This Boolean formulation is general and can be applied to any given specification. In addition, an optimization constraint is defined so that the logic formulation will only validate the most efficient QCA cell arrangements. The correctness of the logic formulation has been empirically verified by testing it with a SAT solver. The effectiveness of the minimization constraint in conjunction with the logic formulation has been tested with a Pseudo-Boolean ILP solver.

Innovation has long been considered crucial for companies to gain a competitive edge in the global marketplace. Unfortunately, a solid understanding of the system of innovation does not exist. The literature lacks formal definitions and methodologies for the system of innovation. Many surrogates for innovation metrics have been posited in past research but none have solidified the overall concept of an innovation system or science. It has been speculated that innovation as a system is complex. Additionally, some researchers have suggested that this innovation system is adaptive. In these instances, of the literature, surrogates were again utilized in place of solid modeling and hypothesis that is benchmarked against real world case studies. Surrogates, such as patent citation, do serve a useful purpose to assist in the understanding of the historic nature of the innovation system but they fall short of defining the system completely. This paper seeks to aid in the solidification of a hypothesis of the system of innovation as a complex adaptive system. Initial consideration is directed towards the historic interactions that have taken place in the system of innovation. These interactions are viewed through the surrogate of patent citation as there is little other record of innovation. The novelty of this paper is that patent citations form not the core but rather a starting point for the definition of innovation as a complex adaptive system. Various models are built using techniques of cellular automata as well as agent-based modeling to assist in the understanding of the principles at work in the innovation system. These models present startling evidence that there exists an upper bound on the number of interactions any one invention should utilize in its course towards being deemed an innovation. Additionally, the models describe the benefits of partnership between innovating entities in a rapidly changing marketplace such as the current technological markets. This paper asserts specific conclusions, from the models, that assist in understanding that the system of innovation is truly a complex adaptive system. The models are further supported through real world examples.

Marroquin and Ramirez (1990) have recently discovered a class of discrete stochastic cellular automata with Gibbsian invariant measures that have a non-reversible dynamic behavior. Practical applications include more powerful algorithms than the Metropolis algorithm to compute MRF models. In this paper we describe a large class of stochastic dynamical systems that has a Gibbs asymptotic distribution but does not satisfy reversibility. We characterize sufficient properties of a sub-class of stochastic differential equations in terms of the associated Fokker-Planck equation for the existence of an asymptotic probability distribution in the system of coordinates which is given. Practical implications include VLSI analog circuits to compute coupled MRF models.

Within the context of the verification of infinite-state systems, 'Regular model checking' is the name of a family of techniques in which states are represented by words or trees, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the problem of computing the set of reachable states of a system can be reduced to the one of computing the iterative closure of the finite-state transducer representing its transition relation. This thesis provides several techniques to computing the transitive closure of a finite-state transducer. One of the motivations of the thesis is to show the feasibility and usefulness of this approach through a combination of the necessary theoretical developments, implementation, and experimentation. For systems whose states are encoded by words, the iteration technique proceeds by comparing a finite sequence of successive powers of the transducer, detecting an 'increment' that is added to move from one power to the next, and extrapolating the sequence by allowing arbitrary repetitions of this increment. For systems whose states are represented by trees, the iteration technique proceeds by computing the powers of the transducer and progressively collapsing their states according to an equivalence relation until a fixed point is reached. The proposed iteration techniques can just as well be exploited to compute the closure of a given set of states by repeated applications of the transducer, which has proven to be a very effective way of using the technique. Various examples have been handled completely within the automata-theoretic setting. Another applications of the techniques are the verification of linear temporal properties as well as the computation of the convex hull of a finite set of integer vectors.

La thèse se situe à la charnière de l'informatique théorique et de la logique mathématique. Elle se concentre en particulier sur les aspects mathématiques de la vérification et du contrôle. La thèse se focalise sur l'étude de deux sous-classes d'automates hybrides: les automates temporisés pondérés et les automates hybrides o-minimaux. Concernant les automates temporisés pondérés, en introduisant un nouvel algorithme, nous donnons une caractérisation exacte de la complexité du problème d'atteignabilité optimal en prouvant qu'il est PSpace-complet. Nous prouvons que le model-checking de la logique WCTL est en général indécidable. Nous nous intéressons alors à une restriction de la logique WCTL. Nous montrons que la décidabilité du model-checking de WCTL restreint dépend de la dimension de l'automate et du fait que le temps soit discret ou dense. Finalement pour, nous prouvons que le problème de contrôle optimal est en général indécidable. Nous prouvons cependant que ce même problème est décidable pour les automates temporisés pondérés de dimension 1. En ce qui concerne les automates hybrides o-minimaux, à l'aide d'un encodage symbolique des trajectoires par des mots, nous sommes parvenus à prouver l'existence d'une bisimulation finie pour ces automates. De plus (toujours en utilisant nos encodages des trajectoires par des mots), nous avons obtenu des résultats de décidabilité pour des problèmes de jeux sur ces mêmes automates hybrides o-minimaux. Pour une classe d'automates hybrides o-minimaux, nous avons prouvé (i) que l'existence de stratégie gagnante pouvait être décidée et (ii) que ces stratégies gagnantes pouvaient être synthétisées.

We give a necessary and sufficient condition for the existence of an increasing coupling of N (N >= 2) synchronous dynamics on S-Zd (PCA). Increasing means the coupling preserves stochastic ordering. We first present our main construction theorem in the case where S is totally ordered; applications to attractive PCAs are given. When S is only partially ordered, we show on two examples that a coupling of more than two synchronous dynamics may not exist. We also prove an extension of our main result for a particular class of partially ordered spaces.

Rule-based systems implemented as event-condition-action (ECA) rules utilize a powerful and flexible paradigm when it comes to specifying systems that need to react to complex situation in their environment. Rules can be specified to react to combinations of events occurring at any time in any order. However, the behavior of a rule based system is notoriously hard to analyze due to the rules ability to interact with each other. Formal methods are not utilized in their full potential for enhancing software quality in practice. We argue that seamless support in a high-level paradigm specific tool is a viable way to provide industrial system designers with powerful verification techniques. This thesis targets the issue of formally verifying that a set of specified rules behaves as indented. The prototype tool REX (Rule and Event eXplorer) is developed as a proof of concept of the results of this thesis. Rules and events are specified in REX which is acting as a rule-based front-end to the existing timed automata CASE tool UPPAAL. The rules, events and requirements of application design are specified in REX. To support formal verification, REX automatically transforms the specified rules to timed automata, queries the requirement properties in the model-checker provided by UPPAAL and returns results to the user of REX in terms of rules and events. The results of this thesis consist of guidelines for modeling and verifying rules in a timed automata model-checker and experiences from using and building a tool implementing the proposed guidelines. Moreover, the result of an industrial case study is presented, validating the ability to model and verify a system of industrial complexity using the proposed approach. / Avhandlingen presenterar en ny ansats för att formellt verifiera regel-baserade system. En verktygsprototyp, REX, är utvecklad inom ramen för detta projekt i syfte att stödja ansatsen genom realisering av de teoretiska resultaten. De regler som avses är Event-Condition-Action (ECA) regler, vilket betyder att en regel exekverar ett stycke kod (Action) om ett villkor (Condition) är sant när en specifik händelse (Event) inträffar. ECA-regler är användbara för att speci¯cera beteendet av system som måste reagera på komplexa situationer i sin interagerande miljö. En regel kan till exempel reagera på en kombination av händelser som kan inträffa när som helst och i vilken ordning som helst. Avhandlingen fokuserar på hur man med hjälp av formella metoder kan påvisa att en regelmängd beter sig som förväntat. Användandet av formella metoder för att öka kvalitén på mjukvara är inte så utbrett som det skulle kunna vara. Några av anledningarna kan vara att formella metoder anses svåra att använda och att de kräver extra tid och kunskap. Avhandlingen handlar om en approach där utvecklare kan uttrycka sitt system i ett för dem enkelt språk och där detaljer rörande det formella verktyget döljs av ett verktyg som sköter interaktionen med det formella verktyget. Regler och händelser specificeras som indata till verktyget REX som agerar som en regelbaserad front-end till det formella verktyget UPPAAL. Regler, händelser och egenskaper som modellen ska uppfylla specificeras i REX. Formell verifiering stöds genom att REX automatiskt överför regler och egenskaper till en tidsautomat som kan verifieras av Uppaal. REX startar model-checkern i UPPAAL och returnerar resultatet från analysen till användaren. Resultatet från avhandlingen består av riktlinjer för hur man kan modellera och verifiera regler i en tidsautomat samt erfarenheter från att bygga och använda ett verktyg som implementerar dessa riktlinjer. Därutöver presenteras resultat från experiment och en fallstudie som genomförts för att validera den framtagna ansatsen.

This paper details the design and simulation of a fault-tolerant Quantum-dot Cellular Automata (QCA) NOT gate. A version of the standard NOT gate can be constructed to take advantage to the ability to easily integrate redundant structures into a QCA design. The fault-tolerant characteristics of this inverter are analyzed with QCADesigner v2.0.3 (Windows version) simulation software. These characteristics are then compared with the characteristics of two other non-redundant styles of NOT gates. The redundant version of the gate is more robust than the standard style for the inverter. However, another simple inverter style seems to be even more than this fault-tolerant design. Both versions of the gate will need to be studied further in the future to determine which design is most practical. / Thesis (M.S.)--Wichita State University, College of Engineering, Dept. of Electrical and Computer Engineering / "July 2006." / Includes bibliographic references (leaves 31-33)

Reference monitor inlining is a technique for enforcing security policies by injecting security checks into the untrusted software in a style similar to aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), without adding behavior (conservativity) or affecting existing policy compliant behavior (transparency). This thesis consists of four papers which covers a range of topics including formalization of monitor inlining correctness properties, certification of inlined monitors, limitations in multithreaded settings and extensions using data-flow monitoring. The first paper addresses the problem of having a potentially complex program rewriter as part of the trusted computing base. By means of proof-carrying code we show how the inliner can be replaced by a relatively simple proof-checker. This technique also enables the use of monitor inlining for quality assurance at development time, while minimizing the need for post-shipping code rewrites. The second paper focuses on the issues associated with monitor inlining in a concurrent setting. Specifically, it discusses the problem of maintaining transparency when introducing locks for synchronizing monitor state reads and updates. Due to Java's relaxed memory model, it turns out to be impossible for a monitor to be entirely transparent without sacrificing the security property. To accommodate for this, the paper proposes a set of new correctness properties shown to be realistic and realizable. The third paper also focuses on problems due to concurrency and identifies a class of race-free policies that precisely characterizes the set of inlineable policies. This is done by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete algorithm for inlining of policies inside the class which is secure, conservative, and transparent. The paper also discusses how certification in the style of proof-carrying code could be supported in multithreaded Java programs. The fourth paper formalizes a new type of data centric runtime monitoring which combines monitor inlining with taint tracking. As opposed to ordinary techniques which focus on monitoring linear flows of events, the approach presented here relies on tree shaped traces. The paper describes how the approach can be efficiently implemented and presents a denotational semantics for a simple ``while'' language illustrating how the theoretical foundations is to be used in a practical setting. Each paper is concluded by a practical evaluation of the theoretical results, based on a prototype implementation and case studies on real-world applications and policies. / Referensmonitorinvävning, eller monitorinvävning, är en teknik som används för att se till att en given säkerhetspolicy efterföljs under exekvering av potentiellt skadlig kod. Tekniken går ut på att bädda in en uppsättning säkerhetskontroller (en säkerhetsmonitor) i koden på ett sätt som kan jämföras med aspektorienterad programmering. Syftet med den invävda monitorn är att garantera att policyn efterföljs (säkerhet) utan att påverka ursprungsprogrammets beteende, såvida det följer policyn (transparans och konservativitet). Denna avhandling innefattar fyra artiklar som tillsammans täcker in en rad ämnen rörande monitorinvävning. Bland annat diskuteras formalisering av korrekthetsegenskaper hos invävda monitorer, certifiering av invävda monitorer, begränsningar i multitrådade program och utökningar för hantering av dataflödesmonitorering. Den första artikeln behandlar problemen associerade med att ha en potentiellt komplex programmodifierare som del i den säkerhetskritiska komponenten av ett datorsystem. Genom så kallad bevisbärande kod visar vi hur en monitorinvävare kan ersättas av en relativt enkel beviskontrollerare. Denna teknik möjliggör även användandet av monitorinvävning som hjälpmedel för programutvecklare och eliminerar behovet av programmodifikationer efter att programmet distribuerats. Den andra artikeln fokuserar på problemen kring invävning av monitorer i multitrådade program. Artikeln diskuterar problemen kring att upprätthålla transparans trots införandet av lås för synkronisering av läsningar av och skrivningar till säkerhetstillståndet. På grund av Javas minnesmodell visar det sig dock omöjligt att bädda in en säkerhetsmonitor på ett säkert och transparent sätt. För att ackommodera för detta föreslås en ny uppsättning korrekthetsegenskaper som visas vara realistiska och realiserbara. Den tredje artikeln fokuserar även den på problemen kring flertrådad exekvering och karaktäriserar en egenskap för en policy som är tillräcklig och nödvändig för att både säkerhet och transparens ska uppnås. Detta görs genom att visa att en policy utan egenskapen inte kan upprätthållas på ett säkert och transparent sätt, och genom att beskriva en implementation av en monitorinvävare som är säker och transparent för en policy som har egenskapen. Artikeln diskuterar också hur certifiering av säkerhetsmonitorer i flertrådade program kan realiseras genom bevisbärande kod. Den fjärde artikeln beskriver en ny typ av datacentrisk säkerhetsmonitorering som kombinerar monitorinvävning med dataflödesanalys. Till skillnad mot existerande tekniker som fokuserar på linjära sekvenser av säkerhetskritiska händelser förlitar sig tekniken som presenteras här på trädformade händelsesekvenser. Artikeln beskriver hur tekniken kan implementeras på ett effektivt sätt med hjälp av abstraktion. Varje artikel avslutas med en praktisk evaluering av de teoretiska resultaten baserat på en prototypimplementation och fallstudier av verkliga program och säkerhetsegenskaper. / <p>QC 20130220</p>

No description available.