スターフリー言語 Marcel-Paul Schützenbergerはスターフリー言語を非周期的な構文モノイドを持つ言語として特徴付けた CTLとLTLの違い
スターフリー言語（Star-free language）とは、正規言語の一種で、クレーネ閉包（）を使用せずに正規表現で表現できる言語のことを指します。正規表現におけるクレーネ閉包（）は、その前の要素（文字または文字の集合）が0回以上繰り返されることを示します。
スターフリー言語は、有限オートマトン、特に決定性有限オートマトン（DFA）を使用して表現できますが、非決定性有限オートマトン（NFA）のクレーネ閉包を使った繰り返しを含まないため、その構造が一般の正規言語よりも制約されています。
例えば、アルファベット{a, b}に対して、aまたはbが1回または2回続く言葉を生成する言語はスターフリーです。この言語は、正規表現 a|b|aa|bb|ab|ba で表現できます。この正規表現にはクレーネ閉包（*）が含まれていないため、この言語はスターフリーです。
スターフリー言語は、その特性上、計算能力が制約されているため、実際のアプリケーションでの利用は限られていますが、理論計算機科学の研究において重要な役割を果たしています。
アルファベット、空集合記号、すべてのブール演算子から構成される正規表現で記述できる場合、正規言語はスターフリーであるといいます。
Marcel-Paul Schützenbergerはスターフリー言語を非周期的な構文モノイドを持つ言語として特徴付けた。 また論理的には、小なり関係を持つ自然数上の一階論理FO [<] で定義可能な言語として特徴付けることができるほか、カウンターフリー言語 [6] および線形時間論理(LTL)で定義できる言語として特徴付けることもできる[7]。
すべてのスターフリー言語は一様AC0である。
線形時相論理(LTL) は CTL* (英語版) の一部である。
LTLは、後者（successor、ペアノの公理参照）と「小なり」の関係についての一階述語論理 FO[S,<] と等価である。また、クリーネスターのない正規表現や loop complexity が 0 であるような決定性有限オートマトンも LTL と等価である。
CTLは計算木論理（CTL）と線形時相論理（LTL）のスーパーセットである。パス量 子と時間演算子を自由に組み合わせることができる。CTLと同様、CTLは分岐時間論理である。CTL*式の形式的意味論は、与えられたクリプキ構造に関して定義される。
LTLは1977年にAmir Pnueliによってコンピュータプログラムの検証のために最初に提案された。4年後の1981年にE. M. ClarkeとE. A. EmersonがCTLとCTLモデル検査を発明している。CTL*は、1983年にE. A. EmersonとJoseph Y. Halpernによって定義された[1]。
CTLとLTLはCTL以前に独立して開発された。CTLはこれらの論理と他の論理を表現し、比較するための表現力豊かなテストベッドを提供するため、実用上重要な存在となっています。
計算木論理 (CTL, Computational Tree Logic) と線形時相論理 (LTL, Linear Temporal Logic) は、両方とも時相論理の一種で、システムの動的な振る舞いをモデル化し、検証するために使われます。両者は、システムの状態が時間と共にどのように変化するかを表現するのに使われる論理ですが、それぞれ異なるアスペクトに焦点を当てています。計算木論理 (CTL):
CTLは、システムの全ての可能な進行（すなわち、計算パス）にわたって成立するプロパティを考えます。
CTLの式は、パス量化子と状態量化子を使って構築されます。パス量化子は、全てのパス（A）またはあるパス（E）に対して成立するかどうかを考えます。状態量化子は、現在（X）、将来（F）、過去（G）、または直前（U）の状態について考えます。
例えば、CTLの式 AF p は、「すべての可能なパスにおいて、いずれかの将来の時点で p が成立する」という意味になります。
線形時相論理 (LTL):
LTLは、システムの個々の進行に沿ったプロパティを考えます。
LTLの式は、時相演算子と命題変数を使って構築されます。時相演算子は、次（X）、最終的に（F）、常に（G）、または直前（U）について考えます。
例えば、LTLの式 G p は、「全ての時点で p が成立する」という意味になります。
CTLとLTLは、それぞれ異なるタイプのプロパティを表現するのに適しています。CTLは、システムの全ての可能な進行にわたるプロパティを表現するのに適していますが、LTLは、システムの個々の進行に沿ったプロパティを表現するのに適しています。これらの論理は、システムの動的な振る舞いを検証するための自動化されたツールで使用されます。
確率的計算木論理（PCTL）は、計算木論理（CTL）を拡張し、記述された性質を確率的に定量化することができるようにしたものである。HanssonとJonssonによる論文で定義されている[1]。
PCTLは「あるサービスを要求した後、2秒以内にそのサービスが実行される確率は少なくとも98%である」といったソフトデッドラインの性質を記述するのに有用な論理である。Akin CTLのモデル検査への適性 PCTL拡張は、確率的モデル検査器の特性指定言語として広く利用されている。
本論文では，不自由なデータ型に対して非線形パターンマッチングを可能とするパターンマッチングシステムを提案する．このシステムでは、パターン内に同じ変数が複数回出現すること、パターンマッチングの結果が複数あること、データ型ごとにパターンマッチングの方法をモジュール化することが同時に可能である。これにより、代数的データ型だけでなく、集合やグラフなどの不自由なデータ型や、データが正準形を持たないデータ型に対してもパターンマッチングを表現でき、複数の分解方法を持つことができるようになった。パターン照合はパターンの左辺から実行するルールと、パターン内の変数へのバインディングはパターンの右辺から参照するルールで実現した。さらに、これらのパターンをレキシカル・スコープでモジュール化することを実現した。私のシステムでは，パターンは第一級オブジェクトではないが，パターンのみを取得し，パターンを返すパターン関数は第一級オブジェクトである．この制約により，レキシカル・スコープのある非線形パターンマッチングシステムが簡略化される。私は、このパターンマッチングシステムをプログラミング言語Egisonにすでに実装している。
いいなと思ったら応援しよう！
