This research pursues the use of powerful BDD-based functional circuit analysis to evaluate some approaches to test set generation. Functional representations of the circuit allow the measurement of information about faults that is not directly available through circuit simulation methods, such as probability of random detection and test-space overlap between faults. I have created a software tool that performs experiments to make such measurements and augments existing test generation strategies with this new information. Using this tool, I explored the relationship of fault model difficulty to test set length through fortuitous detection, and I experimented with the application of function-based methods to help reconcile the traditionally opposed goals of making test sets that are both smaller and more effective.

京都大学 / 新制・課程博士 / 博士(情報学) / 甲第23548号 / 情博第778号 / 新制||情||132(附属図書館) / 京都大学大学院情報学研究科通信情報システム専攻 / (主査)教授 湊 真一, 教授 山本 章博, 准教授 川原 純 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM

京都大学 / 0048 / 新制・課程博士 / 博士(情報学) / 甲第19335号 / 情博第587号 / 新制||情||102(附属図書館) / 32337 / 京都大学大学院情報学研究科知能情報学専攻 / (主査)教授 山本 章博, 教授 鹿島 久嗣, 教授 五十嵐 淳 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM

京都大学 / 新制・課程博士 / 博士(情報学) / 甲第24748号 / 情博第836号 / 新制||情||140(附属図書館) / 京都大学大学院情報学研究科通信情報システム専攻 / (主査)教授 湊 真一, 教授 橋本 昌宜, 教授 岡部 寿男 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM

Quantified Boolean formulas (QBFs) play an important role in theoretical computer science. QBF extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. In this dissertation we present our ZQSAT, which is an algorithm for evaluating quantified Boolean formulas. ZQSAT is based on ZBDD: Zero-Suppressed Binary Decision Diagram / which is a variant of BDD, and an adopted version of the DPLL algorithm. It has been implemented in C using the CUDD: Colorado University Decision Diagram package. <br><br> The capability of ZBDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and let us to embed the notion of memoization to the DPLL algorithm. These points led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with a little overheads. ZQSAT can solve some sets of standard QBF benchmark problems (known to be hard for DPLL based algorithms) faster than the best existing solvers. In addition to prenex-CNF, ZQSAT accepts prenex-NNF formulas. We show and prove how this capability can be exponentially beneficial. <br><br> / In der Dissertation stellen wir einen neuen Algorithmus vor, welcher Formeln der quantifizierten Aussagenlogik (engl. Quantified Boolean formula, kurz QBF) löst. QBFs sind eine Erweiterung der klassischen Aussagenlogik um die Quantifizierung über aussagenlogische Variablen. Die quantifizierte Aussagenlogik ist dabei eine konservative Erweiterung der Aussagenlogik, d.h. es können nicht mehr Theoreme nachgewiesen werden als in der gewöhnlichen Aussagenlogik. Der Vorteil der Verwendung von QBFs ergibt sich durch die Möglichkeit, Sachverhalte kompakter zu repräsentieren. <br><br> SAT (die Frage nach der Erfüllbarkeit einer Formel der Aussagenlogik) und QSAT (die Frage nach der Erfüllbarkeit einer QBF) sind zentrale Probleme in der Informatik mit einer Fülle von Anwendungen, wie zum Beispiel in der Graphentheorie, bei Planungsproblemen, nichtmonotonen Logiken oder bei der Verifikation. Insbesondere die Verifikation von Hard- und Software ist ein sehr aktuelles und wichtiges Forschungsgebiet in der Informatik. <br><br> Unser Algorithmus zur Lösung von QBFs basiert auf sogenannten ZBDDs (engl. Zero-suppressed Binary decision Diagrams), welche eine Variante der BDDs (engl. Binary decision Diagrams) sind. BDDs sind eine kompakte Repräsentation von Formeln der Aussagenlogik. Der Algorithmus kombiniert nun bekannte Techniken zum Lösen von QBFs mit der ZBDD-Darstellung unter Verwendung geeigneter Heuristiken und Memoization. Memoization ermöglicht dabei das einfache Wiederverwenden bereits gelöster Teilprobleme. <br><br> Der Algorithmus wurde unter Verwendung des CUDD-Paketes (Colorado University Decision Diagram) implementiert und unter dem Namen ZQSAT veröffentlicht. In Tests konnten wir nachweisen, dass ZQSAT konkurrenzfähig zu existierenden QBF-Beweisern ist, in einigen Fällen sogar bessere Resultate liefern kann.

Functional decomposition aims at finding efficient representations for Boolean functions. It is used in many applications, including multi-level logic synthesis, formal verification, and testing. This dissertation presents novel heuristic algorithms for functional decomposition. These algorithms take advantage of suitable representations of the Boolean functions in order to be efficient. The first two algorithms compute simple-disjoint and disjoint-support decompositions. They are based on representing the target function by a Reduced Ordered Binary Decision Diagram (BDD). Unlike other BDD-based algorithms, the presented ones can deal with larger target functions and produce more decompositions without requiring expensive manipulations of the representation, particularly BDD reordering. The third algorithm also finds disjoint-support decompositions, but it is based on a technique which integrates circuit graph analysis and BDD-based decomposition. The combination of the two approaches results in an algorithm which is more robust than a purely BDD-based one, and that improves both the quality of the results and the running time. The fourth algorithm uses circuit graph analysis to obtain non-disjoint decompositions. We show that the problem of computing non-disjoint decompositions can be reduced to the problem of computing multiple-vertex dominators. We also prove that multiple-vertex dominators can be found in polynomial time. This result is important because there is no known polynomial time algorithm for computing all non-disjoint decompositions of a Boolean function. The fifth algorithm provides an efficient means to decompose a function at the circuit graph level, by using information derived from a BDD representation. This is done without the expensive circuit re-synthesis normally associated with BDD-based decomposition approaches. Finally we present two publications that resulted from the many detours we have taken along the winding path of our research. / QC 20100909

abstract: After a power system blackout, system restoration is the most important task for the operators. Most power systems rely on an off&ndashline; restoration plan and the experience of operators to select scenarios for the black start path. Using an off&ndashline; designed restoration plan based on past experience may not be the most reliable approach under changing network configurations and loading levels. Hence, an objective restoration path selection procedure, including the option to check constraints, may be more responsive in providing directed guidance to the operators to identify the optimal transmission path to deliver power to other power plants or to pick up load as needed. After the system is subjected to a blackout, parallel restoration is an efficient way to speed up the restoration process. For a large scale power system, this system sectionalizing problem is quite complicated when considering black&ndashstart; constraints, generation/load balance constraints and voltage constraints. This dissertation presents an ordered binary decision diagram (OBDD) &ndashbased; system sectionalizing method, by which the splitting points can be quickly found. The simulation results on the IEEE 39 and 118&ndashbus; system show that the method can successfully split the system into subsystems satisfying black&ndashstart; constraints, generation/load balance constraints and voltage constraints. A power transfer distribution factor (PTDF)&ndashbased; approach will be described in this dissertation to check constraints while restoring the system. Two types of restoration performance indices are utilized considering all possible restoration paths, which are then ranked according to their expected performance characteristics as reflected by the restoration performance index. PTDFs and weighting factors are used to determine the ordered list of restoration paths, which can enable the load to be picked up by lightly loaded lines or relieve stress on heavily loaded lines. A transmission path agent can then be formulated by performing the automatic path selection under different system operating conditions. The proposed restoration strategy is tested on the IEEE&ndash39; bus system and on the Western region of the Entergy system. The testing results reveal that the proposed strategy can be used in real time. / Dissertation/Thesis / Ph.D. Electrical Engineering 2010

Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles. / This PhD thesis proposes the theoretical foundations of a new formal tool for symbolic verification of finite models. Some approaches reduce the problem of system verification to the reachability problem in term rewriting systems (TRSs).In our approach, states are encoded by terms in a BDD-like manner and the transition relation is represented by a new rewriting relation so called Functional Term Rewriting Systems (FTRSs).First, we show that FTRSs are as expressive as TRSs. Then, we focus on a subclass of FTRSs, so called Elementary Functional Term Rewriting Systems (EFTRSs), and we show that EFTRSs preserve the FTRSs expressiveness. The main advantage of EFTRSs is that they are well adapted for acceleration techniques usually used in saturation algorithms on BDD-like data structures.Our experiments show that for well-known protocols (e.g. Tree Arbiter, Percolate, Round RobinMutex protocols,... ) our tool is not only better than other rewriting tools such as Timbuk, Maude or TOM, but also competitive with other model-checkers such as SPIN, NuSMV or SMART. Moreover, it can also be applied to model-checking invariant properties which are a particular subclass of linear temporal logic formula (LTL).

Sistemų gedimo modeliavimas paprastai vykdomas taikant taip vadinamus gedimų medžius. Sistemos gedimo tikimybės ir gedimo atsiradimo priežasčių vertinimas dažniausiai atliekamas sudarant minimalių kirtimų aibę (MCS) ir pagal ją įvertinant gedimo tikimybę. Pastaruosius dvidešimt metų tiksliam gedimo tikimybės vertinimui yra taikoma dvejetainė sprendimų diagrama (BDD). Tačiau BDD sudarymo ir taikymo metodika vis dar yra tobulinama. Iki šiol Lietuvoje sistemos gedimo tikimybės vertinimui BDD dar nebuvo taikyta. Pristatant atliktą darbą aprašomi pagrindiniai MCS ir BDD sudarymo metodai bei jų taikymo ypatybės. Taip pat pateikiamas Kauno hidroelektrinės užtvankos vartų valdymo sistemos gedimo modelis ir gedimo tikimybės vertinimas. Šiuo tikslu buvo taikomi skirtingi MCS ir BDD sudarymo metodai bei atitinkamos programinės priemonės. Atlikus bandomuosius skaičiavimus taip pat pateikiamas gautų rezultatų palyginimas. Darbe apibūdinami pagrindiniai MCS ir BDD taikymo privalumai ir trūkumai bei pristatoma naujai sukurta programinė priemonė „DemoITE“. Taikant išanalizuotus algoritmus bei sukurtą programinę priemonę „DemoITE“ buvo ištirtos ir nustatytos sistemos gedimo priežastys bei tiksliai įvertinta sistemos gedimo tikimybė. Be to, pasiūlyta bazinių įvykių rangavimo principas, įgalinantis gauti mažiausią BDD struktūrą. / Modelling of system failure usually is performed applying so-called fault trees. Assessment of system failure probability and failure occurrence causes usually is performed developing a minimal cut-set (MCS) and according to it evaluating probability of system failure. The last twenty years a binary decision diagram (BDD) has been applied for the exact evaluation of system failure. However, a methodology of creation and application of BDD is still under development. Till now in Lithuania for the assessment of system failure probability BDD has not been applied yet. Presenting a performed work the main methods of development of MCS and BDD as well as features of their application is described. Also, the model and assessment of failure of Kaunas hydropower dam gates’ control system is presented. For this task the different methods of development of MCS and BDD as well as corresponding software was applied. Having performed the testing calculations a comparison of results is presented too. In the work the main advantages and disadvantages of MCS and BDD application are described and newly created software “DemoITE” is introduced. The developed algorithms and universal software “DemoITE” is used for visualization of failure causes and for exact estimation of the investigated system failure probability. Also, it is proposed the order of basic events on purpose to design the least BDD.

Binary Decision Diagrams (BDDs) sind eine Datenstruktur für Boolesche Funktionen, die auch unter dem Namen branching program bekannt ist. In ordered binary decision diagrams (OBDDs) müssen die Tests einer festen Variablenordnung genügen. In free binary decision diagrams (FBDDs) darf jede Variable höchstens einmal getestet werden. Die Effizienz neuer Varianten des BDD-Konzepts wird gewöhnlich anhand spektakulärer (worst-case) Beispiele aufgezeigt. Wir verfolgen einen anderen Ansatz und vergleichen die Darstellungsgrößen für fast alle Booleschen Funktionen. Während I. Wegener bewiesen hat, daß für die `meisten' n die erwartete OBDD-Größe einer zufälligen Booleschen Funktion von n Variablen gleich der worst-case Größe bis auf Terme kleinerer Ordnung ist, zeigen wir daß dies nicht der Fall ist für n innerhalb von Intervallen konstanter Länge um die Werte n = 2h + h. Ferner gibt es Bereiche von n, in denen minimale FBDDs fast immer um mindestens einen konstanten Faktor kleiner sind als minimale OBDDs. Unsere Hauptsätze ha ben doppelt exponentielle Wahrschein- lichkeitsschranken (in n). Außerdem untersuchen wir die Entwicklung zufälliger OBDDs und ihrer worst-case Größe und decken dabei ein oszillierendes Verhalten auf, das erklärt, warum gewisse Aussagen im allgemeinen nicht verstärkt werden können. / Binary Decision Diagrams (BDDs) are a data structure for Boolean functions which are also known as branching programs. In ordered binary decision diagrams (OBDDs), the tests have to obey a fixed variable ordering. In free binary decision diagrams (FBDDs), each variable can be tested at most once. The efficiency of new variants of the BDD concept is usually demonstrated with spectacular (worst-case) examples. We pursue another approach and compare the representation sizes of almost all Boolean functions. Whereas I. Wegener proved that for `most' values of n the expected OBDD size of a random Boolean function of n variables is equal to the worst-case size up to terms of lower order, we show that this is not the case for n within intervals of constant length around the values n = 2h + h. Furthermore, ranges of n exist for which minimal FBDDs are almost always at least a constant factor smaller than minimal OBDDs. Our main theorems have doubly exponentially small probability bounds (in n). We also investigate the evolution of random OBDDs and their worst-case size, revealing an oscillating behaviour that explains why certain results cannot be improved in general.