This thesis presents several algorithms that update the vertex separation of a tree after the tree is modified; the vertex separation of a graph measures the largest number of vertices to the left of and including a vertex that are adjacent to vertices to the right of the vertex, when the vertices in the graph are arranged in the best possible linear ordering. Vertex separation was introduced by Lipton and Tarjan and has since been applied mainly in VLSI design. The tree is modified by either attaching another tree or removing a subtree. The first algorithm handles the special case when another tree is attached to the root, and the second algorithm updates the vertex separation after a subtree of the root is removed. The last two algorithms solve the more general problem when subtrees are attached to or removed from arbitrary vertices; they have good running time performance only in the amortized sense. The running time of all our algorithms is sublinear in the number of vertices in the tree, assuming certain information is precomputed for the tree. This improves upon current algorithms by Skodinis and Ellis, Sudborough, and Turner, both of which have linear running time for this problem. Lower and upper bounds on the vertex separation of a general graph are also derived. Furthermore, analogous bounds are presented for the cutwidth of a general graph, where the cutwidth of a graph equals the maximum number of edges that cross over a vertex, when the vertices in the graph are arranged in the best possible linear ordering.

This thesis presents several algorithms that update the vertex separation of a tree after the tree is modified; the vertex separation of a graph measures the largest number of vertices to the left of and including a vertex that are adjacent to vertices to the right of the vertex, when the vertices in the graph are arranged in the best possible linear ordering. Vertex separation was introduced by Lipton and Tarjan and has since been applied mainly in VLSI design. The tree is modified by either attaching another tree or removing a subtree. The first algorithm handles the special case when another tree is attached to the root, and the second algorithm updates the vertex separation after a subtree of the root is removed. The last two algorithms solve the more general problem when subtrees are attached to or removed from arbitrary vertices; they have good running time performance only in the amortized sense. The running time of all our algorithms is sublinear in the number of vertices in the tree, assuming certain information is precomputed for the tree. This improves upon current algorithms by Skodinis and Ellis, Sudborough, and Turner, both of which have linear running time for this problem. Lower and upper bounds on the vertex separation of a general graph are also derived. Furthermore, analogous bounds are presented for the cutwidth of a general graph, where the cutwidth of a graph equals the maximum number of edges that cross over a vertex, when the vertices in the graph are arranged in the best possible linear ordering.

This thesis presents the first sub-quadratic circle graph recognition algorithm, and develops improved algorithms for two important hierarchical decomposition schemes: modular decomposition and split decomposition. The modular decomposition algorithm results from unifying two different approaches previously employed to solve the problem: divide-and-conquer and factorizing permutations. It runs in linear-time, and is straightforward in its understanding, correctness, and implementation. It merely requires a collection of trees and simple traversals of these trees. The split-decomposition algorithm is similar in being straightforward in its understanding and correctness. An efficient implementation of the algorithm is described that uses the union-find data-structure. A novel charging argument is used to prove the running-time. The algorithm is the first to use the recent reformulation of split decomposition in terms of graph-labelled trees. This facilitates its extension to circle graph recognition. In particular, it allows us to efficiently apply a new lexicographic breadth-first search characterization of circle graphs developed in the thesis. Lexicographic breadth-first search is additionally responsible for the efficiency of the split decomposition algorithm, and contributes to the simplicity of the modular decomposition algorithm.

This thesis presents the first sub-quadratic circle graph recognition algorithm, and develops improved algorithms for two important hierarchical decomposition schemes: modular decomposition and split decomposition. The modular decomposition algorithm results from unifying two different approaches previously employed to solve the problem: divide-and-conquer and factorizing permutations. It runs in linear-time, and is straightforward in its understanding, correctness, and implementation. It merely requires a collection of trees and simple traversals of these trees. The split-decomposition algorithm is similar in being straightforward in its understanding and correctness. An efficient implementation of the algorithm is described that uses the union-find data-structure. A novel charging argument is used to prove the running-time. The algorithm is the first to use the recent reformulation of split decomposition in terms of graph-labelled trees. This facilitates its extension to circle graph recognition. In particular, it allows us to efficiently apply a new lexicographic breadth-first search characterization of circle graphs developed in the thesis. Lexicographic breadth-first search is additionally responsible for the efficiency of the split decomposition algorithm, and contributes to the simplicity of the modular decomposition algorithm.

金融風暴喚起各界改革財務報表未能反映實際虧損的缺失，因此，新版國際財務報導準則第9號及第17號公報應運而生，未來正式接軌後，對於壽險業的財報將產生重大衝擊，更突顯其資產負債管理之重要性，故本研究係採用主成分分析建構極端利率情境，並考量折現率需反映現時狀況下，於資產面分別以攤銷後成本或公允價值衡量、負債面採公允價值評價，欲探討資產負債配置及攤銷後成本比重不同時，利率變動對於壽險公司股東權益波動度之影響，以供壽險業參考。 研究結果發現攤銷後成本比重能夠有效控制股東權益波動度。再者，壽險公司應審慎評估海外投資比例，並配合其壽險商品外幣保單之銷售策略加以布局，同時謹慎考量會計決策，適當選擇攤銷後成本權重，方能有效控制資產負債表之波動。 / The financial crisis has caused wide public concern since it is failed to reflect the actual losses in financial statements. As a result, International Accounting Standards Board (IASB) issued new International Financial Reporting Standards, IFRS 9 and IFRS 17. The surplus of life insurers may fluctuate sharply if assets and liabilities don’t match appropriately under these new IFRS Standards. We follow the international regulation standard by using principal component analysis to generate extreme interest rate shock scenarios. This study examines the volatility of surplus under extreme interest rate shock scenarios for different combinations of liabilities, fair-valued assets, and amortized cost assets. In particular, the assets are measured at amortized cost or fair value, and all liabilities were acquired at fair value approach. In the numerical analysis, we showed that it is one of the most effective methods to control the surplus volatility by adjusting the percentage of amortized cost assets. Furthermore, life insurer should adjust the percentage of foreign investments and insurance policies carefully in order to reduce the fluctuation in shareholders’ equity.

Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.