Recently, every main country in the world has implemented transfer pricing system in order to ensure every multinational enterprise would also be able to pay their taxes equitably and reasonably to the countries which they established their multinational enterprises, and has requested the prices of business transaction between every related party have to be set up and adjusted by arm¡¦s length principle. Moreover, in order to follow the initiative of OECD, adopt the current world trend, and avoid the higher inspection risk for our enterprises, Taiwan has established the method of regulation on December twenty- eighth, 2004 by consulting OECD guidelines and tax law of every country in the world, and has started to implement transfer pricing system. The Taiwanese transfer pricing system has integrated in many ways and in many-sided. It also has extended globally. If everyone could cooperate with mutual benefit, the transfer pricing system would be able to maintain the right of native taxation and effectively protect the right of multinational enterprises; hence it is not only a tax system, but art. Therefore, the checking model of transfer pricing system is very different from the case of normal profit-seeking enterprises. The checking model of the current tax authority mainly focuses on their jurisdiction and formal conditions, so it is interesting to see if our tax authority has capability of doing transfer pricing case which emphasizes on the point of taxation principles in substance or not. In addition, because our profit-seeking enterprises are mainly small or middle size corporations, there is a challenge to them to meet their duty and to provide all the requested certificates under the request of the new system, so it is also a point to discuss with. In this research, I tried to establish an evaluation standard by consulting policy estimated theory, and designed a survey which has collected all of recently related books, articles, references, and practiced thoughts in order to have an objective investigation. Also, in the survey, I would like to look into the situations of the following three points after practice of transfer pricing system. First, I would like to find out the thoughts of related interested parties after practice of this policy. Finally, what satisfactions of appropriateness, neutrality, efficiency, responsiveness, and side-effects externalities would be in this policy efficiency analysis? In addition, the collected data were analyzed with Chi-Square test, cross analysis, one-way ANOVA, multiple comparison analysis, and correlation analysis. In my major research findings, transfer pricing system has been known in the certain level by every related interested party. Moreover, this policy is in the high appropriate level and efficient level. However, this policy is in the low neutral level of land tax and other levies, and in the low responsive level. Therefore, there are other side effects in this policy as well, such us: increasing tax misgiving from every enterprise, increasing taxation, and checking cost, etc,. Also, in the result of this research paper, there are twelve suggestions that have collected from the responses of the survey, the problem finding, and some practical difficulties from the study of research institute and some other comments. These twelve suggestions could provide to related government organization as reference material in order to revise the law and advance tax system and tax policy.

The purpose of the present study was to examine the underlying mechanism of memory distrust as a function of repeated checking in a nonclinical student sample. Recent literature proposes that repeated checking increases familiarity with the material checked. Then, familiarity makes the recollections less vivid and detailed. Afterwards, this condition promotes distrust in memory. Before the experimental phase of the study, Padua Inventory- Washington State University Revision (PI-WSUR) and demographic information form were applied to the 381 students (232 female, 149 male) university students. Then, 84 students were selected according to their PI-WSUR scores. The students scored half standard deviation below the mean of the group were assigned to the low OCD group (N= 42) and the students scored half standard deviation above the mean were assigned to the high OCD group (N= 42). In the experimental phase of the study, an interactive computer animation was developed to test repeated checking behavior. Before the experiment, participants were randomly assigned to two groups: primed with feedback group and primed with no feedback group. In the experiment, participants were all asked to carry out checking rituals on a virtual gas ring. Each participant performed turning on, turning off and checking processes for 15 trials. However, half of the participants in the primed with feedback group were given feedback indicating that the checking activity was successful and complete and half of the participants in the primed with no feedback group were not given any feedback. The data are analyzed by 2 (Group: Low OCD group - High OCD Group) X 2 (Feedback condition: Primed with Feedback Group - Primed with no Feedback Group) Between Subjects ANOVA. Results showed that participants in the primed with feedback group had significantly higher scores on both memory confidence for the last checking trial of the gas rings and overall outcome confidence for all fifteen checking trials than participants in the primed with no feedback group. There was no significant group main effect and interaction effect (group x feedback condition) for the level of memory confidence and overall outcome confidence. There were also no significant group and feedback condition main effects and interaction effect for the level of vividness and detail of the recollections of the last checking behavior. Results are discussed in the light of the related literature.

Model checking is a formal verification technique which is widely used in different areas for automated verification and analysis. In this study, we applied a Model Checking method to a biological system. Firstly we constructed a single-cell, Boolean network model for the signaling pathways of apoptosis (programmed cell death) in lung cancers by combining the intrinsic and extrinsic Apoptosis pathways, p53 signaling pathway and p53 - DAP Kinase pathway in Lung cancers. We translated this model to the NuSMV input language. Then we converted known experimental results to CTL properties and checked the conformance of our model with respect to biological experimental results. We examined the dynamics of the apoptosis in lung cancer using NuSMV symbolic model checker and identified the relationship between apoptosis and lung cancer. Finally we generalized the whole process by introducing translation rules and CTL property patterns for biological queries so that model checking any signaling pathway can be automated.

This study focuses on the development of a new, formal method for the automated checking of pedestrian circulation rules in Courthouse Design Guide. Automated building rule checking is an automated process of design evaluation against design requirements. Since the early 1970's, when the electronic representation of building design became available, automated building rule checking, a computational process, has been a focus of study, and it continues to be a popular research area because it facilitates the design evaluation process by reducing the checking time and evaluation costs and by increasing the objectivity and the reliability of the evaluation. Thanks to the emergence of BIM (Building Information Model) authoring software, BIM became available to use in real building design, and several automated building code checking systems were developed based on BIM. In practice, the use of a rule checking system in real design evaluation may be influenced by several factors. Among the factors that affect the accuracy and the reliability of automated checking such as checking algorithms and rule interpretation is the level of completeness of the BIM in the design process, which can cause limitations in the application of a rule checking algorithm to the model. Problems caused by the incompleteness of the BIM occurred in CORENET project, a project initiated by the Singapore government in 1999 for automation of building code checking, and GSA Courthouse Design Guide Automation project (GSA), initiated at Georgia Tech in 2007 also faced with the same problems caused by incompleteness of BIM in the development stage. This thesis is a continuing research of GSA-Courthouse Design Guide Automation project (Simply, GSA project). The theoretical goals of this study are to provide a logical foundation upon which one can build an automated checking module for circulation rule checking and that is capable of outlining the rule-validation process independently from its diverse implementation. The theory for circulation rule checking is devised to represent the process of the validation of a building design in the development stage. The theory deals with issues of validation caused by the lack of data in the development of a building design.

<p>Pyrosequencing is a DNA sequencing method based on thedetection of released pyrophosphate (PPi) during DNA synthesis.In a cascade of enzymatic reactions, visible light isgenerated, which is proportional to the number of nucleotidesincorporated into the DNA template. When dNTP(s) areincorporated into the DNA template, inorganic PPi is released.The released PPi is converted to ATP by ATP sulfurylase, whichprovides the energy to luciferase to oxidize luciferin andgenerate light. The excess of dNTP(s) and the ATP produced areremoved by the nucleotide degrading enzyme apyrase.</p><p>The commercially available enzymes, isolated from nativesources, show batch-tobatch variations in activity and quality,which decrease the efficiency of the Pyrosequencing reaction.Therefore, the aim of the research presented in this thesis wasto develop methods to recombinantly produce the enzymes used inthe Pyrosequencing method. Production of the nucleotidedegrading enzyme apyrase by Pichia pastoris expression system,both in small-scale and in an optimized large-scale bioreactor,is described. ATP sulfurylase, the second enzyme in thePyrosequencing reaction, was produced in<i>Escherichia coli</i>. The protein was purified and utilizedin the Pyrosequencing method. Problems associated with enzymecontamination (NDP kinase) and batch-to-batch variations wereeliminated by the use of the recombinant ATP sulfurylase.</p><p>As a first step towards sequencing on chip-format,SSB-(single-strand DNA binding protein)-luciferase and KlenowDNA polymerase-luciferase fusion proteins were generated inorder to immobilize the luciferase onto the DNA template.</p><p>The application field for the Pyrosequencing technology wasexpanded by introduction of a new method for clone checking anda new method for template preparation prior the Pyrosequencingreaction.</p><p><b>Keywords:</b>apyrase, Pyrosequencing technology, Z_basictag fusion, luciferase, ATP sulfurylase, dsDNAsequencing, clone checking, Klenow-luciferase, SSB-luciferase,<i>Pichia pastoris, Echerichia coli</i>.</p>

<p>This work focuses on the usage of dominators in circuit graphs in order to reduce the complexity of synthesis and verification tasks. One of the contributions of this thesis is a new algorithm for computing multiple-vertex dominators in circuit graphs. Previous algorithms, based on single-vertex dominators suffer from their rare appearance in many circuits. The presented approach searches efficiently for multiple-vertex dominators in circuit graphs. It finds dominator relations, where algorithms for computing single-vertex dominators fail. Another contribution of this thesis is the application of dominators for combinational equivalence checking based on the arithmetic transform. Previous algorithms rely on representations providing an explicit or implicit disjoint function cover, which is usually excessive in memory requirements. The new algorithm allows a partitioned evaluation of the arithmetic transform directly on the circuit graph using dominator relations. The results show that the algorithm brings significant improvements in memory consumption for many benchmarks. Proper cuts are used in many areas of VLSI. They provide cut points, where a given problem can be split into two disjoint sub-problems. The algorithm proposed in this thesis efficiently detects proper cuts in a circuit graph and is based on a novel concept of a reduced dominator tree. The runtime of the algorithm is less than 0.4 seconds for the largest benchmark circuit. The final contribution of this thesis is the application of the proper cut algorithm as a structural method to decompose a Boolean function, represented by a circuit graph. In combination with a functional approach, it outperforms previous methods, which rely on functional decomposition only.</p>

<p>Model checking is a formal verification method where one tries to prove or disprove properties of a formal system. Typical systems one might want to prove properties within are network protocols and digital circuits. Typical properties to check for are safety (nothing bad ever happens) and liveness (something good eventually happens).</p><p>This thesis describes an implementation of a sound and complete model checker for Computation Tree Logic (CTL) using Constraint Logic Programming over Finite Domains (CLP(FD)). The implementation described uses tabled resolution to remember earlier computations, is parameterised by choices of computation strategies and can with slight modification support different constraint domains. Soundness under negation is maintained through a restricted form of constructive negation.</p><p>The computation process amounts to a fixpoint search, where a fixpoint is reached when no more extension operations has any effect. As results show, the choice of strategies does influence the efficiency of the computation. Soundness and completeness are of course independent of the choice of strategies. Strategies include how to choose the extension operation for the next step and whether to perform global or local rule instantiations, resulting in bottom-up or top-down computations respectively.</p>

Ce mémoire propose des représentations formelles pour contrôleurs logiques industriels qui visent à améliorer le passage à l'échelle des techniques de model-checking. Ces vérifications, focalisées sur les propriétés extrinsèques, permettent d'améliorer la sûreté et aident à la certification de ces contrôleurs. Premièrement, la représentation de contrôleurs ne comprend que les états qui sont pertinents pour la preuve de propriétés et minimise le nombre de variables qui caractérisent chaque état. Puis une représentation de chaque bloc fonctionnel, décrit dans un nouveau langage formel adapté à nos besoins, est incluse dans la représentation du contrôleur. Ces représentations permettent la vérification formelle du contrôleur, même avec des programmes de grande taille. La comparaison avec de précédentes représentations, ainsi que leur utilisation dans un contexte industriel, valide nos représentations et quantifie leur efficacité.

Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (Predicate Diagram for Timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés.

De nombreux sytèmes critiques comportent des aspects temporisés, où interviennent de manière cruciale des contraintes quantitatives sur les délais séparant certaines actions. Un automate programmable industriel (API) constitue un composant fondamental d'un système souvent critique destiné à réagir et à communiquer en temps réel avec son environnement. Ma thèse se situe dans le contexte de la vérification de propriétés temporisées des APIS. Plus précisement, on propose une sémantique formelle à base d'automates temporisés pour la modélisation d'une sous classe de programmes Ladder comportant des blocs TON. On fournie une logique temporisée dont la sémantique permet de considérer seulement les événements "signifcatifs" (c'est à dire les événements qui durent suffisamment longtemps). On propose deux sémantiques différentes pour cette logique: sémantique "locale" et sémantique "globale". Pour la sémantique "locale", on a obtenu plusieurs résultats d'expressivité et grâce à une nouvelle relation d'équivalence, on montre que son model checking reste décidable sans modifier la complexité théorique. En revanche, pour la sémantique "globale", le model checking devient indécidable.