パトリシア・ブイヤー・デシトル

パトリシア・ブイヤー＝デシトル（Patricia Bouyer、1976年生まれ）は、時間オートマトン、モデル検査、 時相論理の研究で知られるフランスの理論計算機科学者である。^[1]彼女はフランス国立科学研究センター（CNRS）の上級研究員であり、CNRSとパリ・サクレー高等師範学校の形式手法研究室（Laboratoire Méthodes Formelles）の所長である。^[2]

パトリシア・ブイヤーは1976年生まれ。^[1] 1996年にENSパリ・サクレー（当時はENSカシャン）に入学し、1997年に数学の修士号、1998年にコンピュータサイエンスの2番目の修士号とディプロム・デ・エチュード・アプロフォンディを取得し、1999年に数学のアグレガシオンに合格した。 ^[3]

彼女は博士号を取得しました。 2002 年、CNRS と ENS Cachan の仕様と検証のラボラトワールで。彼女の学位論文「Modeles et Algorithmes pour la Vérification des Systèmes Temporisés (時限システム検証のためのモデルとアルゴリズム)」は、Antoine Petit  [fr]によって監修されました。^{[1] [3] [4]}彼女は2009 年にパリ ディドロ大学でハビリテーションを修了し、ハビリテーションの論文「時間システムの定性的分析から定量的分析へ」を執筆しました。^[1]

彼女は2002年にオールボー大学のポスドク研究員となり、2002年にはCNRSのジュニア研究員にもなり、2010年に上級研究員に昇進した。^[3]

Bouyer は、時間オートマトンに関するいくつかの重要な結果で知られています。1997 年に始まり、2003 年に Luca Aceto、Augusto Burgueno、Kim Larsen と共同で発表した研究で、Bouyer は時間オートマトンにおける到達可能性の観点から記述できる特性を特徴付けました。^{[1] [A]} Petit および Denis Thérien とともに、彼女は時間オートマトンにおけるKleene の定理の類似物を発見し、それらが特定のクラスの形式言語と同等であることを示しました。^{[1] [B]} Catherine Dufourd、Emmanuel Fleury、Antoine Petit とともに、彼女は更新可能な時間オートマトン、つまりタイミング変数を単にゼロにリセットするのではなく更新する操作を含む時間オートマトン拡張を紹介し、これらのオートマトンで空問題が決定可能ないくつかの重要なサブクラスを発見しました。^{[1] [C]}

時相論理において、ブイヤーはファブリス・シュヴァリエおよびニコラス・マーキーと共同で、時相論理の一種である時間付き命題時相論理が、もうひとつの形式である計量時相論理よりも表現力に優れていることを証明した。^{[1] [G]彼女の研究の他のトピックには、時間付きオートマトンを}障害検出に適用すること、^[E]時間付きオートマトンにコストとエネルギー制約を追加すること、^{[D] [F]}ゲーム理論の時間付きバージョンにおけるナッシュ均衡の存在などがある。^[H]

ブイヤー＝デシトルは2007年にCNRS銅メダルを受賞した。彼女は2011年に欧州理論計算機科学協会のプレスブルガー賞を受賞した。^[1]

• Google Scholarにインデックスされた Patricia Bouyer-Decitre の出版物