Yes / Quantitative risk assessment (QRA) approaches systematically evaluate the likelihood, impacts, and risk of adverse events. QRA using fault tree analysis (FTA) is based on the assumptions that failure events have crisp probabilities and they are statistically independent. The crisp probabilities of the events are often absent, which leads to data uncertainty. However, the independence assumption leads to model uncertainty. Experts’ knowledge can be utilized to obtain unknown failure data; however, this process itself is subject to different issues such as imprecision, incompleteness, and lack of consensus. For this reason, to minimize the overall uncertainty in QRA, in addition to addressing the uncertainties in the knowledge, it is equally important to combine the opinions of multiple experts and update prior beliefs based on new evidence. In this article, a novel methodology is proposed for QRA by combining fuzzy set theory and evidence theory with Bayesian networks to describe the uncertainties, aggregate experts’ opinions, and update prior probabilities when new evidences become available. Additionally, sensitivity analysis is performed to identify the most critical events in the FTA. The effectiveness of the proposed approach has been demonstrated via application to a practical system. / The research of Sohag Kabir was partly funded by the DEIS project (Grant Agreement 732242).

Yes / Fault tree analysis (FTA) is a powerful technique that is widely used for evaluating system safety and reliability. It can be used to assess the effects of combinations of failures on system behaviour but is unable to capture sequence dependent dynamic behaviour. A number of extensions to fault trees have been proposed to overcome this limitation. Pandora, one such extension, introduces temporal gates and temporal laws to allow dynamic analysis of temporal fault trees (TFTs). It can be easily integrated in model-based design and analysis techniques. The quantitative evaluation of failure probability in Pandora TFTs is performed using exact probabilistic data about component failures. However, exact data can often be difficult to obtain. In this paper, we propose a method that combines expert elicitation and fuzzy set theory with Pandora TFTs to enable dynamic analysis of complex systems with limited or absent exact quantitative data. This gives Pandora the ability to perform quantitative analysis under uncertainty, which increases further its potential utility in the emerging field of model-based design and dependability analysis. The method has been demonstrated by applying it to a fault tolerant fuel distribution system of a ship, and the results are compared with the results obtained by other existing techniques.

Yes / Fuzzy data-driven reliability analysis has been used in different safety-critical domains for risk assessment and decision-making where precise failure data is non-existent. Expert judgements and fuzzy set theory have been combined with different variants of fault trees as part of fuzzy data-driven reliability analysis studies. In such fuzzy fault tree analyses, different people represented failure data using different membership functions for the fuzzy set, and different parameters were set differently in the expert opinion elicitation process. Due to the availability of a wide variety of options, it is possible to obtain different outcomes when choosing one option over another. This article performed an analysis in the context of fuzzy data-based temporal fault tree analysis to investigate the effect of choosing different membership functions on the estimated system reliability and criticality ranking of different failure events. Moreover, the effect of using different values for the relaxation factor, a parameter set during the expert elicitation process, was studied on the system reliability and criticality evaluation. The experiments on the fuel distribution system case study show system reliability did not vary when triangular and trapezoidal fuzzy numbers were used with the same upper and lower bounds. However, it was seen that the criticality rankings of a couple of events were changed due to choosing different membership functions and different values of relaxation factor

No / In recent decades, sustainable investing has caught on with investors, and it has now become the norm. In the age of start-ups, with scant information on the sustainability aspects of an asset, it becomes harder to pursue sustainable investing. To this end, this paper proposes a sustainable financial portfolio selection approach in an intuitionistic fuzzy framework. We present a comprehensive three-stage methodology in which the assets under consideration are ethically screened in Stage-I. Stage-II is concerned with cal- culating the sustainability scores, based on various social, environmental, and economic (SEE) criteria and an evaluation of the return and risk of the ethical assets. Intuitionistic fuzzy set theory is used to gauge the linguistic assessment of the assets on several SEE criteria from multiple decision-makers. A novel intuitionistic fuzzy multi-criteria group decision-making technique is applied to calculate the sustainability score of each asset. Finally, in Stage-III, an intuitionistic fuzzy multi-objective financial portfolio selection model is developed with maximization of the satisfaction degrees of the sustainabil- ity score, return, and risk of the portfolio, subject to several constraints. The ε-constraint method is used to solve this model, which yields various efficient, sustainable financial portfolios. Subsequently, investors can choose the portfolio best suited to their preferences from this pool of efficient, sustainable financial portfolios. A detailed empirical illustration and a comparison with existing works are given to substantiate and validate the proposed approach. / Institution of Eminence, University of Delhi, Delhi-110007 under Faculty Research Program

Specification plays a vital role in software engineering to facilitate the development of highly dependable software. The importance of specification in software development is to serve, amongst others, as a communication tool for stakeholders in the software project. The specification also adds to the understanding of operations, and describes the properties of a system. Various techniques may be used for specification work. Z is a formal specification language that is based on a strongly-typed fragment of Zermelo-Fraenkel set theory and first-order logic to provide for precise and unambiguous specifications. Z uses mathematical notation to build abstract data, which is necessary for a specification. The role of abstraction is to describe what the system does without prescribing how it should be done. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. Diagrams, on the other hand, have also been used in various areas, and in software engineering they could be used to add a visual component to software specifications. It is plausible that diagrams may also be used to reason in a semi-formal way about the properties of a specification. Many diagrammatic languages are based on contours and set theory. Examples of these languages are Euler-, Spider-, Venn- and Pierce diagrams. Euler diagrams form the foundation of most diagrams that are based on closed curves. The purpose of this research is to demonstrate the extent to which diagrams can be used to represent a Z specification. A case study is used to transform the specification modelled with Z language into a diagrammatic specification. Euler, spider, Venn and Pierce diagrams are combined for this purpose, to form one diagrammatic notation that is used to transform a Z specification / School of Computing / M. Sc. (Information Systems)

No description available.

Fuzzy relational databases deal with imprecise data or fuzzy information in a relational database. The purpose of this fuzzy database implementation is to retrieve images by using fuzzy queries whose common-language descriptions are defined by the consensus of a particular user community. The fuzzy set, which is presentation of fuzzy attribute values of the images, is determined through membership function. This paper compares two methods of constructing membership functions, the Direct Rating and New Random Proportional, to determine which method gives maximum users satisfaction with minimum feedback from the community. The statistical analysis of results suggests the use of Direct Rating method. Moreover, the analysis shows that the performance of the New Random Proportional method can be improved with the inclusion of a "Not" modifier. This paper also identifies and analyzes issues that are raised by different versions of the database system.

The GUHA method is one of the oldest methods of exploratory data analysis, which is regarded as part of the data mining or knowledge discovery in databases (KDD) scienti_c area. Unlike many other methods of data mining, the GUHA method has firm theoretical foundations in logic and statistics. In scope of the method, finding interesting knowledge corresponds to finding special formulas in satisfactory rich logical calculus, which is called observational calculus. The main topic of the thesis is application of the "fuzzy paradigm" to the GUHA method By the term "fuzzy paradigm" we mean approaches that use many-valued membership degrees or truth values, namely fuzzy set theory and fuzzy logic. The thesis does not aim to cover all the aspects of this application, it emphasises mainly on: - Association rules as the most prevalent type of formulas mined by the GUHA method - Usage of fuzzy data - Logical aspects of fuzzy association rules mining - Comparison of the GUHA theory to the mainstream fuzzy association rules - Implementation of the theory using the bit string approach The thesis throughoutly elaborates the theory of fuzzy association rules, both using the theoretical apparatus of fuzzy set theory and fuzzy logic. Fuzzy set theory is used mainly to compare the GUHA method to existing mainstream approaches to formalize fuzzy association rules, which were studied in detail. Fuzzy logic is used to define novel class of logical calculi called logical calculi of fuzzy association rules (LCFAR) for logical representation of fuzzy association rules. The problem of existence of deduction rules in LCFAR is dealt in depth. Suitable part of the proposed theory is implemented in the Ferda system using the bit string approach. In the approach, characteristics of examined objects are represented as strings of bits, which in the crisp case enables efficient computation. In order to maintain this feature also in the fuzzy case, a profound low level testing of data structures and algoritms for fuzzy bit strings have been carried out as a part of the thesis.

O presente trabalho centra-se no estudo da narrativa do romance O Castelo, escrito em 1922, pelo escritor tcheco Franz Kafka. Por meio da análise formal da obra em questão, objetiva-se estabelecer relações entre aspectos presentes na narrativa que possuam associações metafóricas a temas vigentes no cotidiano do autor e, conseqüentemente, do homem moderno, e que possuam conotação negativa, tais como o poder, simbolizado pela burocracia, pela divinização, e pelo espaço. Partindo dessa premissa, propõe-se relacionar esses temas à teoria dos conjuntos da matemática, na qual um conjunto maior contém um conjunto menor, esse atuando por sua vez como um subconjunto daquele. Propõe-se aqui fazer uma analogia do conjunto poder e seu enfoque negativo como poder com o subconjunto burocracia, este intimamente ligado àquele, e que possui intersecção com os subconjuntos divinização e espaço. Por fim, ressaltar-se-á a universalidade da obra de Kafka, que possibilita a efetuação de analogias temáticas das mais diversas, não só as aqui expostas em forma de conjuntos e subconjuntos, pelo fato de seu texto ser multifacetado no tocante a temas. / This monograph focuses on analyzing the narrative of The Castle, a novel written by the Czech author Franz Kafka, in 1922. It aims at establishing a connection between certain aspects within the text which may have a metaphorical association with themes related to not only the authors life experiences, but also any other modern mans. It will be centered on a formal analysis of the novel and on metaphorical aspects within the narrative, which may have a negative connotation linked with power, represented by bureaucracy, divinization and space. Afterwards, we will propose a relation of such themes to the set theory from Mathematics, in which a greater set contains a smaller set, also known as a subset. We aim at drawing an analogy of power as a set and its negative connotation with the bureaucratic subset, which are intimately connected. Bureaucracy intersects the two other subsets called divinization and space. Eventually, we will focus on the universality of Kafkas work, which enables the drawing of many other thematic analogies, not only the ones discussed in this set theory proposed in this monograph, due to the fact that Kafkas work is multifaceted in terms of themes.

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS