Software Science under Uncertainties:
A Survey
Ichiro Hasuo
National Institute of Informatics & SOKENDAI
Research Director, ERATO MMSD Project
PPL 2021 (Category 4), 2021/03/11

Some slides are by
Satoshi Kura,
Toru Takisaka,
Masaki Waga,
Zhenya Zhang

1情報システムの安全性と「不確かさ」
複雑な情報システム （例：⾃動運転⾞，1B LoC）

ソフトウェア科学における形式検証 formal verification

根本的な問い：• 安全に動作するか？
• 設計にミスはないか？
• 実装にバグはないか？

••

論理的記述の困難な情報システムの出現・普及
論理的記述 ＝ モデリング，数学的定義
例：• 物理情報システム：
物理的外界の完全な論理的記述は困難•

機械学習システム：
ノイジーなデータから数値最適化でルールを学習➜ ルールの論理的記述は困難

バグ不在・安全性を数学の定理として論理的に証明
前提：プログラムは⼈の⼿で⽣み出される論理的実体なので，その振る舞いを数学的に記述（定義）できる

不確かさを内包する
情報システムの安全性保証というチャレンジ•••

ソフトウェア科学の新パラダイム
テストの利⽤が不可避➜ 統計知と論理知の融合（AI 研究の⼀⼤課題）
我々のスローガン：（不確かさのもとでも）論理的⼿法が必要かつ有効

2

不確かさに対応するソフトウェア科学
求ム 良い名前
こういう「分野」ってなんと呼べばいいでしょうか．．．

ソフトウェア
⼯学
テストと論理的証明の融合
Safe AI,
Explainable AI (XAI)

統計的機械学習・AI

不確かさに対応する
ソフトウェア科学
統計知と論理知の融合

連続ダイナミクスと離散ダイナミクスの
数学的統⼀

制御理論

（従来の）
ソフトウェア科学

3

ERATO MMSD での取り組み (2016-2022)• 学際的研究体制
4つの学術分野が共通の理論基盤と応用目標を通じて密接に協働「メタ数理」の役割：
理論的研究の営為⾃体を理論的に解析➜ 理論研究者の応⽤進出を実現（次スライド参照）• 国際的研究体制• グループの1つをカナダ Waterloo ⼤学に設置．
実際の⾃動運転⾞を運⽤• 研究員の半数以上を海外から雇⽤

44ERATO Metamathematics for Systems Design Project「メタ理論」の直接・間接のご利益• 直接のご利益：メタ数理的移転• 「理論の抽象的ひな形」を⽤いて⼿法を移転• 離散➜連続，定性➜定量の移転に特に効果的• 成功例： 圏論，論理学を経由した移転➜ 確率的システムのモデル検査⼿法[Takisaka+, ATVAʼ18] [Komorida+, LICSʼ19]• 間接のご利益： 学際協働のインタプリタ• ⼀般に，理論➜応⽤の向きの移動のほうが逆よりも楽• メタ理論家の「内省」能⼒は（⾃らの研究活動を省みる）
異分野をつなげるときに特に有効• 成功例： ⾃動運転⾞のゲーム理論的意思決定[Pruekprasert+, ITSCʼ19]

⾃動運転安全性の形式検証 [Hasuo+, in preparation]5

Outline
モデル

確率的モデル検査，確率的検証[Kura+, TACASʼ19] [Phalakarn et al., CAVʼ20] を例に実⾏時検証，モニタリング[Waga+, CAVʼ19] を例に

サーチベーステスト＋論理・離散的構造[Zhang+, CAVʼ19] を例に

⾃動運転システムの安全性検証[Kobayashi+, NFMʼ21] を例に（➜ 実応⽤
可能性）

不確かさの
種類

解析⼿法

モデル要
(whitebox)

known
unknowns

formalモデル不要

unknown
unknowns

formalblackbox
モデルのみ
要

unknown
unknowns

testing

部分的モデル要unknown
unknowns

formal6確率的形式検証• 対象システム：
確率的分岐のある状態遷移系や
プログラム
（右図）

Our Approach

Stochastic game (2.5 players).
(Subsumes MDP (1.5 pl.),Markov chain (0.5 pl.))Use parametric certificates, i.e. functions• ⽬標：• 到達可能性・実⾏時間に関する検証<latexit sha1_base64="ZvzVp2GFqRo/MXbV5YAPAFQ/a3Y=">AAAtnXiczVpbc9y2FVZ6TdRb0j72oUjXnsjOStHKk2kmjjy21lbiiSIrkuJ4RpQVkAR3EZEEDWAlbWj+nv6avrbTf9NzQO4SBLhJennozkjLg/Ph4HauWIZFypXe3v7nGz/56c9+/otfvvnW+q9+/Zvf/u7td37/XImZjNhXkUiFfBFSxVKes6801yl7UUhGszBlX4eXY+R/fcWk4iI/1fOCnWd0kvOER1RD08Xbj0gQ8km6EQyTizKtApSYkyCjehqG5XH1ssyrQIu2IRhiB3kH0AHPyUF18fZge2vbfIj/MGoeBmvN5+jineHjIBbRLGO5jlKq1Nlou9DnJZWaRymr1oOZYgWNLumEncFjTjOmzkuz1orchpaYJELCX66JabV7lDRTap6FgMQ5K5eHjX28s5lOPjoveV7MNMujeqBklhItCG4ciblkkU7n8EAjyWGuJJpSSSMN29sZhWl2A/3J6ZQrks2UJiEjespIwiUQDQwFQ3sqaMzidfjYIhKaR/NQ3Ayb1eA3SNXDZgXDdaUzKucyHl5TNQfIEE45hEPNhoUUIhneKJDFKkLWb9urjK94AZtZKC15dKm6m83yCajc9LwMacjSLo+m6Xl5M69A3FhkBU/ZFxRlMEXWg5u5KFCfyqudyqKimbxidsNOxNLUbpBCU42QE5bC7p7C5Mooq0qYN+wfUGRDJIRKKa7VHfhmBHSORpGQMewQI9dcTwnOBw5Nki9EzGS+Hnyl2KM0Pb0WOByczQnMNteL+cJOxywJUlyj0vOUlQFurXmsap5uuvpc64wmkhZTHt0MJcjh3zE8cslezUBPagX9BgwkSmcxa5DqPbIxh+XeEBrDmd9ZN1bVWGcZijSuulqg+eV3Q/y3GcX19ystWTMNpFMeStCCEluV31zv25CoKS0YfEc0jYaEzrSAgemQFEJxPAaeT6Az9oT+peF/sGVWTHZJuflg+GAXtI+mevpetQCarYG5G13fJWcRl2C8Q5LxnGezjOCO7G5vfRhlQzizHE4H1rWLhr5uPrf/m8/6bbPBGg1MFSxCh0YWPmU9yNl1JLKM5nEJiqVVVdb+KykNVXURuGd5dXbvvAzKwQjObLAT3H8d3B/cC1wojxtRMivh2eHSBJRwAWBpGeCeuKBI/BDi8PBZVZYLj3tYeRKors5G5y1kMPIw42rJHfszyCeST6baqIc9G6VB8fBpnbSfQFKuGPiicutDOOvyVqDA/RW1RRhhwfBWVa3osw1dzuDfufkHnduRoZO3vwp3x5lgF4KmmQLo2ALc7iCKFB0fLAvHv7UJw4BhmkYyBRtjcr0XPsuBhWEUmqY0BxuA0Afh7gd6L3cQjKs8cheU1Hz4f7FUnITnW97KYwj1lqDHLj/lic0/8PpHhWjV/PEYqB5E6EBgUqHQDRICXEkegOpVd9/9YPOjQn/wsHxQGU+MxpaJXJCHgNh84EhGDghuj0xTnjoYVvDKHN6U0Xjl4YqimaAoltsFbVWQi5RnXCsHf80mxhTcpbKEJwmIut+q9EIc8GC9tZqWwQGoWsoSbc0ouO9LY69+hLBdv2s2//LJY1BD6L0H/3uYwJmaSH0XlIVDcLy17HTL9VMLBVBJqbR3vDY7Nvz63AomuYjB+2OaCCFAs4mQHMMB09EWgNjWZIsMRuDEN+8x8NaDHXgcmad78GQ8qDOTKWgji2ufqegVOzt/95PBaDjYeXC3HNyrAsmUFpJ53jOjhTkvE1JrH3ph3FcXCFuM+i664GNISTYGozv94Ops59zqiVI3Bjsu+POUcZXyWu7CmD6HjbuExGFzawe8VQAieobRsvEq9Q5r6U5azwrIEIzglKJWEZwDeEJ8drAhm7aikHD4j9JJa6lIuN6AoXarV2oWQvRiry6W4OQ69nxLysIV6LAfvUr43n4POlklfH8P0f9poId+kBtPoFBJIcmHBCLS/AqSTQ2++VJh8pzJrUsKqphRxNb5ACNYLRDIGXmeMMkwR5SzFLQdMZAeGYzIIXOcCoXZJCRAMALkEREtuKYp4qgiIc8hgyICrIeCKjsGwDN0VFo4m/HUND/94ghtz42531ZGMWJwqOBRoW5JeQzraTLY/FtY4AzyW5ZfbcG07Gja8wGrTRUUTFsR5reYsuIIzQBOKlAPXUdDA7jVE3zM7KC+6jIe14xnx077vpBQDwDn0cGBw3pyA5EMM64nL9y8hqFSHz47xYANR2NrEU7bm6OHEtICCemtA+bp8IlzQHA0SwQcoo/A6bUycqF9CK55CUnMTvggWP0Sw8yW+Jg9e6ywbyhQVMz2liblecpnqJ+xleAuGlznBC40DU2S9n3FT8NdVf64AcnkgavEWlniCsE2olpocVYoPsmXSemD2jPvFDr4VvC8v8VLcI0dslyBQaGcZnd4Xi4HgJyiqZCdHF7Knq7gpZGxoo8p6/t71awV/RQDo437Oza8FT3RObUBxFBuJjXTNqQmHcxnImvLGSQ8z0HTSRsqQbvqlr6QrVjWxL4Uas/oEupIE/1kQ2Fl60Rt3amEBIg2Bz+FNMiqOe4V2tQcUyF1xsEv1IBIRtItJpzIhFXE/2SUtFOPmJFqbQ0FlagyD++WZ683du6ce4kMIqrSAF9v3g0wxX5duXuhVLHYu4KCy4MQpSAgQS0qpdUAzmHd6Rl31a6+t9O6jBcJzYewLi9V/HrKU0xljGFHZU32YYx48/TSjOVmKUrlrRhD9SCMEHzolfEZ7Iw1l5rswxgx5qlXznQOjq8ui6uX5d3K3oDeDJOmbYl87LFbpxuWX7rc3OYeetxZ1nIf1/UTJRnT9IpKTkNIDDFXOR6SLwl8H7q+JLXrvH3fzqK6+n/dWKGjEc+XVg/m+ty3+UdPbooWYCgHsddB7PUgxlncApBwz8sDXJRndZ3tWch+lrZQJFx/vCwJjftu9BtbXWTYiwx7kHKJXNZygJQ9SC1ni5wfEIZyfT9NlQWpSf/CRenWjwIsWvjQ2yuAfR72khftxoIQbPAuUJJxSiHNrUuzBsgTqEzBm9xfLmTKcmzaaZsYzhvvvNwKG61/IXOnlWnaHbGxMELdE1SKSb0QYW1CzTAy3I34/lGxOgtKmL2neCdWroSEw7fZPldbpw0BUTcuZNTvRBP75PFWpwNPPP8ESUdGAX7FIjhLQ3iXX4fUquFr0sM8zTsYJL3kQB9BaWDnB3WDuwKIzF3gssW74ImfvDIqhXq5C1tfdQ0N+gKmqrD492qLCbdvJgzpKlkRGc24xjSizzCUuYBZpkavPNvP24P1glAIZUfYXr9NfM/BO4DIB6gOQJkMwEtoaJrjNPABsBNGtlFOt4Q5tjTmmPn8p1ZG9tRLyE6OpIjaYFmTfRgTLDuo3qAJnImkmVU+LFscZDFp97/wriOKyQnPWQdxsSQMy7vjFlD7tsPWpBtI41Zi7gWZPP6CctzvPG7HMk0ussF1IM5s4kOaMWs6Nd0z5x+DO4GQeWw5GoygF03K0QMd+1Dvyj4UwkpX9jyLz2at2vC+Qfb8QYxM1yWE854Yiq3ekUvxrXNXC0jT6kHF9fJnERSLCVpwzeKJrxZcHbeJGUaumnYXBHnNk/zKWlLT4B1rB1WT3rXpDJOBkE/Uqwgem8vu+sdeFhNgQ249y7wLHVNXLC6Ez5a+Q1fnZX01tBAFQV3zfCZmimS0UG7Ix+Li+2V1yw+8I3CcozsXkwuXlhhvTnc33Vn1LE6Li46QVQtasZ7utF1R7k1CO6I/+x877YMXCzOPZHkAOv7CPe0D5UKa4V54qngwdpGeVR4oD9NMfuz/IPfZvDDpR43YCMYvMVInel7d8TJwF7u3GnvsYtHNrIafnALM9jhI9y7OcPZ6kJ73OYwNy7IzQ3vyuiZ72muwp47F9qH2n7fODp5d7onNPvH5h4cW/9Ar355TqyB57jsf2d7zm18JsLwzTfVN7oYUszy+Q0zd7uwAn+SQM1p70DS4O5UtyhOMnpmX459kemoDtPfzAY11u8YYcldnCXH96ximexbsZQnVYt3ZHXHSPeGG9lBH0sU1LQ7ydNwp+2rSLZp4J6SZbZ4ywjM6qa/mZznXjicc0zil1i8n4wCSmStW0ipOl49e9rLshQkT19Drm7rHN6vRT415Lailvbl5q4yZ5FeVdYfqbnrnnC7K9z3HoaYtRHknjW8maalSo4+D0cv2Ou+k8i8HMHPGcmowuihH1TCIBSSIQ6Qgo+8Jst0I650Q4ym+OVJfXSGFvyIGEp9cj9ZNXpxphTRfHBrkEu+u/LU3DI9aOUfeNVrCw7rsba/1trch2bN/Smmu24OUygm7HRzg1zp5Czi3yrJzI03w+pJqUXS7L14N6EJh9zpvRcTiOjdhD1mdFyNQotMZSib/9vIqqi9f/z/WMyv+7dV4Z4NODb6aY0Rq7OUBYzx4J60EZa6bPevab7XBuyc7ksy6gzJUDwJVpplV3aFqXhhyoyyz3BUSPt8SZdArJJ3MwtaekXDDE7dKWf/2bxYaLUeLM0OBBBOFyr5Lzn1qVZNIeHdXWVcaYBbSlpN/zCJQLnzZb/qs+TE0eLGMPi9WQT5dQj5dBdlfQrx1yst24vDsXd7i0Zo3P8uegw1Tc41T8w3hASBTthBIuQqbzU3P+j0rS5S/y9kc52ADka7vZhGId/4FHPrHG6Ph5ujOw5fl681q+YtYEQ5Gi3co3v9kZ5sUeoj/HnxMzTUXlQ+hd1lVZ+ftWxXdtwTxLWHww+gtU6XxDT4oVgjBlxBmwN8dD43NhlTxyBjpbiAzOHuezmvOJZtfCxk3vDBRzLwfYnh4CExFtGBDJI1koqbiGl8ghUHxxym1a+7Cmg4ww4XA3frCbkhiMSQ8GWIEz4f40zW0JXxIRAxtcoaUkUDMnea6X2taLy4ZCvbg4u3ByH3L2H94vrM12t4afbk9eLjXvIH85tof1/68trE2WvvL2sO1z9aO1r5ai9b+uva3tb+v/WPzT5tPNg82D2voT95o+vxhrfPZ/Ppf+iJugQ==</latexit>

to give approximate answers. Template-based synthesis

Probabilistic Programs
Programs withrandom assignment

Qualitative questions
Pr(ReachC) =? 1 (almost sure reachability)
Pr(ReachC) >=? α (threshold reachability)

x := Gaussian(0, 0.2)

probabilistic branching

Quantitative questions
Pr(ReachC) >= ?? (lowerbound, “verification”)

if prob(0.2)

Pr(ReachC) <= ?? (upperbound, “refutation”)
Exp(StepsToReach ), upperbound, lowerbound, …
• ⼀般の時相論理式仕様の検証は“Concentration”
Find B s.t. (x > B ➜ Pr(StepsToReach > x) < ae )到達可能性に帰着可能．
C[Chaterjee+, POPL’16]

C[Baier & Katoen 2008, Chap. 10]

X-bx

Hasuo (NII, Tokyo)(also nondet. assignment& branching)

1 x := m
2 while x > 0 do
3i f prob(p) do
4
x := x 1
5else
6x := x + 1
7
fi
8 od
(say, m = 16 and p = 0.2)
<latexit sha1_base64="JaB/5Fey3F2sEw+FzLG75bYBN20=">AAAuIHiczVrdc9zGkadyl4u9l7vYucd7Gd9SFUrG0lyqfJeyQpbMlWirTFM0SctKCIoeALO7YwIYaGZAcgPhn8nfkoe8Xd3j3V9z3QPsApjB2s7HQ7aKXPT0b3o+uqc/ZhFkMVd6Z+d/7/3kH/7xp//0s3feHfzzz//lX3/x3vu/fKlELkP2dShiIV8FVLGYp+xrzXXMXmWS0SSI2TfB9QT539wwqbhIz/UiY5cJnaV8ykOqoenqvT/6AZvxtEh4yjM6Y2UxfhQm5aBujpXGSfB0Vl6keRKApL2YTfXlYPPuk71kc3A75zEjm3f7O5skEgNC+JRs+pkUwVb2oG4iBMF3o/EmECxWrGn70LRN+UBEA5+lUXvAwZaiC49sJnvj/9wkNI3IZra3s727+aCCrqY8uHpvuLO9Yz7EfRjXD8ON+nNy9b731I9EmCcs1WFMlboY72T6sqBS8zAGiX6uWEbDaxB/AY8pTZi6LMx2l+Q+tERkKiT8pZqY1naPgiZKLZIAkAnVc2XzsLGPd5Hr6a8vC55muWZpWA00zWOiBUHdkYhLFup4AQ80lBzmSsI5lTTUoJfOKEyzO+hPzudckSRXmgSM6DmDrZZA1DAUDO2xoBGLBvBpi5jSNFwE4s6rV4PfIFV79Qq8gdIJlQsZebdULQDigaEFYFeJB/oXU+9OgSxWEjK4315ldMMz2MxMacnDa9XdbJbOQP/zyyKgAYu7PBrHl8XdogRxE5FkYHhfUpTBFBn4dwuRoUkXN7tliwpzecPaDbshi+N2gxSaaoScsRh29xwmV8AJKGDesH9AkS0xJVRKcasewDcjPCU0DIWMYIcYueV6TnA+oDRJvhQRk+nA/1qxT+P4/FbgcKCbM5htqpfzhZ2O2NSPcY1KL2JW+Li15rGseLru6nJbOppJms15eOdJkMN/z1Dlkr3JwU4qA/3W52kY5xGrkepXZGsBy70jNAKdw0lCVdYOoghEHJVdK9D8+vce/huFUfX9RktWTwPpmAcSrKDAVuU2V/vmETWnGYPvkMahR2iuBQxMPZIJxVEN5sD72BP6F4b/0bZZMdkjxWjf298D66Oxnv+qXALN1sDcja3vkYuQSzi8HkHHkOQJwR0Bh/FxmHigsxS0A+vaw4M+MJ/7f81ncN9ssMYDpjIWok8lS58y8FN2G4okAa9VgGFpVRZmp4NpYaiyi8A9S8uLR5eFXwzHoLPhrv/4rf94+Mi3oTyqRcmkgGeLS6dghEsAiwsf98QGheKHEMfHL8qinnFQHJeOBKrLi/FlAxmOHcykXHEn7gzSmeSzuTbm0Z6N0mB4+GRiRP3xJeWKgS8qtj8GXRebvgL3l1Unwgjzvc2yXNNnB7pcwL9L8w86NyNDJ2d/Fe6ONcEuBI9mDKDTFuB+B5HF6PhgWTj+5giGgYNpGskczhiTg154ngILIzk0zWkKZ6BIy9L3fqD3agfhcBUn9oKmFR/+X60MZ8rTbWflEcTdlqCnNj/m0zb/yOkfZqIx86cToHoQgQWBSQVC10gIcAXZB9MrH37w0ejXmf7oSbFfGk+Mhy0RqSBPADHatyQjBwQ3KtOUxxaGZbw0ypszGq1VrsjqCYpstV3QVvqpiHnCtbLwt2xmjoK9VDbl0ymIetyY9FIc8GC9lZkW/hGYGqZUrRn5j11p7M2PELbndk0WXz17CmYIvQ/gfw8TOHMTqR+CsXAIjpurTpu2n1oagJoWSjvqbbMjw6/0ljHJRQTeHzNVCAGazYTkGA6YDrcBxLZn22Q4Bic+esTAWw934XFsnh7Bk/Gg1kzmYI0sqnymojfs4vKD3wzH3nB3/2ExfFT6kiktJHO8Z0Izoy8TUisfemXcVxcIW4z2LrrgU0hJtobjB/3g8mL3stUTpW4Nd23wFzHjKuaV3OVh+gI27hoSh9H2LngrH0T0DKNl7VWqHdbSnrTOM8gQjOCYolURnAN4Qny2sAGbN6KQsPifxrPmpCJhewOG1q3eqDyA6MXeXK3A09vI8S0xC9agg370OuEHhz3o6TrhhweI/ksDPfSD3HgGtVIMST4kEKHmN5BsavDN1wqT50RuX1MwxYQitsoHGMFqgUDOyNMpkwxzRJnHYO2IgfTIYEQKmeNcKMwmIQGCESCPCGnGNY0RRxUJeAoZFBFweiiYsnUAeIKOSgtrM56b5udfnuDZs2Pud6UxjAgcKnhUqFtiHsF66gw2/Q4WmEN+y9KbbZhWO5r2fO5jKQcF03aI+S2mrDhCPYCVClRDV9HQADZ7go+ZHdRXXcbTivHi1Go/FBLqAeB8enRksZ7dQSTDjOvZKzuvYWjUxy/OMWCDatpWhNN25uighGyBhHTWAfO0+MRSEKhmhQAlugicXiMjFdqF4JpXkKnZCRcEq19hmNkSF3PQHivoGwoMFbO91ZFyPOULtM+oleAuG2znBC40DkyS9n3FT81dV/7YAcnkgevEtrLENYLbiHJpxUmm+CxdJaX7lWfezbT/neBpf4uT4JpzyFIFBwrl1LvD02I1AOQUdYVs5fBS9nQFL42MNX1MWd/fq2Kt6acYHNqov2PNW9MTnVMTQAxlZ1K5bkMq0sJ8LpKmnEHC8Rw0njWhEqyraukL2YoldeyLofYMr6GONNFP1hRWtlbU1p1KSIBoo/g5pEGtmuNRpk3NMRdSJxz8QgUIZSjtYsKKTFhF/E1GiTv1iBmpstZAUIkm8+RhcfF2a/fBpZPIIKIsDPDt6KGPKfbb0t4LpbLl3mUUXB6EKAUBCWpRKVsN4BwGVs+oa3bELFTrIlomNB/DupxU8Ru8Nizrgx0WFdmHMeLN02szlp2lKJU2YgzVgzBC8KFXxuewM625VGQfxogxT71y5gtwfFVZXL4uHpbtDejNMGnclMinDrtxukHxlc1N29xjh5snDfdpVT9RkjBNb6jkNIDEEHOVU498ReD72PYlcbvOO3TPWVhV/2/rU2hZxMvVqYfj+tI9858+u8sagKEsxEEHcdCDmCRRA0DC1pcDuCouqjrbOSGHSdxAkbD98aokNO67tm9stZFBLzLoQcoVclXLAVL2ILXMlzk/IAxl+34aqxakIt0LF6UbPwqwcOlD768B9nnYa541GwtCsMG5QJlOYgppblWa1UA+hcoUvMnj1ULmLMWm3aYJfxnApkd2hY2nfylzt5Fp2i2xkTBCbQ0qxaReimhtQsUwMuyN+P5RsTrzC5i9Y3hnrVwJCYvfZrtc3dI2BERdu5BxvxOdtjWPtzod+NTxT5B0JBTgNywEXRrCufw6pq0aviIdzPO0g0HSSQ70CZQG7fygarBXAJG5C1y1OBc80bM3xqTQLvdg68vuQYO+gClLLP6d2mLG2zcThrSNLAuNZdxiGtF3MJS5gFmlRm+cs582inWCUABlR9Bcv81cz8E7gNAFqA5AmQzASWhonOI08AGwM0Z2UE63hDltWcwpc/nPWxnZcychOzuRImyCZUX2YUyw7KB6gyZwZpImrfJh1WIhs1mz/5lzHZHNznjKOoirFWFYzh23gNq3GbYi7UAaNRJTJ8ik0ZeU436nUTOWabKRNa4DsWYTHdOEtaZT0T1z/jG4MwiZpy1HgxH0qk45eqATF+pc2QdCtNKVA+fEJ3ljNrxvkAN3ECPTdgnBoieGYqujcim+s+5qAWlaHai4Xf0sgmIxQfNvWTRzzYKr0yYxw8hV0faCIK95lt60llQ3OGrtoCrSuTbNMRkI+Ey9CeGxvuyufuxlEQE25NZ54lzomLpieSF8sfIdurwsqquhpSgI6pqnucgVSWim7JCPxcX3y+qWH3hHYDlHey4mFy5aYpw5PRzZs+pZnBZXHSHrFrRmPd1p26Lsm4RmRHf2P3baR6+WxzyUxRHY+Ctb20fKhtTDvXJM8WhiI51TeaQcTD35ifuD3OeLzKQfFWLLn7zGSD3Vi/KBk4Hb2IP12FMbi25mPfzsHGBtj4N07+IM56AH6Xif48iwWufM0I687pE97z2w59aJ7UMdvmycHTzb3LM2+8zlHx+3+MdO+faStgqSl67zkc09v/mVAMs701Td5G5JkafRA2LqdmsH+CyFnLG1B3WDvVPJsjzB6Jk4Of5ZoudtgHZ+PqCRbtYYQe5qLSGqfh3DdK8Fe11AtVh1tkecdTVc0w7qRNq4usVCnk86ZV9F2kUT74Q0s81zRnhCZ9XVfJ5ybXnCCY1i2vrlZOJDMnPDClpG8erRyV5WvTBh4hp6fVv1+HY9+rk5Xktqdd7svFVGTPKbsnWHam96R09XxYeO41DzBqIcTeObSVqq2NjjcPy6uc47K93LAcycsZwajq+Kcen5kYAE0UMKMvqeINuNsI6GGI/Nu2nm6gop/BXRl/hke7Ru8mJNK6DpUmmQS3yw9tfeIDhp5Jw412hTHlRlb3Ott7MDyV77p5T6ut2PqZyx+/4Rfg3Iu/hGXFF0bqQJXl9SLbJu9+WrAV0o7F7nrYhI3KYm7CGr82IESrQ6Q8nk3l7ehNXl69/HevLsz16Noxt0avBVqxGpiZMHTFDxVloJxlw1O6frsLEG557sRLLWHZShehBoMvWsqg5l/cKQHWVZy10h4fJbogx6jaSzPGjOMxJ2eOKtUta9/csDY+V44sxQIMFEoaLvkvOQtqpJJJy7q6QrDTBLaavJP2UhGBe+7Dd/Uf8Y6r9aRZ9X6yCfrSCfrYMcriDOOuV1M3F4di5vUbXmzc+iR7FBbK5xKr4hHABkyi0EUrbBJgvTs3rPqiXK3eVkgXNoA5Gu7mYRiHf+GSj9k62xNxo/ePK6eDsqV7+IZcFwvHyH4sPf7O6QTHv4b/8Taq65qHwCvYuyvLhs3qroviVYv7KL3jJWGt/gg2KFEHwJIQf+3sQzZzagiofmkO75MgHd83hRca7Z4lbIqOYFU8XM+yGGh0pgKqQZ85A0komai1t8gRQGxR+n1J65C6s7wAyXAveqCzuPRMIjfOphBE898xayR6bcIyKCNpkjZSQQc6c5cGvN1otLhoI9uHpvOLbfMnYfXu5uj3e2x1/tDp8c1G8gv7Px7xv/sbG1Md74r40nG59vnGx8vRHee3jv5N5v7/1u9IfRn0b/PfqfCvqTe3Wff9vofEb/9//2g5Rz</latexit>

Example: right (randomwalk)
Probabilistic
programs(without conditioning)
We disregard the Bayesian aspects

7

ソフトウェア科学の仕事：「構造をときほぐす」• 構造が複雑な検証問題から，構造が単純な制約充⾜問題・グラフ問題へ• ソルバに渡すまでが仕事• ポイント• 確率的検証でもスキームは同じ（「構造をときほぐす」）• 検証技法の発⾒は必要（ランク関数 ➜ ranking supermartingale，等）だが，束論・圏論のレベルではしばしば同⼀視できる（メタ数理的移転）• 現実的課題，理論的に豊穣（fixed point theory + martingale 集中不等式など）➜ 研究上やることがたくさん！

• （ついでに：制御理論もスキームは同じ）• ERATO MMSD の成果群：[Urabe+, LICSʼ17] [Takisaka+, ATVAʼ18] [Kura+, TACASʼ19] [Phalakarn+, CAVʼ20] 他

成果例１：
Probabilistic
Programs
確率的プログラムの
tail probability
検証[Kura, Urabe & Hasuo, TACASʼ19]Programs withrandom assignment• 対象： 確率的プログラム（右図）（状態遷移系としては無限状態 ➜ 直接グラフ解析による検証は不可）
x := Gaussian(0, 0.2)

• ⽬標：
probabilistic
stopping time の tail probability の guaranteed
upperbranchingbound
if prob(0.2)“100” は所与の(also nondet. assignment
deadline

1 x := m
2 while x > 0 do
3i f prob(p) do
4
x := x 1
5else
6x := x + 1
7
fi
8 od
(say, m = 16 and p = 0.2)
<latexit sha1_base64="JaB/5Fey3F2sEw+FzLG75bYBN20=">AAAuIHiczVrdc9zGkadyl4u9l7vYucd7Gd9SFUrG0lyqfJeyQpbMlWirTFM0SctKCIoeALO7YwIYaGZAcgPhn8nfkoe8Xd3j3V9z3QPsApjB2s7HQ7aKXPT0b3o+uqc/ZhFkMVd6Z+d/7/3kH/7xp//0s3feHfzzz//lX3/x3vu/fKlELkP2dShiIV8FVLGYp+xrzXXMXmWS0SSI2TfB9QT539wwqbhIz/UiY5cJnaV8ykOqoenqvT/6AZvxtEh4yjM6Y2UxfhQm5aBujpXGSfB0Vl6keRKApL2YTfXlYPPuk71kc3A75zEjm3f7O5skEgNC+JRs+pkUwVb2oG4iBMF3o/EmECxWrGn70LRN+UBEA5+lUXvAwZaiC49sJnvj/9wkNI3IZra3s727+aCCrqY8uHpvuLO9Yz7EfRjXD8ON+nNy9b731I9EmCcs1WFMlboY72T6sqBS8zAGiX6uWEbDaxB/AY8pTZi6LMx2l+Q+tERkKiT8pZqY1naPgiZKLZIAkAnVc2XzsLGPd5Hr6a8vC55muWZpWA00zWOiBUHdkYhLFup4AQ80lBzmSsI5lTTUoJfOKEyzO+hPzudckSRXmgSM6DmDrZZA1DAUDO2xoBGLBvBpi5jSNFwE4s6rV4PfIFV79Qq8gdIJlQsZebdULQDigaEFYFeJB/oXU+9OgSxWEjK4315ldMMz2MxMacnDa9XdbJbOQP/zyyKgAYu7PBrHl8XdogRxE5FkYHhfUpTBFBn4dwuRoUkXN7tliwpzecPaDbshi+N2gxSaaoScsRh29xwmV8AJKGDesH9AkS0xJVRKcasewDcjPCU0DIWMYIcYueV6TnA+oDRJvhQRk+nA/1qxT+P4/FbgcKCbM5htqpfzhZ2O2NSPcY1KL2JW+Li15rGseLru6nJbOppJms15eOdJkMN/z1Dlkr3JwU4qA/3W52kY5xGrkepXZGsBy70jNAKdw0lCVdYOoghEHJVdK9D8+vce/huFUfX9RktWTwPpmAcSrKDAVuU2V/vmETWnGYPvkMahR2iuBQxMPZIJxVEN5sD72BP6F4b/0bZZMdkjxWjf298D66Oxnv+qXALN1sDcja3vkYuQSzi8HkHHkOQJwR0Bh/FxmHigsxS0A+vaw4M+MJ/7f81ncN9ssMYDpjIWok8lS58y8FN2G4okAa9VgGFpVRZmp4NpYaiyi8A9S8uLR5eFXwzHoLPhrv/4rf94+Mi3oTyqRcmkgGeLS6dghEsAiwsf98QGheKHEMfHL8qinnFQHJeOBKrLi/FlAxmOHcykXHEn7gzSmeSzuTbm0Z6N0mB4+GRiRP3xJeWKgS8qtj8GXRebvgL3l1Unwgjzvc2yXNNnB7pcwL9L8w86NyNDJ2d/Fe6ONcEuBI9mDKDTFuB+B5HF6PhgWTj+5giGgYNpGskczhiTg154ngILIzk0zWkKZ6BIy9L3fqD3agfhcBUn9oKmFR/+X60MZ8rTbWflEcTdlqCnNj/m0zb/yOkfZqIx86cToHoQgQWBSQVC10gIcAXZB9MrH37w0ejXmf7oSbFfGk+Mhy0RqSBPADHatyQjBwQ3KtOUxxaGZbw0ypszGq1VrsjqCYpstV3QVvqpiHnCtbLwt2xmjoK9VDbl0ymIetyY9FIc8GC9lZkW/hGYGqZUrRn5j11p7M2PELbndk0WXz17CmYIvQ/gfw8TOHMTqR+CsXAIjpurTpu2n1oagJoWSjvqbbMjw6/0ljHJRQTeHzNVCAGazYTkGA6YDrcBxLZn22Q4Bic+esTAWw934XFsnh7Bk/Gg1kzmYI0sqnymojfs4vKD3wzH3nB3/2ExfFT6kiktJHO8Z0Izoy8TUisfemXcVxcIW4z2LrrgU0hJtobjB/3g8mL3stUTpW4Nd23wFzHjKuaV3OVh+gI27hoSh9H2LngrH0T0DKNl7VWqHdbSnrTOM8gQjOCYolURnAN4Qny2sAGbN6KQsPifxrPmpCJhewOG1q3eqDyA6MXeXK3A09vI8S0xC9agg370OuEHhz3o6TrhhweI/ksDPfSD3HgGtVIMST4kEKHmN5BsavDN1wqT50RuX1MwxYQitsoHGMFqgUDOyNMpkwxzRJnHYO2IgfTIYEQKmeNcKMwmIQGCESCPCGnGNY0RRxUJeAoZFBFweiiYsnUAeIKOSgtrM56b5udfnuDZs2Pud6UxjAgcKnhUqFtiHsF66gw2/Q4WmEN+y9KbbZhWO5r2fO5jKQcF03aI+S2mrDhCPYCVClRDV9HQADZ7go+ZHdRXXcbTivHi1Go/FBLqAeB8enRksZ7dQSTDjOvZKzuvYWjUxy/OMWCDatpWhNN25uighGyBhHTWAfO0+MRSEKhmhQAlugicXiMjFdqF4JpXkKnZCRcEq19hmNkSF3PQHivoGwoMFbO91ZFyPOULtM+oleAuG2znBC40DkyS9n3FT81dV/7YAcnkgevEtrLENYLbiHJpxUmm+CxdJaX7lWfezbT/neBpf4uT4JpzyFIFBwrl1LvD02I1AOQUdYVs5fBS9nQFL42MNX1MWd/fq2Kt6acYHNqov2PNW9MTnVMTQAxlZ1K5bkMq0sJ8LpKmnEHC8Rw0njWhEqyraukL2YoldeyLofYMr6GONNFP1hRWtlbU1p1KSIBoo/g5pEGtmuNRpk3NMRdSJxz8QgUIZSjtYsKKTFhF/E1GiTv1iBmpstZAUIkm8+RhcfF2a/fBpZPIIKIsDPDt6KGPKfbb0t4LpbLl3mUUXB6EKAUBCWpRKVsN4BwGVs+oa3bELFTrIlomNB/DupxU8Ru8Nizrgx0WFdmHMeLN02szlp2lKJU2YgzVgzBC8KFXxuewM625VGQfxogxT71y5gtwfFVZXL4uHpbtDejNMGnclMinDrtxukHxlc1N29xjh5snDfdpVT9RkjBNb6jkNIDEEHOVU498ReD72PYlcbvOO3TPWVhV/2/rU2hZxMvVqYfj+tI9858+u8sagKEsxEEHcdCDmCRRA0DC1pcDuCouqjrbOSGHSdxAkbD98aokNO67tm9stZFBLzLoQcoVclXLAVL2ILXMlzk/IAxl+34aqxakIt0LF6UbPwqwcOlD768B9nnYa541GwtCsMG5QJlOYgppblWa1UA+hcoUvMnj1ULmLMWm3aYJfxnApkd2hY2nfylzt5Fp2i2xkTBCbQ0qxaReimhtQsUwMuyN+P5RsTrzC5i9Y3hnrVwJCYvfZrtc3dI2BERdu5BxvxOdtjWPtzod+NTxT5B0JBTgNywEXRrCufw6pq0aviIdzPO0g0HSSQ70CZQG7fygarBXAJG5C1y1OBc80bM3xqTQLvdg68vuQYO+gClLLP6d2mLG2zcThrSNLAuNZdxiGtF3MJS5gFmlRm+cs582inWCUABlR9Bcv81cz8E7gNAFqA5AmQzASWhonOI08AGwM0Z2UE63hDltWcwpc/nPWxnZcychOzuRImyCZUX2YUyw7KB6gyZwZpImrfJh1WIhs1mz/5lzHZHNznjKOoirFWFYzh23gNq3GbYi7UAaNRJTJ8ik0ZeU436nUTOWabKRNa4DsWYTHdOEtaZT0T1z/jG4MwiZpy1HgxH0qk45eqATF+pc2QdCtNKVA+fEJ3ljNrxvkAN3ECPTdgnBoieGYqujcim+s+5qAWlaHai4Xf0sgmIxQfNvWTRzzYKr0yYxw8hV0faCIK95lt60llQ3OGrtoCrSuTbNMRkI+Ey9CeGxvuyufuxlEQE25NZ54lzomLpieSF8sfIdurwsqquhpSgI6pqnucgVSWim7JCPxcX3y+qWH3hHYDlHey4mFy5aYpw5PRzZs+pZnBZXHSHrFrRmPd1p26Lsm4RmRHf2P3baR6+WxzyUxRHY+Ctb20fKhtTDvXJM8WhiI51TeaQcTD35ifuD3OeLzKQfFWLLn7zGSD3Vi/KBk4Hb2IP12FMbi25mPfzsHGBtj4N07+IM56AH6Xif48iwWufM0I687pE97z2w59aJ7UMdvmycHTzb3LM2+8zlHx+3+MdO+faStgqSl67zkc09v/mVAMs701Td5G5JkafRA2LqdmsH+CyFnLG1B3WDvVPJsjzB6Jk4Of5ZoudtgHZ+PqCRbtYYQe5qLSGqfh3DdK8Fe11AtVh1tkecdTVc0w7qRNq4usVCnk86ZV9F2kUT74Q0s81zRnhCZ9XVfJ5ybXnCCY1i2vrlZOJDMnPDClpG8erRyV5WvTBh4hp6fVv1+HY9+rk5Xktqdd7svFVGTPKbsnWHam96R09XxYeO41DzBqIcTeObSVqq2NjjcPy6uc47K93LAcycsZwajq+Kcen5kYAE0UMKMvqeINuNsI6GGI/Nu2nm6gop/BXRl/hke7Ru8mJNK6DpUmmQS3yw9tfeIDhp5Jw412hTHlRlb3Ott7MDyV77p5T6ut2PqZyx+/4Rfg3Iu/hGXFF0bqQJXl9SLbJu9+WrAV0o7F7nrYhI3KYm7CGr82IESrQ6Q8nk3l7ehNXl69/HevLsz16Noxt0avBVqxGpiZMHTFDxVloJxlw1O6frsLEG557sRLLWHZShehBoMvWsqg5l/cKQHWVZy10h4fJbogx6jaSzPGjOMxJ2eOKtUta9/csDY+V44sxQIMFEoaLvkvOQtqpJJJy7q6QrDTBLaavJP2UhGBe+7Dd/Uf8Y6r9aRZ9X6yCfrSCfrYMcriDOOuV1M3F4di5vUbXmzc+iR7FBbK5xKr4hHABkyi0EUrbBJgvTs3rPqiXK3eVkgXNoA5Gu7mYRiHf+GSj9k62xNxo/ePK6eDsqV7+IZcFwvHyH4sPf7O6QTHv4b/8Taq65qHwCvYuyvLhs3qroviVYv7KL3jJWGt/gg2KFEHwJIQf+3sQzZzagiofmkO75MgHd83hRca7Z4lbIqOYFU8XM+yGGh0pgKqQZ85A0komai1t8gRQGxR+n1J65C6s7wAyXAveqCzuPRMIjfOphBE898xayR6bcIyKCNpkjZSQQc6c5cGvN1otLhoI9uHpvOLbfMnYfXu5uj3e2x1/tDp8c1G8gv7Px7xv/sbG1Md74r40nG59vnGx8vRHee3jv5N5v7/1u9IfRn0b/PfqfCvqTe3Wff9vofEb/9//2g5Rz</latexit>& branching)

Example: right (random walk)• 既存⼿法 [Chakarov & Sankaranarayanan, CAVʼ13]等： We disregard the Bayesian aspects
ranking supermartingale （〜 ランク関数の確率版） ＋ Markov 集中不等式• 提案⼿法：observations, conditioning, priors/posteriors, etc.
See e.g. [Gordon+, FOSE’14])• （平均＝1次モーメントだけでなく）⾼次モーメントを bound する ranking supermartingale• ⾼次 Markov 集中不等式

による bound の改善

X

Hasuo (NII, Tokyo)

9成果例１：
確率的プログラムの tail probability 検証[Kura, Urabe & Hasuo, TACASʼ19]• 実験結果• 対象プログラム：
coupon collectorʼs problem• ⾚が真の tail probability（実⾏時間が d を超える確率）• k次モーメントまで考慮してsupermartingale を線形計画法で合成• k が上がるほど，bound が tight になる• 線形計画法なので，⾼次化に伴うコスト増⼤も許容可能

10成果例２： 確率的ゲームの効率的解法[Phalakarn, Takisaka, Haas & Hasuo, CAVʼ20]• 対象： 確率的ゲーム• オートマトン＋ controllerʼs angelic
nondeterminism+ adversaryʼs demonic
nondeterminism+ probabilistic branching• ”2.5-player game”• 多くの意思決定シナリオのモデル• （ここでは）有限状態に限る• 勝利条件：
特定のポジションに到達（右図では “goal”）• ⽬標： 最適戦略の合成，およびその場合のスコアの計算
maxσ: Ctrlʼs str. minτ: Advʼs str. Pr(σ, τのもとで Goal に到達 )• 線形計画法で exact に解けるが計算量⼤• 既存⼿法1： Value iteration (VI) による近似解法 [Condon, I&C ʼ92]
➜ Bellman operator による Kleene 反復（右図）

Goal から 到達
可能性確率を逆伝播させていく11成果例２： 確率的ゲームの効率的解法[Phalakarn, Takisaka, Haas & Hasuo, CAVʼ20]• VIの問題点： 真の解にどれだけ⾁薄できているか不明• 既存⼿法2： Bounded Value iteration (BVI) による近似解法 [McMahan+, ICMLʼ05]等➜ 真の解の上界についても Bellman operator で Kleene 反復• BVIのチャレンジ： 上界の反復改良は最⼤不動点に収束．
到達可能性確率（最⼩不動点）とは⼀致しないことがある• より具体的に：ゲームにループがあると，上界の反復改良が⾃家撞着，
⾼⽌まりして下がらない• 既存⼿法での解決法：
ゲームにおける「ループ」をグラフアルゴリズムで発⾒して「つぶす」 [Kelmendi+, CAVʼ18]➜ 計算コスト⼤12成果例２： 確率的ゲームの効率的解法[Phalakarn, Takisaka, Haas & Hasuo, CAVʼ20]• 提案⼿法：Bellman operator による局所伝播に，「ラフな⼤域伝播」を組み合わせる• 下界については，地道に．
Bellman update による局所伝播を
Kleene 反復• 上界については，局所伝播はループにつかまるので，もともとのゲームを抽象化した
重み付きグラフを適切に構成して，そこで widest path problem を解く

13

成果例２： 確率的ゲームの効率的解法[Phalakarn, Takisaka, Haas & Hasuo, CAVʼ20]• 実験結果• ループをつ
ぶす既存⼿
法に対して
数倍〜数千
倍の⾼速化

14

成果例２： 確率的ゲームの効率的解法[Phalakarn, Takisaka, Haas & Hasuo, CAVʼ20]（うまく広報と連携しました．
滝坂さんありがとうございました）15成果例２： 確率的ゲームの効率的解法[Phalakarn, Takisaka, Haas & Hasuo, CAVʼ20]• 提案⼿法（再掲）： 上界については，局所伝播はループにつかまるので，もともとのゲームを抽象化した重み付きグラフを適切に構成して，そこで widest path problem を解く

Lattice-Theoretic Foundation

L: complete lattice, f : L ! L monotone• 教訓１：
Thm. (Knaster-Tarski)
不動点理論の• µf =
威⼒
min{l 2 L | f (l) v l}f (l) v l=) f (?) v µf (8↵ 2 Ord)
（CSの基本！）=)• 教訓２：

Thm. (Cousot-Cousot)? v f (?) v · · · v f ! (?) v · · ·stabilizes, and converges to µf↵µf v l• ⌫f =
max{l 2 L | l v f (l)}=)

l v f (l)l v ⌫f> w f (>) w · · · w f ! (>) w · · ·stabilizes, and converges to ⌫f=)↵⌫f v f (>)(8↵ 2 Ord)

Hasuo (Tokyo)「⼤域解を局所反復で求める」が
CS の基本戦略だが，時々「ラフな⼤域解を直接求める」
が有効！
16

Outline

Messages:• 確率的検証でもスキームは同じ（構造を解きほぐして制約充⾜・最適化問題に帰着）• 特に，束論・圏論のレベルではしばしば同じになる• 線形計画法に落とせば勝ち• 現実的課題，理論的に豊穣 （不動点理論，集中不等式等）➜ 研究上やることがたくさんモデル

確率的モデル検査，確率的検証[Kura+, TACASʼ19] [Phalakarn et al., CAVʼ20] を例に実⾏時検証，モニタリング[Waga+, CAVʼ19] を例に

サーチベーステスト＋論理・離散的構造[Zhang+, CAVʼ19] を例に

⾃動運転システムの安全性検証[Kobayashi+, NFMʼ21] を例に（➜ 実応⽤
可能性）

不確かさの
種類

解析⼿法

モデル要
(whitebox)

known
unknowns

formalモデル不要

unknown
unknowns

formalblackbox
モデルのみ
要

unknown
unknowns

testing

部分的モデル要unknown
unknowns

formal17

（モデル検査＋連続量）の⼀般論
モデル検査： 物理情報システムへ
物理情報システムへの適用
一義的には，連続量が現れた時点でアウト
状態空間が無限になって，探索できない
例： ハイブリッド・オートマトン

ハイブリッド・オートマトンの例（オートマトン＋微分方程式）では，到達可能性が決定不能

from [Casau+, CDC’11]

確率的オートマトンならばOKMarkov chain, Markov decision process, …
到達可能性判定の代わりに，到達確率を計算する（線形計画法で解ける）
時間付きオートマトン timed automatonも OK
連続量の領域が，決まったテンプレート（region, zone）で記述できる
region, zone は有限個しかない
X

時間付きオートマトンと zone graphfrom [Daws+, FORMATS’06]• ➜確率的システム，
timed automatonの研究の勃興（特に欧州）• 物理情報システム，⼯業製品の品質保証にも有効• ただし，（連続量の有無に関わらず）モデル検査の物理
情報システムや⼯業製品への実適⽤
は，モデリングのコストがバカ⾼い…
航空宇宙くらいしか割に合わない？ 18

実⾏時検証，モニタリング• （参考）モデル検査• ⼊⼒： システムモデル M，仕様 φ• 出⼒： M の任意の実⾏トレース w が φを満たすか否か(∀𝑤 ∈ 𝐿 𝑀 . 𝑤 ⊨ 𝜙)

• 実⾏時検証，モニタリング• ⼊⼒： システムの実⾏トレース w，仕様 φ• 出⼒： w が φを満たすか否か (𝑤 ⊨ 𝜙)

• 簡単すぎてつまらない？ ➜ no!
• モデルが不要 ➜ 産業界の実プロセスですぐに利⽤可能• 現場では「⽬の⼦モニタリング」「ad-hoc ⾃動モニタリング」
が横⾏➜ ご利益がわかりやすい• ログはしばしば巨⼤（右図，MONAA は [Waga+, MT-CPSʼ18]）➜ パフォーマンスへの要求が⼤きい．
線形時間計算量・定数空間計算量が望ましい• Timed pattern matching は理論的にも challenging．
実⾏トレース： 連続時間スタンプ付きイベント列（右）仕様： 連続時間制約付き論理式／オートマトン（下）19状態空間が無限になって，探索できない

実⾏時検証，モニタリング
ERATO MMSD の成果群
例： ハイブリッド・オートマトン

ハイブリッド・オートマトンの例（オートマトン＋微分方程式）では，到達可能性が決定不能

確率的オートマトンならばOKMarkov chain, Markov decision process, …

到達可能性判定の代わりに，到達確率を計算する• Timed automaton 理論の応⽤として取り組む（線形計画法で解ける）• オートマトン＋連続量from [Casau+, CDC’11][Waga+, EMSOFTʼ18] [Andre+, ICECCSʼ18][Waga+, NFMʼ19] [Waga+, CAVʼ19][Waga, FORMATSʼ19] [Waga+, ICCPSʼ21] …

時間付きオートマトン timed automatonも OK
連続量の領域が，決まったテンプレート（region, zone）で記述できる
region, zone は有限個しかない
X

時間付きオートマトンと zone graphfrom [Daws+, FORMATS’06]• 産業界のニーズ： モニタリングの枠組みの flexibility••••

仕様にパラメータを含む
⽂字列等のデータを含む
Boolean に限らない「充⾜度合い」の定量的意味論…

• ⽅針： polyhedra による空間抽象化の限界を追求• Zone 抽象化，線形計画法で効率的操作• その範囲の中で枠組みの表現可能性・flexibility を上げていく• モデル検査が⾮決定的になる setting でも，モニタリングであれば実効的に動作20

実⾏時検証，モニタリング
成果例： パラメータ付き timed pattern matching[Andre+, ICECCSʼ18] [Waga+, NFMʼ19] [Waga+, CAVʼ19]（パラメータなし）
timed pattern matching• ⼊⼒：

パラメータ付き
timed pattern matching
• ⼊⼒：
•
•

• timed word w = (a, 0.12) (b, 1.28) …
• specification φ”no occurrence of c for 6 sec. after b”• 出⼒：• All intervals [t, tʼ] such thatwʼs restriction w|[t, tʼ] to it satisfies the
spec φ• By a laptop,~ 1M
events/sec

•

出⼒：
•

•

timed word w = (a, 0.12) (b, 1.28) …
パラメータ付き specification φ(p)”no occurrence of c for p sec. after b”
こういうしきい値を決めるのが現場では⼤変…

All triples {p0, t, tʼ} such thatwʼs restriction w|[t, tʼ] to the interval [t, tʼ]satisfies the spec instance φ(p0)By a laptop,~ 10K
events/sec

21

実⾏時検証，モニタリング
研究の展開と展望• オートマトン理論の応⽤先として豊穣• 実⽤ニーズ⼤（企業との共同研究）• モデル不要 ➜ すぐにご利益が出る• モデル検査が undeciable でも，モニタリングはしばしば実効的に動作• 展開１： 部分モデルの活⽤ [Waga, Andre, Hasuo, ICCPSʼ21]• 離散サンプルの補間は根源的課題（下左）• ”bounding model” （下右） を⽤いてあり得る補間を制限 ➜ false positive を削減• 展開２： 形式仕様記述⽀援• システムモデルは不要．しかし，形式仕様記述はそれでもむずかしい（ユーザーは論理・オートマトンに習熟しているとは限らない）• 形式仕様記述の対話的⽀援ツールを作成中
22

Outline

Messages:• オートマトン理論の応⽤先としてのモニタリング• 産業上のニーズも⼤• Polyhedra 抽象（←線形計画法）で連続時間・データもさばける• 形式仕様記述がやはり実⽤の壁モデル

確率的モデル検査，確率的検証[Kura+, TACASʼ19] [Phalakarn et al., CAVʼ20] を例に実⾏時検証，モニタリング[Waga+, CAVʼ19] を例に

サーチベーステスト＋論理・離散的構造[Zhang+, CAVʼ19] を例に

⾃動運転システムの安全性検証[Kobayashi+, NFMʼ21] を例に（➜ 実応⽤
可能性）

不確かさの
種類

解析⼿法

モデル要
(whitebox)

known
unknowns

formalモデル不要

unknown
unknowns

formalblackbox
モデルのみ
要

unknown
unknowns

testing

部分的モデル要unknown
unknowns

formal23

サーチベーステスト＋論理・離散的構造• サーチベーステスト：「危ない⼊⼒を探す」• システムはブラックボックス• 危ない出⼒から論理的に逆算，は不可• ⼊⼒を⾊々試して探すしかない➜ メタヒューリスティクス（進化計算，…），強化学習• Hybrid system falsification （反例⽣成） [Fainekos & Pappas, TCSʼ09]• 「危なさ」を論理式の形式仕様で定義• 定量的意味論で，論理式を最適化の⽬的関数に変換

24

Hybrid System Falsification• Hybrid-system falsification: logic-powered search-based testing• Goal:
nal u
-box)
g
k
i
c
s
a
t
l
u
b
↓(
find u such that the output M(u)↓ inpo de l Mmme
syst
violates the given logical specification• Enabling technology:
quantitative robust semantics➜ falsification by optimizationt signa
u
p
t
u
↓o
M(u)

l

[Fainekos & Pappas, TCS’09]

more robustly
true

??

true
false

input

Boolean semantics

This way toclimb down :)less soquantitativerobust semantics

input

Satisfy the given
logical specification, such as⇤(req ! ⌃[0,3] res) ??
25

Exploiting Logical Structures• In hybrid system falsification (and statistical ML in general),efficiency comes mainly from gradient descent (which is continuous)• Question: can we also exploit discrete structures for efficiency and explainability?
• Example: hierarchical optimization scheme [Zhang+, CAV’19]• Given: a black-box model M and a specification ⇤I ('1 _ '2 )<latexit sha1_base64="MmCJ43cd92+X1L3OT0Bd9Lf9u8w=">AAACB3icbVBLSwMxGMzWV62vVY+CBItQL2W3CHos9aK3CvYB3WXJptk2NJssSbZYSm9e/CtePCji1b/gzX9j2q6grQOBycw3JN+ECaNKO86XlVtZXVvfyG8WtrZ3dvfs/YOmEqnEpIEFE7IdIkUY5aShqWaknUiC4pCRVji4mvqtIZGKCn6nRwnxY9TjNKIYaSMF9rFXE/fBTckbIpn0aeB6JvFzqZwFdtEpOzPAZeJmpAgy1AP70+sKnMaEa8yQUh3XSbQ/RlJTzMik4KWKJAgPUI90DOUoJsofz/aYwFOjdGEkpDlcw5n6OzFGsVKjODSTMdJ9tehNxf+8TqqjS39MeZJqwvH8oShlUAs4LQV2qSRYs5EhCEtq/gpxH0mEtamuYEpwF1deJs1K2XXK7u15sVrL6siDI3ACSsAFF6AKrkEdNAAGD+AJvIBX69F6tt6s9/lozsoyh+APrI9vSB+Y6w==</latexit>• Goal: input u s.t. M(u) violates the spec

26

サーチベーステスト＋論理・離散的構造研究の展開と展望• 「論理構造＋数値最適化・メタヒューリスティクス」
はまだまだ掘れるテーマ• [Sato+, ADHSʼ21]:
制約付き最適化で論理積を解釈，
危険発⾒確率を⼤きく向上• 「統計AI＋論理AI」にも近い• モデル推定との組み合わせ[Waga, HSCCʼ20] [Shijubo+, PPLʼ21] [Okudono+, AAAIʼ20] [Gutierrez+, GECCOʼ20]• ⼊⼒を試しながら，モデルをだんだん
ホワイトボックス化• 近似モデルでモデル検査することで反例⼊⼒を推定• 産業応⽤が容易（トヨタ，Volvo，Airbus などから適⽤報告）27

system

少し脱線：
Logical Confinement of Uncertainties• Need to cope with uncertainties• Physical environment(rich interface)• Numeric optimization• Data-driven decision making,statistical reasoning

subsystemcomponent

modulesubsystemcomponent

uncertaintiescomponent

uncertmoduleainties• A related big challenge:
reconsilinglogical and statistical reasoning• Obj.-level stat. reasoning:
NNs in CPS• Meta-level stat. reasoning:
testing• Meta-level logical reasoning:safety arguments and proofs
28

Logical Confinement of Uncertainties

29

Logical Confinement of Uncertainties
Towards safe AI and XAI…
•

A common approach:examine the internal
working of AI

•

Here:
safety envelope,
logical confinement30

Logical Confinement of Uncertainties

31

Outline

Messages:• 論理を使った賢いバグ探し• ニーズ⼤，実適⽤容易．わかりやすいご利益• 論理と数値最適化の組み合わせ．階層的最適化フレームワーク• 「不確かさの論理的封じ込め」とも関連

モデル

確率的モデル検査，確率的検証[Kura+, TACASʼ19] [Phalakarn et al., CAVʼ20] を例に実⾏時検証，モニタリング[Waga+, CAVʼ19] を例に

サーチベーステスト＋論理・離散的構造[Zhang+, CAVʼ19] を例に

⾃動運転システムの安全性検証[Kobayashi+, NFMʼ21] を例に（➜ 実応⽤
可能性）

不確かさの
種類

解析⼿法

モデル要
(whitebox)

known
unknowns

formalモデル不要

unknown
unknowns

formalblackbox
モデルのみ
要

unknown
unknowns

testing

部分的モデル要unknown
unknowns

formal32

⾃動運転研究の地平
ERATO MMSD は学際研究の牽引役と，わかりやすいキーアプリのため，⾃動運転研究に戦略的集中••••

sip-adas•••

実動作する⾃動運転⾞を作ることがが⽬標
製品に直結 ➜ 各社が競争⾛⾏時に動作するハードウェア・
ソフトウェアを開発

⾃動運転ベンチャーのほとんど．
Waymo, Tesla, pony.ai, plus.ai,
Oxbotica, Tier IV, …
名⼤の取り組みもこちらに重点

⾃動運転研究••⾃動運転シス

地図インフラテムの構築

交通インフラ••「⾛⾏XXマイルあたり事故１件」「この交差点では⼣刻必ず事故が起きる」を排除できない与えられた⾃動運転⾞の安全性保証が⽬標（⾃分で作る必要はない）
製品に直結しないが，製品を売る上で必須 ➜ ⾃動⾞業界（＋政府，保険業界，…）の包括的取り組み
多くの企業が採⽤することで⼿法への信頼性アップ．
よって競争領域になりにくい
製品設計時に⽤いるソフトウェア・システムを開発•••

⾃動運転シス
HMI

統計データによる安全性保証••テムの 安全性・信頼性

テストによる
安全性保証

www.pegasusprojekt.de
L. Briand (Luxembourg)

RSS (Mobileye/Intel)
IEEE 2846
制御理論的研究(TU Munich など）

論理的論証による安全性保ERATO MMSD の取り組みの特徴• 安全性・信頼性を確かめる研究（⇔ ⾃動運転⾞を作る研究）• ⾃動運転安全性の論理的論証（最近の関⼼の⾼まり ➜ RSS, 国際規格，IEEE 2846 など） （⇔ 統計データ，テストによる保証）• ソフトウェア科学・数学・論理学に基づく，基礎的・⻑射程の研究• テストや実システム構築とも密接に協働（グループ２＠ Waterloo，産業界協働）➜ 応⽤への即応性も確保

証

UL 4600
autonomoose@ Waterloo(ERATO G2)
33

⾃動運転安全性の論理的論証• ?? 「モデル化不可能なので検証不能」と⾔ったはずでは…？
• ➜ 検証（＝証明）でなく論証．
”safety case” “safety argument”• 安全であることの論理的議論の積み上げ

情報システムの安全性と「不確かさ」
複雑な情報システム （例：⾃動運転⾞，1B LoC）

ソフトウェア科学における形式検証 formal verification

根本的な問い：• 安全に動作するか？
• 設計にミスはないか？
• 実装にバグはないか？

••

論理的記述の困難な情報システムの出現・普及
論理的記述 ＝ モデリング，数学的定義
例：• 物理情報システム：
物理的外界の完全な論理的記述は困難•

機械学習システム：
ノイジーなデータから数値最適化でルールを学習➜ ルールの論理的記述は困難• 設計者が duty of care を果たしていることの証拠• 事故の際には，論証を辿ることで原因の特定が容易に• 「テスト結果の解釈」とも考えられる

バグ不在・安全性を数学の定理として論理的に証明
前提：プログラムは⼈の⼿で⽣み出される論理的実体なので，その振る舞いを数学的に記述（定義）できる

不確かさを内包する
情報システムの安全性保証というチャレンジ•••

ソフトウェア科学の新パラダイム
テストの利⽤が不可避➜ 統計知と論理知の融合（AI 研究の⼀⼤課題）
我々のスローガン：（不確かさのもとでも）論理的⼿法が必要かつ有効• ⾃動運転安全性の基準・規格は五⾥霧中状態• ISO 26262/21448, UL 4600, IEEE 2846, …
• （2018年の事故以降 hype がしぼんだ⼤きな理由はこれ）• 論理的論証・議論に注⽬が集まっている．ルールベースの安全性解析
例： UL 4600, IEEE 2846, RSS (responsibility-sensitive safety)
34

2

Our Approach:Decompositional Proofs
with Open Assumptions• Goal:a decompositional formal proof for ADS
safety• Rigorous. Mathematical correctness• Uncertainties confined into
open assertions,which can be tested or monitored• Can be refined by further efforts

Technical element:
Event-B and Rodin• Formal modeling and verification
framework• Allows iterative refinement➜ suited for accommodating partial
proofs• A technical result for accommodating
uncertainties: [Kobayashi+, NFMʼ21]
Open assertions (unproved subgoals)➜ tested offline, or runtime-monotored
Safetysubgoal
2111(XX)
Safety subgoal
211

Safety subgoal
212

Safety subgoal
213

(XX)

proof/modelrefinement

Safety subgoal 21…

Safe in S1

Safetysubgoal2112

Safe in S1• Tree-style arguments are not rare…
but this one is formal
with mathematical correctness• Ongoing collaboration witha car company & Waterloo

Safety subgoal 1

(XX)

(XX)
Safety subgoal 2

Logical deduction,… mathematicallycorrect

ADS issafe in S1
35

Logical Confinement of Uncertainties
Safetysubgoal2111

Safetysubgoal2112(XX)
Safety subgoal
211

Safety subgoal
212

Safety subgoal213

as an instance of

(XX)

…

Safety subgoal 21

Safety subgoal 1

(XX)

(XX)
Safety subgoal 2

Logical deduction,… mathematicallycorrect

ADS issafe in S1

36

Outline

Messages:• ⾃動運転の安全性保証は未開の領域．社会受容には必須• 論理的論証，ルールベースの安全性保証への関⼼の⾼まり• Decompositional proofs with open assertions が論理的論証に対応• Event-B & Rodin によるモデルの逐次的詳細化が有効モデル

確率的モデル検査，確率的検証[Kura+, TACASʼ19] [Phalakarn et al., CAVʼ20] を例に実⾏時検証，モニタリング[Waga+, CAVʼ19] を例に

サーチベーステスト＋論理・離散的構造[Zhang+, CAVʼ19] を例に

⾃動運転システムの安全性検証[Kobayashi+, NFMʼ21] を例に（➜ 実応⽤
可能性）

不確かさの
種類

解析⼿法

モデル要
(whitebox)

known
unknowns

formalモデル不要

unknown
unknowns

formalblackbox
モデルのみ
要

unknown
unknowns

testing

部分的モデル要unknown
unknowns

formal37

まとめ：
不確かさに対応するソフトウェア科学• 不確かさのもとでのソフトウェア研究➜ 研究スコープの拡⼤が必要• 論理的理論・⼿法はそれでも有効かつ必要ソフトウェア
⼯学
テストと論理的証明の融合
Safe AI,
Explainable AI (XAI)

求ム 良い名前

統計的機械学習・AI

こういう「分野」ってなんと呼べばいいでしょ
うか．．．

モデル

確率的モデル検査，確率的検証[Kura+, TACASʼ19] [Phalakarn et al., CAVʼ20] を例に実⾏時検証，モニタリング[Waga+, CAVʼ19] を例に

サーチベーステスト＋論理・離散的構造[Zhang+, CAVʼ19] を例に

⾃動運転システムの安全性検証[Kobayashi+, NFMʼ21] を例に（➜ 実応⽤
可能性）

不確かさの
種類

解析⼿法

モデル要
(whitebox)

known
unknowns

formalモデル不要

unknown
unknowns

formalblackbox
モデルのみ
要

unknown
unknowns

testing

部分的モデル要unknown
unknowns

formal

不確かさに対応する
ソフトウェア科学
統計知と論理知の融合

連続ダイナミクスと離散ダイナミクスの
数学的統⼀

制御理論

（従来の）
ソフトウェア科学
ご清聴ありがとうございました．蓮尾 ⼀郎（国⽴情報学研究所, twitter @IchiroHasuo）• 関連する興味をお持ちの⽅，お声をおかけください．⼀緒にやりましょう！
• ⼤学院⽣（総研⼤）募集中．トピック・環境・経済的待遇などご相談ください．

38