Safety under
Statistical and Environmental
Uncertainties
Challenges in Cyber-Physical Systems with
Machine-Learning Components

Ichiro Hasuo
National Institute of Informatics & SOKENDAI
Research Director, ERATO MMSD

Outline
Cyber-physical systems under uncertainties
Formal methods and testing for CPS
Hybrid system falsification
Logical connectives [CAV’19]
Causality in time [EMSOFT’18]… as demonstration of combining
logical and statistical

Other topics
2

Hasuo (NII, Tokyo)

Uncertainties in
Cyber-Physical Systems 2020

Internal uncertainties:

Take automated driving…

never trust neural nets!

perception

object recognition

local planningbehavior planning

path tracking

path planningsensingl
ica
ys
ph lityrea

actuation

External uncertainties:
other traffic participants, weather,sunlight, comets, earthquakes, …

3

Hasuo (NII, Tokyo)

You walk in the dark,
guided by an apparatus

4

Hasuo (NII, Tokyo)

… which itself is a black box!

5

Hasuo (NII, Tokyo)

Never Trust Statistical AI
They approximate.
You never know when they are completely
preciseGround truth➜ noisy data➜ approximation
by regression

Approximating the sine curve by NN
https://i.stack.imgur.com/l8qjP.png
https://stackoverflow.com/questions/1565115/
unable-to-approximate-the-sine-function-using-aneural-network

Adversarial example
https://i.stack.imgur.com/l8qjP.png
https://stackoverflow.com/questions/1565115/
unable-to-approximate-the-sine-function-using-aneural-network

6

Hasuo (NII, Tokyo)

Never Trust Statistical AI
Question your “ground truth”

Ground truth➜ noisy data➜ approximation
by regression

Husky vs Wolf? Snow vs No Snow?
https://arxiv.org/pdf/1602.04938.pdf

7Hasuo (NII, Tokyo)

ML Component as“Super-Sharp but Not-Totally-Reliable Colleague”
Often super sharp“Wonderful idea! How did you get it?”… for no clear reason“It just came down to me…”

… and not always so“How come you made this stupid mistake?”

Great to have one in a team;
you don’t want all to be like that
8

Hasuo (NII, Tokyo)

ML Component in
Safety-Critical Cyber-Physical Systems
Take its opinion
with a pinch of salt

Safetyenvelope

Suggestion,
instead of decision
Extreme example:
proof check

System-levelassurance
9

Hasuo (NII, Tokyo)

Statistical AI vs Formal Deduction
A<latexit sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

Statistical AI
Allow noisy data

No guarantee

Correctnessof concl.

High

Scalability

Low
Decision making by “weights”

B

Formal Deduction
Errors in
input

Automatic pattern discovery from data

A
B

Explainability
10

Axioms are absolute

Logical guarantee(mathematical proofs)

Low
Manual preparation of axioms

High
Explicit deduction processes as proofs

Hasuo (NII, Tokyo)

Questions
Quality assurance of CPS
under internal (ML) and external (env.) uncertainties?
How to combine the two worlds?
statistical

logicalcontinuous

discretenoisy

rigorous

data-based

rule-based

bottom-up

top-down

11

Hasuo (NII, Tokyo)

Outline
Cyber-physical systems under uncertainties
Formal methods and testing for CPS
Hybrid system falsification
Logical connectives [CAV’19]
Causality in time [EMSOFT’18]… as demonstration of combining
logical and statistical

Other topics
12

Hasuo (NII, Tokyo)

Formal Methods
The general body ofmathematical techniques,originally in software science
Goals:
Verification
Input:a system model Ma specification 𝛗
Output: if M ⊨ 𝛗 or not
w/ a proof, if yes
w/ a counterexample,

Successes in software/
ICT* IC design (Intel, …)* device drivers (Microsoft)* light-weight FM(Facebook)* …

Synthesis
Input:
a specification 𝛗
Output: a system M
such that M ⊨ 𝛗or: a parameter ofa given (partial)
13

Specification
Expressing aproperty desired ina formal language
machinerepresentablebasis for verif. &synthesis

Hasuo

Verification by Theorem Proving
Example: program verification by Hoare logic
Proof search can be automatic or interactive(proof assistants like Coq, Agda, PVS, Isabelle, …)A mathematical proof guarantees correctness
Unlike testing (empirical guarantee)
Can cover infinitely many inputs/environments(in principle)
Write “let i be the input” in the proof!
program

Theorem forall_exists : (forall P : Set->Prop,(forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
intros P.
intros forall_x_not_Px.
unfold not.
intros exists_x_Px.
destruct exists_x_Px as [ witness proof_of_Pwitness].
pose (not_Pwitness := forall_x_not_Px witness).
unfold not in not_Pwitness.
pose (proof_of_False := not_Pwitness proof_of_Pwitness).
case proof_of_False.
Qed.

Proof
searchhoge

specificationk = N!
after
execution

proof
14

A Coq proof of ∀x. ¬P(x) → ¬ ∃x. P(x)Hasuo

Verification by Model Checking“Automated proof” by algorithms for automata
Proofs reduced to graph reachability
An automaton is finite ➜ “automated proofs” by enumeration
Example: Check if
we never reach 👿 under any input word

b

a

(*)

b
a,b

👿
a

a, b

15

(Wrong)Check the spec (*) for all input words(How many words? Infinite!!)(Correct)
Compute the reachable set(graph exploration, saturates within
finite time), and check if
👿 is not there

History of Formal Methods
Softwaregets bigger
network,
distributed,
concurrent
meetphysical
dynamics
rise ofstatistical ML

1970’s Initial studies on software quality assurance byformal methods (software verification).
Theorem proving, model checking
1990’s Software verification put to use, realistic tools
Theorem proving: Isabelle, Coq, PVS, …
model checking: SPIN, SMV/NuSMV, mCRL2, PRISM,
Uppaal, …
2006 Cyber-physical systems as a new application
domain.
Software verification + control theory
2016 Machine learning systems as a new application
domain.
Formal/logical deduction + statistical inference!16CPS Research, So Far(the V&V Aspect)
CPS(esp. hybrid systems)
Analysis⇤(p ) ⌃q)<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

FormalMethods

Col

Control
Theorylabo

x0 = f (x, u)<latexit sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit>
sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit>

rati
on

US and Europe have had systematic efforts
US: CPS Initiative of NSF (2006-)
Europe: Quantitative extension of formal methods (probability, time, …)
Need to catch up…?
➜ They haven’t necessarily been so successful in real-world applications

17

CPS Research, So Far(the V&V Aspect)
CPS(esp. hybrid systems)
Analysis⇤(p ) ⌃q)<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

FormalMethods

Col

Control
Theorylabo

x0 = f (x, u)<latexit sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit>
sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit>

rati
on

Problem: scalability, esp. for real-world CPSs
Require complete understanding of a white-box model
Insist on being absolutely sound and correct
Little tolerance to uncertainty and noise
Big problem too in presence of statistical machine learning18

Towards Formal Methods That Are
Down-Scalable
Many FM methods (esp. for verification) are
not down-scalable
They demand white-box models. Needformal models of all systemcomponents
They also require totally new design
processes

degree ofguarantee

Mathematical
proofs,strong guarantee➜ huge cost before getting non-zero
benefit (quality assurance)
Example applications to CPS:
airplanes (Airbus), space (NASA), …
Failure is so expensive➜ worth verification effots
Still takes decades

cost
Costly to constructwhite-box models

Integrating continuous dynamics is hard
➜ They focus on software
19

Towards Formal Methods That Are
Down-Scalable
For real-world applications(esp. automotive domain),
we need down-scalability

degree ofguarantee

Even if we can only afford
half the cost,degree of guarantee does not
become zero, but half

✘
✔
cost

20

Hasuo (NII, Tokyo)

Formal Methods: Spectrum
Formal methods
testing

Model Checking

lowWork withblack-box models

highAutomated Theorem
Proving

Interactive Theorem
Proving

Cost

high

Mandates white-box models
Automation

Automated

low(Expert) Laborintensive

low

Guarantees comprehensive?

high

low

Guarantees mathematically rigorous?

highempirical
guarantees

mathematical proofs ➜ “formal verification”!21

Towards Formal Methods That Are
Down-Scalable
Real-world applications(esp. automotive domain),need down-scalability

degree ofguarantee

Even if we can only afford
half the cost,degree of guarantee does not
become zero, but half✘✔

Our efforts at ERATO MMSD
cost

Combinetesting and formal verification.
Search-based testing
monitoring
contract-based verification
22

Hasuo (NII, Tokyo)

On ERATO MMSDJST ERATO Project, 2016/10-2022/03
https://group-mmm.org/eratommsd
Our goal:formal methods for cyber-physical systems (CPS)
Extend formal methods, from software to CPS
Safety, reliability, V&V (Verification & Validation).
“Check if a system behaves as expected”
Emphasizing industry collaboration, also forscientific inspirations
Automated driving as a strategic target domain.
Collaboration with U Waterloo:
www.autonomoose.net
Our team:
28 researchers, > 20 students (as of 2019/09)
International and scientifically diverse
23

Hasuo (NII, Tokyo)

Our Organization
International and multi-disciplinary. “creative chaos”
Kyoto U IS Site:
Advanced Deductive
Verification
Leader:Kohei Suenaga
Kyoto U RIMS Site:
Categorical
Infrastructure
Leader:Masahito Hasegawa

Group 0 @ NII:
Metatheoretical Integration
Leader: Shin-ya Katsumata
Topics:Programming
Languages,
Formal Semantics,
Categorical Models,Mathematical
Logic, …

Group 3 @ NII:
Formal Methods andIntelligence
Leader: Fuyuki Ishikawa
Subleader: Paolo Arcaini
Topics:SoftwareEngineering,Formal Modeling,
Testing, Safe &Explainable AI

Kyushu U Site:
Optimization for
CPS V&V
Leader:Hayato Waki

Group 2 @ U Waterloo:
Formal Methods in Industry
Leader: Krzysztof Czarnecki

Osaka U Site:
Control Theory for
CPS
Leader:Toshimitsu Ushio

Group 1 @ NII:
Heterogeneous Formal Methods
Leader: Ichiro Hasuo
Subleader: Masako Kishida
Topics:Automata Theory,
Control Theory,
Formal Verification,
Proof Assistants,
Automated
Deduction,
Runtime Verification

Topics:Automated
Driving, Software
Engineering,
Machine Learning

Hasuo (NII, Tokyo)

Interdisciplinary Efforts towards CPS:
Six Scientific Fields
application

Cyber-Physical Systems(esp. Automated Driving)F

Statistical ML & AI

Software Science
Formal Methods

D

BE

Control
Theoryfoundation

SoftwareEngineeringC(Meta-)Theoretical
Foundation
25

A• Four academic fields (B,C,D,E)
closely collaborating,• driven by clear application goals(F), and• backed up by mathematicalfoundation (A)Our
TechniquesinaSpectrumtesting

Search-based testing(aka hybrid system falsification)

Fault localization, stability analysis- “Which part of the system is-- Active search for counterexamples- Incompletely but eﬃciently,
A Component-Based Simplex Architecture forresponsible for this failure?”[Zhang+, ICECCS’19] [Lee+, GECCO’19]

by reinforcement learning

High-Assurance Cyber-Physical
Systems
CAV’19] [Zhang+, EMSOFT’18]- [Zhang+,

Dung Phan⇤ , Junxing Yang⇤ , Matthew Clark† , Radu Grosu‡ , John Schierman§ , Scott Smolka⇤ and Scott Stoller⇤⇤ Department of Computer Science
Stony Brook University, Stony Brook, NY, USA† Air Force Research Laboratory, Dayton, OH, USA‡ Department of Computer Science
Vienna University of Technology, Vienna, Austria§ Barron Associates Inc., Charlottesville, VA, USA

Monitoring, runtime verification-[Waga+, CAV’19] [Waga+, EMSOFT’19]

Quantitative verification

arXiv:1704.04759v1 [cs.SY] 16 Apr 2017

- “Warn me when something is wrong”- “Extract interesting parts out of this 10 GB log”
- Pattern matching via timed automata

As such, verification,
Simplex is a very powerful architecture.
It assures
Contract-based
safetyarchitecturethat the plant is properly controlled even if the advanced con-

Abstract—We present Component-Based Simplex Architecture(CBSA), a new framework for assuring the runtime safety ofcomponent-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based
CPSs to run advanced, uncertified controllers while still providing
runtime assurance that A-G contracts and global properties are
satisfied. In CBSA, multiple Simplex instances, which can becomposed in a nested, serial or parallel manner, coordinate toassure system-wide properties.
Combining A-G reasoning and the Simplex architecture is achallenging problem that yields significant benefits. By utilizing
A-G contracts, we are able to compositionally determine theswitching logic for CBSAs, thereby alleviating the state explosion
encountered by other approaches. Another benefit is that we
can use A-G proof rules to decompose the proof of system-widesafety assurance into sub-proofs corresponding to the componentbased structure of the system architecture. We also introduce thenotion of coordinated switching between Simplex instances, a key
component of our compositional approach to reasoning about
CBSA switching logic.
We illustrate our framework with a component-based control
system for a ground rover. We formally prove that the CBSA for
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides witha stationary obstacle). We also consider a CBSA for the roverthat guarantees mission completion: all target destinations visited
within a prescribed amount of time.
Index Terms—Simplex architecture; Assume-guarantee reasoning; Component-based system architecture; Cyber-physicalsystems; Collision avoidance- Formal verification in presence of black-box models- Failover strategy + switching, monitoring- Incremental modeling by Event-B, fuzzy logic, …

- “Termination probability for this probabilistic-

program?” “How long will it take?”
Automated analysis by martingale synthesis[Takisaka+, ATVA’18] [Kura+, TACAS’19]

Phan
et al.,and
ACSD’17
Fig. 1. The Simplex architecture. The Decision
ModuleBaseline
Controller are pre-certified.

The Simplex architecture was developed 20 years ago. Since
then, control systems have evolved to take on a more complex
structure consisting of multiple controllers, each with a distinct
functionality. For example, an autonomous vehicle might havea hierarchical control system consisting of controllers for (inorder of decreasing level of abstraction) mission-planning,
guidance, navigation, and inner-loop control. A system ofthis form is illustrated in Fig. 2. Furthermore, some of thesecontrollers themselves may have a hierarchical or nested
structure.
Advanced control systems are not necessarily hierarchical,
but are better understood as having a component-based architecture. A “component” may be a software module or the
distinguished physical-plant node (we do not consider multiple
physical plants, because a physical plant can be arbitrarily
complex). It is important to have runtime assurance techniques
for component-based control systems that are equally modular,
to reduce their associated complexity and cost.
Components may have different update periods (or execution periods). For the autonomous-vehicle example, themission-planning component’s update period may be a multi-

Categorical foundations- “Uniform framework for bisimilarityand bisimulation distance?”“Structural justification of
backpropagation for RNN?”

I. I NTRODUCTION-

Simplex [1]–[3] is a software architecture for high-assurance
process-control systems. It traditionally consists of a physical plant and two versions of the controller: an advanced
controller (AC) and a baseline controller (BC). The AC isin control of the plant under nominal operating conditions,and is designed to achieve high-performance according tocertain metrics (e.g., maneuverability, fuel economy, missioncompletion time). The BC is pre-certified to keep the plantwithin a prescribed safety region, i.e., a region of safe operation. A decision module (DM), which is also pre-certified,continually monitors the state of the plant and switches controlof the plant to the BC should the plant be in imminent danger-

verification

troller has bugs. As advanced controllers are increasingly more
complex, more adaptive with the use of unverified algorithms
such as machine-learning’s, runtime assurance techniques like
Simplex are becoming more important. Figure 1 illustrates the
Simplex architecture.

26[Komorida+, LICS’19][Sprunger+, LICS’19] …

Hasuo (NII, Tokyo)

Outline
Cyber-physical systems under uncertainties
Formal methods and testing for CPS
Hybrid system falsification
Logical connectives [CAV’19]
Causality in time [EMSOFT’18]… as demonstration of combining
logical and statistical

Other topics
27

Hasuo (NII, Tokyo)Hybrid System Falsification[Fainekos & Pappas, TCS’09]
Black-box, search-based testing. Actively search for erroneous input by:
Try an input
signalObserve thesystem’s behavior

throttle

speed
60
45
30
15
0

time
brake

Choose the next
input that is likely
to be erroneous

0

10

20

30

10

20

30

RPM
70
52.5
35
17.5
0

time

[Fainekos & Pappas, TCS’09]
A reinforcement learning problem,by moving

more robustly
true

??

true

from the Boolean semantics(erroneous or not)

false

input

Boolean semantics

to quantitative “robust semantics”(how far from being erroneous)
28

0This way toclimb down :)less soquantitativerobust semantics

inputDiscrete Structures inContinuous Learning & Optimization[Zhang, Ernst, Sedwards, Arcaini & Hasuo, EMSOFT’18][Zhang, Hasuo & Arcaini, CAV’19]

In hybrid system falsification(and statistical machine learning in general),eﬃciency comes mainly from
gradient descent (which is continuous)

Search-based testing(aka hybrid system falsification)- Active search for counterexamples- Incompletely but eﬃciently,
by reinforcement learning- [Zhang+, CAV’19] [Zhang+, EMSOFT’18]

Question: can we also exploit discrete structures
for eﬃciency and explainability?
Example: hierarchical optimization scheme [Zhang+, CAV’19]
Given: a black-box model M anda specification ⇤I ('1 _ '2 )Goal: input i s.t. M(i) violates the spec
<latexit sha1_base64="MmCJ43cd92+X1L3OT0Bd9Lf9u8w=">AAACB3icbVBLSwMxGMzWV62vVY+CBItQL2W3CHos9aK3CvYB3WXJptk2NJssSbZYSm9e/CtePCji1b/gzX9j2q6grQOBycw3JN+ECaNKO86XlVtZXVvfyG8WtrZ3dvfs/YOmEqnEpIEFE7IdIkUY5aShqWaknUiC4pCRVji4mvqtIZGKCn6nRwnxY9TjNKIYaSMF9rFXE/fBTckbIpn0aeB6JvFzqZwFdtEpOzPAZeJmpAgy1AP70+sKnMaEa8yQUh3XSbQ/RlJTzMik4KWKJAgPUI90DOUoJsofz/aYwFOjdGEkpDlcw5n6OzFGsVKjODSTMdJ9tehNxf+8TqqjS39MeZJqwvH8oShlUAs4LQV2qSRYs5EhCEtq/gpxH0mEtamuYEpwF1deJs1K2XXK7u15sVrL6siDI3ACSsAFF6AKrkEdNAAGD+AJvIBX69F6tt6s9/lozsoyh+APrI9vSB+Y6w==</latexit>“made thismuchprogress for

φi ”

Discrete Optim.

Feed search
results backRestrictsearchdomainContinuous Optim.

Which formula(φ1 or φ2)
to try to falsify

Stochastic gradient descent(such as CMA-ES)
for input that violates φi
29Multi-armed bandit
over subformulas φ1 and φ2

Multi-armed Bandits for Boolean Connectives
in Hybrid System Falsification

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini
National Institute of Informatics, Tokyo, JapanThe Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan
31st International Conference on Computer-Aided Verification
July 16, 2019

Falsification•

Falsification problem:M : black-box modelu : input signal (piecewise constant)M(u) : output signal' : specification in Temporal Logic• Goal: find an input signal

Example:throttle

hybrid system

u s.t. M(u) 2 '

speed
60
45
30
15

⇤[0,30] (speed < 120)
• Always Bounded-time

0

0

10

20

30

10

20

30

time
brake

RPM
70

Proposition

52.5
35
17.5
0

time
National Institute of Informatics, Tokyo, Japan

31

0

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

STL robustness•

Quantitative robustness semantics of STL [Donze, Maler FORMATS’10]e.g.,' = ⇤[0,30] (speed < 120)<latexit sha1_base64="X60qa9y9hXjW3qtSUsD+SLjhwhI=">AAAB8HicbVBNSwMxEJ2tX7V+VT16CRbBU9kVQS9C0YvHCvZD2qVk02wbmmRDki2Upb/CiwdFvPpzvPlvTNs9aOuDgcd7M8zMixRnxvr+t1dYW9/Y3Cpul3Z29/YPyodHTZOkmtAGSXii2xE2lDNJG5ZZTttKUywiTlvR6G7mt8ZUG5bIRztRNBR4IFnMCLZOeuqOsVZDhm565Ypf9edAqyTISQVy1Hvlr24/Iamg0hKOjekEvrJhhrVlhNNpqZsaqjAZ4QHtOCqxoCbM5gdP0ZlT+ihOtCtp0Vz9PZFhYcxERK5TYDs0y95M/M/rpDa+DjMmVWqpJItFccqRTdDse9RnmhLLJ45gopm7FZEh1phYl1HJhRAsv7xKmhfVwK8GD5eV2m0eRxFO4BTOIYArqME91KEBBAQ8wyu8edp78d69j0VrwctnjuEPvM8fWBuQFw==</latexit>

Speed

Speed

130

OutputSignals

Quantitative
Robustness

30

130

120

130

97.5

97.5

65

65

65

32.5

32.5

32.5

97.5

0

BooleanSatisfaction

120

Speed

0

10

20

Time

30

0

0

10

20

30

Time

0

120

0

10

20

True

True
Boolean

False

30

Real number-5

National Institute of Informatics, Tokyo, Japan

10

32

30

Time

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Hill-climbing optimization•

falsification => optimization•

robustness

Objective function: [[M(u), ']]<latexit sha1_base64="95eobfK1If83My+s418w9fQeH+M=">AAACEXicbZDLSsNAFIYn9VbrLerSzdQiVJCSiKDLohs3QgV7gSSUyXTSDp1MwsykUEJfwY2v4saFIm7dufNtnKRZaOsPAx//OYc55/djRqWyrG+jtLK6tr5R3qxsbe/s7pn7Bx0ZJQKTNo5YJHo+koRRTtqKKkZ6sSAo9Bnp+uObrN6dECFpxB/UNCZeiIacBhQjpa2+WXfcqgPdEKkRRiy9m9Vz9oM0mZ2euRMk4hH13KrXN2tWw8oFl8EuoAYKtfrmlzuIcBISrjBDUjq2FSsvRUJRzMis4iaSxAiP0ZA4GjkKifTS/KIZPNHOAAaR0I8rmLu/J1IUSjkNfd2ZrSsXa5n5X81JVHDlpZTHiSIczz8KEgZVBLN44IAKghWbakBYUL0rxCMkEFY6xIoOwV48eRk65w3batj3F7XmdRFHGRyBY1AHNrgETXALWqANMHgEz+AVvBlPxovxbnzMW0tGMXMI/sj4/AGaGpze</latexit>•

Goal: min [[M(u), ']]<latexit sha1_base64="95eobfK1If83My+s418w9fQeH+M=">AAACEXicbZDLSsNAFIYn9VbrLerSzdQiVJCSiKDLohs3QgV7gSSUyXTSDp1MwsykUEJfwY2v4saFIm7dufNtnKRZaOsPAx//OYc55/djRqWyrG+jtLK6tr5R3qxsbe/s7pn7Bx0ZJQKTNo5YJHo+koRRTtqKKkZ6sSAo9Bnp+uObrN6dECFpxB/UNCZeiIacBhQjpa2+WXfcqgPdEKkRRiy9m9Vz9oM0mZ2euRMk4hH13KrXN2tWw8oFl8EuoAYKtfrmlzuIcBISrjBDUjq2FSsvRUJRzMis4iaSxAiP0ZA4GjkKifTS/KIZPNHOAAaR0I8rmLu/J1IUSjkNfd2ZrSsXa5n5X81JVHDlpZTHiSIczz8KEgZVBLN44IAKghWbakBYUL0rxCMkEFY6xIoOwV48eRk65w3batj3F7XmdRFHGRyBY1AHNrgETXALWqANMHgEz+AVvBlPxovxbnzMW0tGMXMI/sj4/AGaGpze</latexit>•[[M(u), ']] < 0<latexit sha1_base64="zbRGujZJCU09UjYRomJdzWOZOHw=">AAACEnicbZDLSsNAFIYn9VbrLerSTWoRWpCSiKALF0U3boQK9gJJKJPppB06mYSZSaGEPIMbX8WNC0XcunLn2zhJs9DWHwY+/nMOc87vRZQIaZrfWmlldW19o7xZ2dre2d3T9w+6Iow5wh0U0pD3PSgwJQx3JJEU9yOOYeBR3PMmN1m9N8VckJA9yFmE3QCOGPEJglJZA71hO1XbCaAcI0iTu7Ses+cncdo4daaQR2PiOlX3yhzoNbNp5jKWwSqgBgq1B/qXMwxRHGAmEYVC2JYZSTeBXBJEcVpxYoEjiCZwhG2FDAZYuEl+UmqcKGdo+CFXj0kjd39PJDAQYhZ4qjNbWCzWMvO/mh1L/9JNCItiiRmaf+TH1JChkeVjDAnHSNKZAog4UbsaaAw5RFKlWFEhWIsnL0P3rGmZTev+vNa6LuIogyNwDOrAAhegBW5BG3QAAo/gGbyCN+1Je9HetY95a0krZg7BH2mfP0pZnTQ=</latexit>

•

done!

robustness
1“Hill-climbing” optimization algorithms•

Decide the next sample based on history•

More intelligent than random sampling•Tools: Breach [Donze CAV’10] (CMA-ES, NM, etc.)2
sampleS-TaLiRo [Annapureddy et al. TACAS’11] (SA etc.)

National Institute of Informatics, Tokyo, Japan

33

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Motivating example
Scale problem

•

•

e.g.,
<latexit sha1_base64="rUuSuBxDm+ZcTKv0Wcux6VLav9g=">AAACF3icbVDLSgMxFM34rPVVdekmWIQKUjKtoBul1I3LCvYBnaFk0ts2NPMwyRTL0L9w46+4caGIW935N6aPhbYeCBzOuZebc7xIcKUJ+baWlldW19ZTG+nNre2d3czefk2FsWRQZaEIZcOjCgQPoKq5FtCIJFDfE1D3+tdjvz4AqXgY3OlhBK5PuwHvcEa1kVqZvBP1uAP3MR845fChlTTJaZG4o1wXqMSXuOjoEKsIoH2FC+SklcmSPJkALxJ7RrJohkor8+W0Qxb7EGgmqFJNm0TaTajUnAkYpZ1YQURZn3ahaWhAfVBuMsk1wsdGaeNOKM0LNJ6ovzcS6is19D0z6VPdU/PeWPzPa8a6c+EmPIhiDQGbHurEApus45Jwm0tgWgwNoUxy81fMelRSpk2VaVOCPR95kdQKeZvk7duzbKk8qyOFDtERyiEbnaMSukEVVEUMPaJn9IrerCfrxXq3PqajS9Zs5wD9gfX5A8tfnb0=</latexit>⌘ ⇤I ('1 _ '2 ) where '1 ⌘ ¬(gear = 3) and '2 ⌘ (speed > 20)•<latexit sha1_base64="9LUCmGaeMwOiWHQPveg/0GpwxgA=">AAACCHicbVA9SwNBEN2LXzF+RS0tXAxCbMKdCtoIQRvLCOYDcsext5lLluztnbt7gRBS2vhXbCwUsfUn2Plv3CRXaOKDgcd7M8zMCxLOlLbtbyu3tLyyupZfL2xsbm3vFHf3GipOJYU6jXksWwFRwJmAumaaQyuRQKKAQzPo30z85gCkYrG418MEvIh0BQsZJdpIfvHQHRCZ9JjvYBceUjbAroBuuQtE4it8duIXS3bFngIvEicjJZSh5he/3E5M0wiEppwo1XbsRHsjIjWjHMYFN1WQENonXWgbKkgEyhtNHxnjY6N0cBhLU0Ljqfp7YkQipYZRYDojontq3puI/3ntVIeX3oiJJNUg6GxRmHKsYzxJBXeYBKr50BBCJTO3YtojklBtsiuYEJz5lxdJ47Ti2BXn7rxUvc7iyKMDdITKyEEXqIpuUQ3VEUWP6Bm9ojfryXqx3q2PWWvOymb20R9Ynz+BBJhT</latexit><latexit sha1_base64="O91FlTCgvLvjo/Cif3t3I9FR65Y=">AAACE3icbVBLSwMxGMz6rPW16tFLsAjVQ9ktgh5Lveitgn1Ad1myadqGZpM1yRbL0v/gxb/ixYMiXr1489+Ytito60BgMvMNyTdhzKjSjvNlLS2vrK6t5zbym1vbO7v23n5DiURiUseCCdkKkSKMclLXVDPSiiVBUchIMxxcTvzmkEhFBb/Vo5j4Eepx2qUYaSMF9qkX96lH7hI69KriPkivx0VviKRRA9cz6Z9L+SSwC07JmQIuEjcjBZChFtifXkfgJCJcY4aUartOrP0USU0xI+O8lygSIzxAPdI2lKOIKD+d7jSGx0bpwK6Q5nANp+rvRIoipUZRaCYjpPtq3puI/3ntRHcv/JTyONGE49lD3YRBLeCkINihkmDNRoYgLKn5K8R9JBHWpsa8KcGdX3mRNMol1ym5N2eFSjWrIwcOwREoAhecgwq4AjVQBxg8gCfwAl6tR+vZerPeZ6NLVpY5AH9gfXwDd7iefg==</latexit>•⌘ ⇤[0,30] (gear = 3 ! speed > 20)<latexit sha1_base64="qSsp5Cu+moY1jaVI121yrkXczCc=">AAACBnicbVDLSsNAFJ3UV62vqEsRBotQNyUpgq6k6MZlBfuAJoTJ5LYdOnk4MymU0JUbf8WNC0Xc+g3u/BunbRbaeuDC4Zx7ufceP+FMKsv6Ngorq2vrG8XN0tb2zu6euX/QknEqKDRpzGPR8YkEziJoKqY4dBIBJPQ5tP3hzdRvj0BIFkf3apyAG5J+xHqMEqUlzzx2RkQkA+bVsAMPKRvhikwAAnyFa9aZZ5atqjUDXiZ2TsooR8Mzv5wgpmkIkaKcSNm1rUS5GRGKUQ6TkpNKSAgdkj50NY1ICNLNZm9M8KlWAtyLha5I4Zn6eyIjoZTj0NedIVEDuehNxf+8bqp6l27GoiRVENH5ol7KsYrxNBMcMAFU8bEmhAqmb8V0QAShSidX0iHYiy8vk1ataltV++68XL/O4yiiI3SCKshGF6iOblEDNRFFj+gZvaI348l4Md6Nj3lrwchnDtEfGJ8/rvWXTA==</latexit>

STL robustness semantics [Donze, Maler FORMATS’10]

gear 2 {1, 2, 3, 4}
speed 2 [0, 150]
<latexit sha1_base64="ykhpDixlbz6TbjRqOAl2Vx/riTM=">AAAB+3icbVBNS8NAEJ3Ur1q/Yj16WSyCh1KSWtBj0YvHCvYDmlA22027dLMJuxuxhP4VLx4U8eof8ea/cdvmoK0PBh7vzTAzL0g4U9pxvq3CxubW9k5xt7S3f3B4ZB+XOypOJaFtEvNY9gKsKGeCtjXTnPYSSXEUcNoNJrdzv/tIpWKxeNDThPoRHgkWMoK1kQZ2eUSx9JjwMrdar15WG95sYFecmrMAWiduTiqQozWwv7xhTNKICk04VqrvOon2Myw1I5zOSl6qaILJBI9o31CBI6r8bHH7DJ0bZYjCWJoSGi3U3xMZjpSaRoHpjLAeq1VvLv7n9VMdXvsZE0mqqSDLRWHKkY7RPAg0ZJISzaeGYCKZuRWRMZaYaBNXyYTgrr68Tjr1muvU3PtGpXmTx1GEUziDC3DhCppwBy1oA4EneIZXeLNm1ov1bn0sWwtWPnMCf2B9/gAiupMv</latexit>?

[[M(u), '1 ]] t [[M(u), '2 ]]<latexit sha1_base64="JR7BTau9LjPxATRvkQqnjDWedQ4=">AAAB7XicbVDLSgNBEOz1GeMr6tHLYBA8hV0R9Bj04jGCeUCyhNlJbzJmdmadmRVCyD948aCIV//Hm3/jJNmDJhY0FFXddHdFqeDG+v63t7K6tr6xWdgqbu/s7u2XDg4bRmWaYZ0poXQrogYFl1i33ApspRppEglsRsObqd98Qm24kvd2lGKY0L7kMWfUOqnRMY8sS7ulsl/xZyDLJMhJGXLUuqWvTk+xLEFpmaDGtAM/teGYasuZwEmxkxlMKRvSPrYdlTRBE45n107IqVN6JFbalbRkpv6eGNPEmFESuc6E2oFZ9Kbif147s/FVOOYyzSxKNl8UZ4JYRaavkx7XyKwYOUKZ5u5WwgZUU2ZdQEUXQrD48jJpnFcCvxLcXZSr13kcBTiGEziDAC6hCrdQgzoweIBneIU3T3kv3rv3MW9d8fKZI/gD7/MHxWOPPg==</latexit><latexit<latexit sha1_base64="ebiV7XKXew+zzhYLvVtJKJL8icI=">AAACE3icbZDLSsNAFIYn9VbrLerSzdQiVJGSiKDLohs3QgV7gSSEyXTSDk4uzEwKJeQd3Pgqblwo4taNO9/GSZqFtv4w8PGfc5hzfi9mVEjD+NYqS8srq2vV9drG5tb2jr671xNRwjHp4ohFfOAhQRgNSVdSycgg5gQFHiN97+E6r/cnhAsahfdyGhMnQKOQ+hQjqSxXP7HsumUHSI4xYults0DPT5PsODuF9gTxeExd07Hrjqs3jJZRCC6CWUIDlOq4+pc9jHASkFBihoSwTCOWToq4pJiRrGYngsQIP6ARsRSGKCDCSYubMniknCH0I65eKGHh/p5IUSDENPBUZ76ymK/l5n81K5H+pZPSME4kCfHsIz9hUEYwDwgOKSdYsqkChDlVu0I8RhxhqWKsqRDM+ZMXoXfWMo2WeXfeaF+VcVTBATgETWCCC9AGN6ADugCDR/AMXsGb9qS9aO/ax6y1opUz++CPtM8f4Wedgg==</latexit><latexit sha1_base64="zds/yhJc1BoNNiA/zrb5Il0J98g=">AAAB+HicbVBNS8NAEN34WetHox69LBbBg5SNKHosevFYwX5AG8pmM2mXbjZhdyPU0F/ixYMiXv0p3vw3btsctPXBwOO9GWbmBang2hDy7aysrq1vbJa2yts7u3sVd/+gpZNMMWiyRCSqE1ANgktoGm4EdFIFNA4EtIPR7dRvP4LSPJEPZpyCH9OB5BFn1Fip71Z0ChD2uOySM++S+H23SmpkBrxMvIJUUYFG3/3qhQnLYpCGCap11yOp8XOqDGcCJuVepiGlbEQH0LVU0hi0n88On+ATq4Q4SpQtafBM/T2R01jrcRzYzpiaoV70puJ/Xjcz0bWfc5lmBiSbL4oygU2CpyngkCtgRowtoUxxeytmQ6ooMzarsg3BW3x5mbTOax6pefcX1fpNEUcJHaFjdIo8dIXq6A41UBMxlKFn9IrenCfnxXl3PuatK04xc4j+wPn8AU30ki8=</latexit>

National Institute of Informatics, Tokyo, Japan6<latexit sha1_base64="Tr5ACI1YZ6g2Rk3HAtWTWzDQDuM=">AAACE3icbZDLSsNAFIYn9VbrLerSzdQiVJGSFEGXRTduhAr2AkkIk+mkHTq5MDMplJB3cOOruHGhiFs37nwbJ2kX2vrDwMd/zmHO+b2YUSEN41srrayurW+UNytb2zu7e/r+QVdECcekgyMW8b6HBGE0JB1JJSP9mBMUeIz0vPFNXu9NCBc0Ch/kNCZOgIYh9SlGUlmufmbZVcsOkBxhxNK7eoGenybZaXYO7Qni8Yi6TceuOq5eMxpGIbgM5hxqYK62q3/ZgwgnAQklZkgIyzRi6aSIS4oZySp2IkiM8BgNiaUwRAERTlrclMET5QygH3H1QgkL9/dEigIhpoGnOvOVxWItN/+rWYn0r5yUhnEiSYhnH/kJgzKCeUBwQDnBkk0VIMyp2hXiEeIISxVjRYVgLp68DN1mwzQa5v1FrXU9j6MMjsAxqAMTXIIWuAVt0AEYPIJn8AretCftRXvXPmatJW0+cwj+SPv8AeLvnYM=</latexit>
sha1_base64="hP+6LrUf2d3tZaldqaQQvEKMXyw=">AAAB2XicbZDNSgMxFIXv1L86Vq1rN8EiuCozbnQpuHFZwbZCO5RM5k4bmskMyR2hDH0BF25EfC93vo3pz0JbDwQ+zknIvSculLQUBN9ebWd3b/+gfugfNfzjk9Nmo2fz0gjsilzl5jnmFpXU2CVJCp8LgzyLFfbj6f0i77+gsTLXTzQrMMr4WMtUCk7O6oyaraAdLMW2IVxDC9YaNb+GSS7KDDUJxa0dhEFBUcUNSaFw7g9LiwUXUz7GgUPNM7RRtRxzzi6dk7A0N+5oYkv394uKZ9bOstjdzDhN7Ga2MP/LBiWlt1EldVESarH6KC0Vo5wtdmaJNChIzRxwYaSblYkJN1yQa8Z3HYSbG29D77odBu3wMYA6nMMFXEEIN3AHD9CBLghI4BXevYn35n2suqp569LO4I+8zx84xIo4</latexit>
sha1_base64="y29SFyS1+gxNr7eMGONaWiqeGug=">AAACCHicbZDLSgMxGIX/qbdaq45u3aQWoYqUmW50KbhxI1SwF5gZhkyaaUMzF5JMoQzzDm58FTcuFPEJ3Pk2ppeFth4IfJyTkP8/QcqZVJb1bZQ2Nre2d8q7lb3q/sGheVTtyiQThHZIwhPRD7CknMW0o5jitJ8KiqOA014wvp3lvQkVkiXxo5qm1IvwMGYhI1hpyzcvHLfmuBFWI4J5ft+YYxDmWXFeXCJ3gkU6Yn7Lc2ueb9atpjUXWgd7CXVYqu2bX+4gIVlEY0U4ltKxrVR5ORaKEU6LiptJmmIyxkPqaIxxRKWXz3cq0Jl2BihMhD6xQnP394scR1JOo0DfnI0sV7OZ+V/mZCq89nIWp5miMVl8FGYcqQTNCkIDJihRfKoBE8H0rIiMsMBE6RorugR7deV16LaattW0HywowwmcQgNsuIIbuIM2dIDAE7zAG7wbz8ar8bGoq2QsezuGPzI+fwAgNpwF</latexit>
sha1_base64="WI7eKz0Fx5aKCNJs1zLQA/bUBTs=">AAACE3icbZDLSsNAFIYn9VbrLerSzdQiVJGSdKPLohs3QgV7gSSEyXTSDk4uzEwKJeQd3Pgqblwo4taNO9/GSZqFtv4w8PGfc5hzfi9mVEjD+NYqK6tr6xvVzdrW9s7unr5/0BdRwjHp4YhFfOghQRgNSU9Sycgw5gQFHiMD7+E6rw+mhAsahfdyFhMnQOOQ+hQjqSxXP7PsumUHSE4wYults0DPT5PsNDuH9hTxeELdtmPXHVdvGC2jEFwGs4QGKNV19S97FOEkIKHEDAlhmUYsnRRxSTEjWc1OBIkRfkBjYikMUUCEkxY3ZfBEOSPoR1y9UMLC/T2RokCIWeCpznxlsVjLzf9qViL9SyelYZxIEuL5R37CoIxgHhAcUU6wZDMFCHOqdoV4gjjCUsVYUyGYiycvQ7/dMo2WeWc0OldlHFVwBI5BE5jgAnTADeiCHsDgETyDV/CmPWkv2rv2MW+taOXMIfgj7fMH4a+dfw==</latexit>

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Motivating example⌘ ⇤[0,30] (gear = 3 ! speed > 20)<latexit sha1_base64="rUuSuBxDm+ZcTKv0Wcux6VLav9g=">AAACF3icbVDLSgMxFM34rPVVdekmWIQKUjKtoBul1I3LCvYBnaFk0ts2NPMwyRTL0L9w46+4caGIW935N6aPhbYeCBzOuZebc7xIcKUJ+baWlldW19ZTG+nNre2d3czefk2FsWRQZaEIZcOjCgQPoKq5FtCIJFDfE1D3+tdjvz4AqXgY3OlhBK5PuwHvcEa1kVqZvBP1uAP3MR845fChlTTJaZG4o1wXqMSXuOjoEKsIoH2FC+SklcmSPJkALxJ7RrJohkor8+W0Qxb7EGgmqFJNm0TaTajUnAkYpZ1YQURZn3ahaWhAfVBuMsk1wsdGaeNOKM0LNJ6ovzcS6is19D0z6VPdU/PeWPzPa8a6c+EmPIhiDQGbHurEApus45Jwm0tgWgwNoUxy81fMelRSpk2VaVOCPR95kdQKeZvk7duzbKk8qyOFDtERyiEbnaMSukEVVEUMPaJn9IrerCfrxXq3PqajS9Zs5wD9gfX5A8tfnb0=</latexit>'1 ⌘ ¬(gear = 3)
⌘ ⇤I ('1 _ '2 ) ' ⌘ (speed > 20)
2<latexit sha1_base64="9LUCmGaeMwOiWHQPveg/0GpwxgA=">AAACCHicbVA9SwNBEN2LXzF+RS0tXAxCbMKdCtoIQRvLCOYDcsext5lLluztnbt7gRBS2vhXbCwUsfUn2Plv3CRXaOKDgcd7M8zMCxLOlLbtbyu3tLyyupZfL2xsbm3vFHf3GipOJYU6jXksWwFRwJmAumaaQyuRQKKAQzPo30z85gCkYrG418MEvIh0BQsZJdpIfvHQHRCZ9JjvYBceUjbAroBuuQtE4it8duIXS3bFngIvEicjJZSh5he/3E5M0wiEppwo1XbsRHsjIjWjHMYFN1WQENonXWgbKkgEyhtNHxnjY6N0cBhLU0Ljqfp7YkQipYZRYDojontq3puI/3ntVIeX3oiJJNUg6GxRmHKsYzxJBXeYBKr50BBCJTO3YtojklBtsiuYEJz5lxdJ47Ti2BXn7rxUvc7iyKMDdITKyEEXqIpuUQ3VEUWP6Bm9ojfryXqx3q2PWWvOymb20R9Ynz+BBJhT</latexit><latexit sha1_base64="O91FlTCgvLvjo/Cif3t3I9FR65Y=">AAACE3icbVBLSwMxGMz6rPW16tFLsAjVQ9ktgh5Lveitgn1Ad1myadqGZpM1yRbL0v/gxb/ixYMiXr1489+Ytito60BgMvMNyTdhzKjSjvNlLS2vrK6t5zbym1vbO7v23n5DiURiUseCCdkKkSKMclLXVDPSiiVBUchIMxxcTvzmkEhFBb/Vo5j4Eepx2qUYaSMF9qkX96lH7hI69KriPkivx0VviKRRA9cz6Z9L+SSwC07JmQIuEjcjBZChFtifXkfgJCJcY4aUartOrP0USU0xI+O8lygSIzxAPdI2lKOIKD+d7jSGx0bpwK6Q5nANp+rvRIoipUZRaCYjpPtq3puI/3ntRHcv/JTyONGE49lD3YRBLeCkINihkmDNRoYgLKn5K8R9JBHWpsa8KcGdX3mRNMol1ym5N2eFSjWrIwcOwREoAhecgwq4AjVQBxg8gCfwAl6tR+vZerPeZ6NLVpY5AH9gfXwDd7iefg==</latexit><latexit sha1_base64="qSsp5Cu+moY1jaVI121yrkXczCc=">AAACBnicbVDLSsNAFJ3UV62vqEsRBotQNyUpgq6k6MZlBfuAJoTJ5LYdOnk4MymU0JUbf8WNC0Xc+g3u/BunbRbaeuDC4Zx7ufceP+FMKsv6Ngorq2vrG8XN0tb2zu6euX/QknEqKDRpzGPR8YkEziJoKqY4dBIBJPQ5tP3hzdRvj0BIFkf3apyAG5J+xHqMEqUlzzx2RkQkA+bVsAMPKRvhikwAAnyFa9aZZ5atqjUDXiZ2TsooR8Mzv5wgpmkIkaKcSNm1rUS5GRGKUQ6TkpNKSAgdkj50NY1ICNLNZm9M8KlWAtyLha5I4Zn6eyIjoZTj0NedIVEDuehNxf+8bqp6l27GoiRVENH5ol7KsYrxNBMcMAFU8bEmhAqmb8V0QAShSidX0iHYiy8vk1ataltV++68XL/O4yiiI3SCKshGF6iOblEDNRFFj+gZvaI348l4Md6Nj3lrwchnDtEfGJ8/rvWXTA==</latexit>2

not (gear[t] == 3)(a)Quant. sat
Bool. sat[[M(u), '1 ]]<latexit sha1_base64="iogWf2yE1oa0906PKQWzaI/Y+TU=">AAACEnicbZDLSsNAFIYnXmu9RV26mVqEFqQkIuiy6MaNUMFeIAlhMp20QycXZiaFEvIMbnwVNy4UcevKnW/jJM1CW38Y+PjPOcw5vxczKqRhfGsrq2vrG5uVrer2zu7evn5w2BNRwjHp4ohFfOAhQRgNSVdSycgg5gQFHiN9b3KT1/tTwgWNwgc5i4kToFFIfYqRVJarNy27ZtkBkmOMWHqXNQr2/DTJmmf2FPF4TF3TsWuOq9eNllEILoNZQh2U6rj6lz2McBKQUGKGhLBMI5ZOirikmJGsaieCxAhP0IhYCkMUEOGkxUkZPFXOEPoRVy+UsHB/T6QoEGIWeKozX1gs1nLzv5qVSP/KSWkYJ5KEeP6RnzAoI5jnA4eUEyzZTAHCnKpdIR4jjrBUKVZVCObiycvQO2+ZRsu8v6i3r8s4KuAYnIAGMMElaINb0AFdgMEjeAav4E170l60d+1j3rqilTNH4I+0zx+A3p1Y</latexit>
sha1_base64="hP+6LrUf2d3tZaldqaQQvEKMXyw=">AAAB2XicbZDNSgMxFIXv1L86Vq1rN8EiuCozbnQpuHFZwbZCO5RM5k4bmskMyR2hDH0BF25EfC93vo3pz0JbDwQ+zknIvSculLQUBN9ebWd3b/+gfugfNfzjk9Nmo2fz0gjsilzl5jnmFpXU2CVJCp8LgzyLFfbj6f0i77+gsTLXTzQrMMr4WMtUCk7O6oyaraAdLMW2IVxDC9YaNb+GSS7KDDUJxa0dhEFBUcUNSaFw7g9LiwUXUz7GgUPNM7RRtRxzzi6dk7A0N+5oYkv394uKZ9bOstjdzDhN7Ga2MP/LBiWlt1EldVESarH6KC0Vo5wtdmaJNChIzRxwYaSblYkJN1yQa8Z3HYSbG29D77odBu3wMYA6nMMFXEEIN3AHD9CBLghI4BXevYn35n2suqp569LO4I+8zx84xIo4</latexit>
sha1_base64="X7LC1tMI51Dgj+1XvadQ7ANYMK8=">AAACB3icbZDLSsNAGIX/eK21anTrZmoRWpCSuNGl4MaNUMFeIAlhMp20QycXZiaFEvIMbnwVNy4U8Q3c+TZO2i609cDAxzkzzP+fIOVMKsv6NjY2t7Z3dit71f3aweGReVzrySQThHZJwhMxCLCknMW0q5jidJAKiqOA034wuS3z/pQKyZL4Uc1S6kV4FLOQEay05Zstx607boTVmGCe3xfNOQdhnhWtC3eKRTpmvu25dc83G1bbmgutg72EBizV8c0vd5iQLKKxIhxL6dhWqrwcC8UIp0XVzSRNMZngEXU0xjii0svnKxXoXDtDFCZCn1ihufv7RY4jKWdRoG+WA8vVrDT/y5xMhddezuI0UzQmi4/CjCOVoLIfNGSCEsVnGjARTM+KyBgLTJRusapLsFdXXofeZdu22vaDBRU4hTNogg1XcAN30IEuEHiCF3iDd+PZeDU+FnVtGMveTuCPjM8fv8Gb2w==</latexit>
sha1_base64="1YsUvd8MFRP7wHDcbumXqwQXLFA=">AAACEnicbZDLSsNAFIYn9VbrLerSTWoRWpCSuNFl0Y0boYK9QBLCZDpph04mYWZSKCHP4MZXceNCEbeu3Pk2TtIstPWHgY//nMOc8/sxJUKa5rdWWVvf2Nyqbtd2dvf2D/TDo76IEo5wD0U04kMfCkwJwz1JJMXDmGMY+hQP/OlNXh/MMBckYg9yHmM3hGNGAoKgVJant2ynbjshlBMEaXqXNQv2gzTJWufODPJ4QjzLdequpzfMtlnIWAWrhAYo1fX0L2cUoSTETCIKhbAtM5ZuCrkkiOKs5iQCxxBN4RjbChkMsXDT4qTMOFPOyAgirh6TRuH+nkhhKMQ89FVnvrBYruXmfzU7kcGVmxIWJxIztPgoSKghIyPPxxgRjpGkcwUQcaJ2NdAEcoikSrGmQrCWT16F/kXbMtvWvdnoXJdxVMEJOAVNYIFL0AG3oAt6AIFH8AxewZv2pL1o79rHorWilTPH4I+0zx9/np1U</latexit>

throttle

31

0
30

-2
29

0

0

brake

5
5

100
1

[[M(u), '2 ]]

true

10
10

15

(b)20

15
2520
speed[t] >

20

25

false
30

30

true

0

0

<latexit sha1_base64="9cpwUIxj3lyDzaFea4y5+jQdeHU=">AAACEnicbZDLSsNAFIYn9VbrLerSzdQitCAlKYIui27cCBXsBZIQJtNJO3RyYWZSKKHP4MZXceNCEbeu3Pk2TtIstPWHgY//nMOc83sxo0IaxrdWWlvf2Nwqb1d2dvf2D/TDo56IEo5JF0cs4gMPCcJoSLqSSkYGMSco8Bjpe5ObrN6fEi5oFD7IWUycAI1C6lOMpLJcvWHZVcsOkBxjxNK7eT1nz0+TeePcniIej6nbcuyq4+o1o2nkgqtgFlADhTqu/mUPI5wEJJSYISEs04ilkyIuKWZkXrETQWKEJ2hELIUhCohw0vykOTxTzhD6EVcvlDB3f0+kKBBiFniqM1tYLNcy87+alUj/yklpGCeShHjxkZ8wKCOY5QOHlBMs2UwBwpyqXSEeI46wVClWVAjm8smr0Gs1TaNp3l/U2tdFHGVwAk5BHZjgErTBLeiALsDgETyDV/CmPWkv2rv2sWgtacXMMfgj7fMHgmadWQ==</latexit>-1 -100
0
0
4

Text

5

5 10

15 10

(c)

50

gear

[[M(u), '1 _ '2 ]]

15 25
30 20
(not (gear[t] == 3)) or (speed[t] > 20)[[w1 , ]] = 1

2
0

0

speed

100

5

0

50

15

5
(d)

50

20

25

30

10
15
20
alw_[0,30] ((not (gear[t] == 3)) or (speed[t] > 20))

25

false
30
true

[[M(u), ⇤I ('1 _ '2 )]]<latexit sha1_base64="KGDpApNciXxZ1mQ/tKu79UJg0ag=">AAACJ3icbVBbS8MwGE29znmr+uhL5xA2kNEOQZ9kzBd9ECa4C7SlpFm6haUXknQ4Sv+NL/4VXwQV0Uf/iVlXQTcPBE7Od0nOcSNKuND1T2VpeWV1bb2wUdzc2t7ZVff2OzyMGcJtFNKQ9VzIMSUBbgsiKO5FDEPfpbjrji6n9e4YM07C4E5MImz7cBAQjyAopOSoF6ZVMi0fiiGCNLlJKxl3vSROqydWM7x3rivWGLJoSBzDktt+LvWqbZVsRy3rNT2DtkiMnJRBjpajvlj9EMU+DgSikHPT0CNhJ5AJgihOi1bMcQTRCA6wKWkAfcztJPOZasdS6WteyOQJhJapvycS6HM+8V3ZOXXB52tT8b+aGQvv3E5IEMUCB2j2kBdTTYTaNDStTxhGgk4kgYgR+VcNDSGDSMhoizIEY97yIunUa4ZeM25Py41mHkcBHIIjUAEGOAMNcAVaoA0QeABP4BW8KY/Ks/KufMxal5R85gD8gfL1Dapypcg=</latexit>

10

true

speed

gear

<latexit sha1_base64="qnMdUekalbx7LgkhmI9/uA/xKSA=">AAACB3icbVDLSsNAFJ3UV62vqEtBphbBhZSMCLoRim5cVrAPSEKZTCft0MkkzEyUErpz46+4caGIW3/BnX/jpM1CqwcuHM65l3vvCRLOlHacL6u0sLi0vFJeraytb2xu2ds7bRWnktAWiXksuwFWlDNBW5ppTruJpDgKOO0Eo6vc79xRqVgsbvU4oX6EB4KFjGBtpJ6973pV14uwHgZhdj/poWMvGTLoe1UfXkDUs2tO3ZkC/iWoIDVQoNmzP71+TNKICk04VspFTqL9DEvNCKeTipcqmmAywgPqGipwRJWfTf+YwEOj9GEYS1NCw6n6cyLDkVLjKDCd+cVq3svF/zw31eG5nzGRpJoKMlsUphzqGOahwD6TlGg+NgQTycytkAyxxESb6ComBDT/8l/SPqkjp45uTmuNyyKOMtgDB+AIIHAGGuAaNEELEPAAnsALeLUerWfrzXqftZasYmYX/IL18Q1Tf5el</latexit><latexit sha1_base64="EhrB+eZTLWtmYn4NID52bpFoqPY=">AAACH3icbVDLSsNAFJ3UV62vqEs3U4tQQUpSRF0W3bgRKtgHJCFMppN26OTBzKRQQv/Ejb/ixoUi4q5/4ySNoNUDA2fOuXfm3uPFjAppGHOttLK6tr5R3qxsbe/s7un7B10RJRyTDo5YxPseEoTRkHQklYz0Y05Q4DHS88Y3md+bEC5oFD7IaUycAA1D6lOMpJJc/cKyq5YdIDnCiKV3s3rOPT9NZqdn9gTxeERd01bPfF+ajl11XL1mNIwc8C8xC1IDBdqu/mkPIpwEJJSYISEs04ilkyIuKWZkVrETQWKEx2hILEVDFBDhpPl+M3iilAH0I65OKGGu/uxIUSDENPBUZTa9WPYy8T/PSqR/5aQ0jBNJQrz4yE8YlBHMwoIDygmWbKoIwpyqWSEeIY6wVJFWVAjm8sp/SbfZMI2GeX9ea10XcZTBETgGdWCCS9ACt6ANOgCDR/AMXsGb9qS9aO/ax6K0pBU9h+AXtPkXFJGi+g==</latexit>

0

25

20

false
30

0

0

0

5

10

15

20

25

30

time

0

National Institute of Informatics, Tokyo, Japan

5

10

35

15
time

20

25

false
30

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Motivating example0-25⌘ ⇤[0,30] (gear = 3 ! speed > 20)<latexit sha1_base64="rUuSuBxDm+ZcTKv0Wcux6VLav9g=">AAACF3icbVDLSgMxFM34rPVVdekmWIQKUjKtoBul1I3LCvYBnaFk0ts2NPMwyRTL0L9w46+4caGIW935N6aPhbYeCBzOuZebc7xIcKUJ+baWlldW19ZTG+nNre2d3czefk2FsWRQZaEIZcOjCgQPoKq5FtCIJFDfE1D3+tdjvz4AqXgY3OlhBK5PuwHvcEa1kVqZvBP1uAP3MR845fChlTTJaZG4o1wXqMSXuOjoEKsIoH2FC+SklcmSPJkALxJ7RrJohkor8+W0Qxb7EGgmqFJNm0TaTajUnAkYpZ1YQURZn3ahaWhAfVBuMsk1wsdGaeNOKM0LNJ6ovzcS6is19D0z6VPdU/PeWPzPa8a6c+EmPIhiDQGbHurEApus45Jwm0tgWgwNoUxy81fMelRSpk2VaVOCPR95kdQKeZvk7duzbKk8qyOFDtERyiEbnaMSukEVVEUMPaJn9IrerCfrxXq3PqajS9Zs5wD9gfX5A8tfnb0=</latexit>'100
1 ⌘ ¬(gear = 3)
⌘ ⇤I ('1 _ '2 ) ' ⌘ (speed > 20)
2<latexit sha1_base64="9LUCmGaeMwOiWHQPveg/0GpwxgA=">AAACCHicbVA9SwNBEN2LXzF+RS0tXAxCbMKdCtoIQRvLCOYDcsext5lLluztnbt7gRBS2vhXbCwUsfUn2Plv3CRXaOKDgcd7M8zMCxLOlLbtbyu3tLyyupZfL2xsbm3vFHf3GipOJYU6jXksWwFRwJmAumaaQyuRQKKAQzPo30z85gCkYrG418MEvIh0BQsZJdpIfvHQHRCZ9JjvYBceUjbAroBuuQtE4it8duIXS3bFngIvEicjJZSh5he/3E5M0wiEppwo1XbsRHsjIjWjHMYFN1WQENonXWgbKkgEyhtNHxnjY6N0cBhLU0Ljqfp7YkQipYZRYDojontq3puI/3ntVIeX3oiJJNUg6GxRmHKsYzxJBXeYBKr50BBCJTO3YtojklBtsiuYEJz5lxdJ47Ti2BXn7rxUvc7iyKMDdITKyEEXqIpuUQ3VEUWP6Bm9ojfryXqx3q2PWWvOymb20R9Ynz+BBJhT</latexit><latexit sha1_base64="O91FlTCgvLvjo/Cif3t3I9FR65Y=">AAACE3icbVBLSwMxGMz6rPW16tFLsAjVQ9ktgh5Lveitgn1Ad1myadqGZpM1yRbL0v/gxb/ixYMiXr1489+Ytito60BgMvMNyTdhzKjSjvNlLS2vrK6t5zbym1vbO7v23n5DiURiUseCCdkKkSKMclLXVDPSiiVBUchIMxxcTvzmkEhFBb/Vo5j4Eepx2qUYaSMF9qkX96lH7hI69KriPkivx0VviKRRA9cz6Z9L+SSwC07JmQIuEjcjBZChFtifXkfgJCJcY4aUartOrP0USU0xI+O8lygSIzxAPdI2lKOIKD+d7jSGx0bpwK6Q5nANp+rvRIoipUZRaCYjpPtq3puI/3ntRHcv/JTyONGE49lD3YRBLeCkINihkmDNRoYgLKn5K8R9JBHWpsa8KcGdX3mRNMol1ym5N2eFSjWrIwcOwREoAhecgwq4AjVQBxg8gCfwAl6tR+vZerPeZ6NLVpY5AH9gfXwDd7iefg==</latexit><latexit sha1_base64="qSsp5Cu+moY1jaVI121yrkXczCc=">AAACBnicbVDLSsNAFJ3UV62vqEsRBotQNyUpgq6k6MZlBfuAJoTJ5LYdOnk4MymU0JUbf8WNC0Xc+g3u/BunbRbaeuDC4Zx7ufceP+FMKsv6Ngorq2vrG8XN0tb2zu6euX/QknEqKDRpzGPR8YkEziJoKqY4dBIBJPQ5tP3hzdRvj0BIFkf3apyAG5J+xHqMEqUlzzx2RkQkA+bVsAMPKRvhikwAAnyFa9aZZ5atqjUDXiZ2TsooR8Mzv5wgpmkIkaKcSNm1rUS5GRGKUQ6TkpNKSAgdkj50NY1ICNLNZm9M8KlWAtyLha5I4Zn6eyIjoZTj0NedIVEDuehNxf+8bqp6l27GoiRVENH5ol7KsYrxNBMcMAFU8bEmhAqmb8V0QAShSidX0iHYiy8vk1ataltV++68XL/O4yiiI3SCKshGF6iOblEDNRFFj+gZvaI348l4Md6Nj3lrwchnDtEfGJ8/rvWXTA==</latexit>(a) not ((gear[t] == 3))

41
2

throttle[[M(u), '1 ]]

true

0

Quant. sat
Bool. sat40
0<latexit sha1_base64="iogWf2yE1oa0906PKQWzaI/Y+TU=">AAACEnicbZDLSsNAFIYnXmu9RV26mVqEFqQkIuiy6MaNUMFeIAlhMp20QycXZiaFEvIMbnwVNy4UcevKnW/jJM1CW38Y+PjPOcw5vxczKqRhfGsrq2vrG5uVrer2zu7evn5w2BNRwjHp4ohFfOAhQRgNSVdSycgg5gQFHiN9b3KT1/tTwgWNwgc5i4kToFFIfYqRVJarNy27ZtkBkmOMWHqXNQr2/DTJmmf2FPF4TF3TsWuOq9eNllEILoNZQh2U6rj6lz2McBKQUGKGhLBMI5ZOirikmJGsaieCxAhP0IhYCkMUEOGkxUkZPFXOEPoRVy+UsHB/T6QoEGIWeKozX1gs1nLzv5qVSP/KSWkYJ5KEeP6RnzAoI5jnA4eUEyzZTAHCnKpdIR4jjrBUKVZVCObiycvQO2+ZRsu8v6i3r8s4KuAYnIAGMMElaINb0AFdgMEjeAav4E170l60d+1j3rqilTNH4I+0zx+A3p1Y</latexit>
sha1_base64="hP+6LrUf2d3tZaldqaQQvEKMXyw=">AAAB2XicbZDNSgMxFIXv1L86Vq1rN8EiuCozbnQpuHFZwbZCO5RM5k4bmskMyR2hDH0BF25EfC93vo3pz0JbDwQ+zknIvSculLQUBN9ebWd3b/+gfugfNfzjk9Nmo2fz0gjsilzl5jnmFpXU2CVJCp8LgzyLFfbj6f0i77+gsTLXTzQrMMr4WMtUCk7O6oyaraAdLMW2IVxDC9YaNb+GSS7KDDUJxa0dhEFBUcUNSaFw7g9LiwUXUz7GgUPNM7RRtRxzzi6dk7A0N+5oYkv394uKZ9bOstjdzDhN7Ga2MP/LBiWlt1EldVESarH6KC0Vo5wtdmaJNChIzRxwYaSblYkJN1yQa8Z3HYSbG29D77odBu3wMYA6nMMFXEEIN3AHD9CBLghI4BXevYn35n2suqp569LO4I+8zx84xIo4</latexit>
sha1_base64="X7LC1tMI51Dgj+1XvadQ7ANYMK8=">AAACB3icbZDLSsNAGIX/eK21anTrZmoRWpCSuNGl4MaNUMFeIAlhMp20QycXZiaFEvIMbnwVNy4U8Q3c+TZO2i609cDAxzkzzP+fIOVMKsv6NjY2t7Z3dit71f3aweGReVzrySQThHZJwhMxCLCknMW0q5jidJAKiqOA034wuS3z/pQKyZL4Uc1S6kV4FLOQEay05Zstx607boTVmGCe3xfNOQdhnhWtC3eKRTpmvu25dc83G1bbmgutg72EBizV8c0vd5iQLKKxIhxL6dhWqrwcC8UIp0XVzSRNMZngEXU0xjii0svnKxXoXDtDFCZCn1ihufv7RY4jKWdRoG+WA8vVrDT/y5xMhddezuI0UzQmi4/CjCOVoLIfNGSCEsVnGjARTM+KyBgLTJRusapLsFdXXofeZdu22vaDBRU4hTNogg1XcAN30IEuEHiCF3iDd+PZeDU+FnVtGMveTuCPjM8fv8Gb2w==</latexit>
sha1_base64="1YsUvd8MFRP7wHDcbumXqwQXLFA=">AAACEnicbZDLSsNAFIYn9VbrLerSTWoRWpCSuNFl0Y0boYK9QBLCZDpph04mYWZSKCHP4MZXceNCEbeu3Pk2TtIstPWHgY//nMOc8/sxJUKa5rdWWVvf2Nyqbtd2dvf2D/TDo76IEo5wD0U04kMfCkwJwz1JJMXDmGMY+hQP/OlNXh/MMBckYg9yHmM3hGNGAoKgVJant2ynbjshlBMEaXqXNQv2gzTJWufODPJ4QjzLdequpzfMtlnIWAWrhAYo1fX0L2cUoSTETCIKhbAtM5ZuCrkkiOKs5iQCxxBN4RjbChkMsXDT4qTMOFPOyAgirh6TRuH+nkhhKMQ89FVnvrBYruXmfzU7kcGVmxIWJxIztPgoSKghIyPPxxgRjpGkcwUQcaJ2NdAEcoikSrGmQrCWT16F/kXbMtvWvdnoXJdxVMEJOAVNYIFL0AG3oAt6AIFH8AxewZv2pL1o79rHorWilTPH4I+0zx9/np1U</latexit>

false

-2
39

0

0

5

5

10

10

1

brake

25

20

30

25

-100(b) (speed[t] > 20)
0100[[M(u), '2 ]]

20 15

15

0

30

5

true

0

<latexit sha1_base64="9cpwUIxj3lyDzaFea4y5+jQdeHU=">AAACEnicbZDLSsNAFIYn9VbrLerSzdQitCAlKYIui27cCBXsBZIQJtNJO3RyYWZSKKHP4MZXceNCEbeu3Pk2TtIstPWHgY//nMOc83sxo0IaxrdWWlvf2Nwqb1d2dvf2D/TDo56IEo5JF0cs4gMPCcJoSLqSSkYGMSco8Bjpe5ObrN6fEi5oFD7IWUycAI1C6lOMpLJcvWHZVcsOkBxjxNK7eT1nz0+TeePcniIej6nbcuyq4+o1o2nkgqtgFlADhTqu/mUPI5wEJJSYISEs04ilkyIuKWZkXrETQWKEJ2hELIUhCohw0vykOTxTzhD6EVcvlDB3f0+kKBBiFniqM1tYLNcy87+alUj/yklpGCeShHjxkZ8wKCOY5QOHlBMs2UwBwpyqXSEeI46wVClWVAjm8smr0Gs1TaNp3l/U2tdFHGVwAk5BHZjgErTBLeiALsDgETyDV/CmPWkv2rv2sWgtacXMMfgj7fMHgmadWQ==</latexit>

-1

-100

00

false

5

5

10

4

gear

20 15

2

30

25

30

true

<latexit sha1_base64="aHupGoY6QDxVxSXUxqcFC6iG9Ks=">AAACB3icbVDLSsNAFJ3UV62vqEtBphbBhZSkCLoRim5cVrAPSEKYTCft0MkkzEyUErpz46+4caGIW3/BnX/jpM1CWw9cOJxzL/feEySMSmVZ30ZpaXllda28XtnY3NreMXf3OjJOBSZtHLNY9AIkCaOctBVVjPQSQVAUMNINRte5370nQtKY36lxQrwIDTgNKUZKS7556LhVx42QGgZh9jDxG6duMqTQc6sevIS2b9asujUFXCR2QWqgQMs3v9x+jNOIcIUZktKxrUR5GRKKYkYmFTeVJEF4hAbE0ZSjiEgvm/4xgcda6cMwFrq4glP190SGIinHUaA784vlvJeL/3lOqsILL6M8SRXheLYoTBlUMcxDgX0qCFZsrAnCgupbIR4igbDS0VV0CPb8y4uk06jbVt2+Pas1r4o4yuAAHIETYINz0AQ3oAXaAINH8AxewZvxZLwY78bHrLVkFDP74A+Mzx9VEZem</latexit>

gear

0
0 0
0

5

5

10

100

speed

20

50 == 3))) or ((speed[t] > 20))(c) (not ((gear[t]<latexit sha1_base64="EhrB+eZTLWtmYn4NID52bpFoqPY=">AAACH3icbVDLSsNAFJ3UV62vqEs3U4tQQUpSRF0W3bgRKtgHJCFMppN26OTBzKRQQv/Ejb/ixoUi4q5/4ySNoNUDA2fOuXfm3uPFjAppGHOttLK6tr5R3qxsbe/s7un7B10RJRyTDo5YxPseEoTRkHQklYz0Y05Q4DHS88Y3md+bEC5oFD7IaUycAA1D6lOMpJJc/cKyq5YdIDnCiKV3s3rOPT9NZqdn9gTxeERd01bPfF+ajl11XL1mNIwc8C8xC1IDBdqu/mkPIpwEJJSYISEs04ilkyIuKWZkVrETQWKEx2hILEVDFBDhpPl+M3iilAH0I65OKGGu/uxIUSDENPBUZTa9WPYy8T/PSqR/5aQ0jBNJQrz4yE8YlBHMwoIDygmWbKoIwpyqWSEeIY6wVJFWVAjm8sp/SbfZMI2GeX9ea10XcZTBETgGdWCCS9ACt6ANOgCDR/AMXsGb9qS9aO/ax6K0pBU9h+AXtPkXFJGi+g==</latexit>[[M(u), ⇤I ('1 _ '2 )]]25[[w2 , ]] = 1 speed50[[M(u), '1 _ '2 ]]

15

10

15

10

20 15

25

20

30

false
25

30

(d) alw_[0,30] ((not ((gear[t] == 3))) or ((speed[t] > 20)))

50

true

50

<latexit sha1_base64="KGDpApNciXxZ1mQ/tKu79UJg0ag=">AAACJ3icbVBbS8MwGE29znmr+uhL5xA2kNEOQZ9kzBd9ECa4C7SlpFm6haUXknQ4Sv+NL/4VXwQV0Uf/iVlXQTcPBE7Od0nOcSNKuND1T2VpeWV1bb2wUdzc2t7ZVff2OzyMGcJtFNKQ9VzIMSUBbgsiKO5FDEPfpbjrji6n9e4YM07C4E5MImz7cBAQjyAopOSoF6ZVMi0fiiGCNLlJKxl3vSROqydWM7x3rivWGLJoSBzDktt+LvWqbZVsRy3rNT2DtkiMnJRBjpajvlj9EMU+DgSikHPT0CNhJ5AJgihOi1bMcQTRCA6wKWkAfcztJPOZasdS6WteyOQJhJapvycS6HM+8V3ZOXXB52tT8b+aGQvv3E5IEMUCB2j2kBdTTYTaNDStTxhGgk4kgYgR+VcNDSGDSMhoizIEY97yIunUa4ZeM25Py41mHkcBHIIjUAEGOAMNcAVaoA0QeABP4BW8KY/Ks/KufMxal5R85gD8gfL1Dapypcg=</latexit>

0
0 0
0

National Institute of Informatics, Tokyo, Japan

5

10
5

15
10

0
0

time

36

20

25
15

30
20

25

5

time

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

50

false
30

Bool. sat

0

false

-2
0

100

0

robustness

0

Problem
2nd trial
550[[w1 , ]] = 1

10

15

20

25

(b) (speed[t] > 20)
true

10

15

20

25

true

<latexit sha1_base64="aHupGoY6QDxVxSXUxqcFC6iG9Ks=">AAACB3icbVDLSsNAFJ3UV62vqEtBphbBhZSkCLoRim5cVrAPSEKYTCft0MkkzEyUErpz46+4caGIW3/BnX/jpM1CWw9cOJxzL/feEySMSmVZ30ZpaXllda28XtnY3NreMXf3OjJOBSZtHLNY9AIkCaOctBVVjPQSQVAUMNINRte5370nQtKY36lxQrwIDTgNKUZKS7556LhVx42QGgZh9jDxG6duMqTQc6sevIS2b9asujUFXCR2QWqgQMs3v9x+jNOIcIUZktKxrUR5GRKKYkYmFTeVJEF4hAbE0ZSjiEgvm/4xgcda6cMwFrq4glP190SGIinHUaA784vlvJeL/3lOqsILL6M8SRXheLYoTBlUMcxDgX0qCFZsrAnCgupbIR4igbDS0VV0CPb8y4uk06jbVt2+Pas1r4o4yuAAHIETYINz0AQ3oAXaAINH8AxewZvxZLwY78bHrLVkFDP74A+Mzx9VEZem</latexit>

false

0
0

5

?

2

10

15

20

Hill-climbing algorithm
gets lost!

25

0
0

?

true

false
5

10

15

20

25

time

sample•Falsification of safety properties with boolean connectives⇤I ('1 ^ '2 ), conjunctive• ⇤I ('1 _ '2 ), disjunctive•<latexit sha1_base64="ko5A7HM161LKjPqzsn9LSSf/BcY=">AAACCHicbVDLSsNAFJ3UV62vqEsXBotQNyUpgi5L3eiugn1AE8JkMmmHTmbCzKRYQpdu/BU3LhRx6ye482+cthG09cCFM+fcy9x7goQSqWz7yyisrK6tbxQ3S1vbO7t75v5BW/JUINxCnHLRDaDElDDcUkRR3E0EhnFAcScYXk39zggLSTi7U+MEezHsMxIRBJWWfPPYbfB7/6bijqBIBsR3XApZ+POqnflm2a7aM1jLxMlJGeRo+uanG3KUxpgpRKGUPcdOlJdBoQiieFJyU4kTiIawj3uaMhhj6WWzQybWqVZCK+JCF1PWTP09kcFYynEc6M4YqoFc9Kbif14vVdGllxGWpAozNP8oSqmluDVNxQqJwEjRsSYQCaJ3tdAACoiUzq6kQ3AWT14m7VrVsavO7Xm53sjjKIIjcAIqwAEXoA6uQRO0AAIP4Am8gFfj0Xg23oz3eWvByGcOwR8YH9/0LJlH</latexit><latexit sha1_base64="MmCJ43cd92+X1L3OT0Bd9Lf9u8w=">AAACB3icbVBLSwMxGMzWV62vVY+CBItQL2W3CHos9aK3CvYB3WXJptk2NJssSbZYSm9e/CtePCji1b/gzX9j2q6grQOBycw3JN+ECaNKO86XlVtZXVvfyG8WtrZ3dvfs/YOmEqnEpIEFE7IdIkUY5aShqWaknUiC4pCRVji4mvqtIZGKCn6nRwnxY9TjNKIYaSMF9rFXE/fBTckbIpn0aeB6JvFzqZwFdtEpOzPAZeJmpAgy1AP70+sKnMaEa8yQUh3XSbQ/RlJTzMik4KWKJAgPUI90DOUoJsofz/aYwFOjdGEkpDlcw5n6OzFGsVKjODSTMdJ9tehNxf+8TqqjS39MeZJqwvH8oShlUAs4LQV2qSRYs5EhCEtq/gpxH0mEtamuYEpwF1deJs1K2XXK7u15sVrL6siDI3ACSsAFF6AKrkEdNAAGD+AJvIBX69F6tt6s9/lozsoyh+APrI9vSB+Y6w==</latexit>

National Institute of Informatics, Tokyo, Japan30(d) alw_[0,30] ((not ((gear[t] == 3))) or ((speed[t] > 20)))

50

1

30

(c) (not ((gear[t] == 3))) or ((speed[t] > 20))[[w2 , ]] = 1<latexit sha1_base64="qnMdUekalbx7LgkhmI9/uA/xKSA=">AAACB3icbVDLSsNAFJ3UV62vqEtBphbBhZSMCLoRim5cVrAPSEKZTCft0MkkzEyUErpz46+4caGIW3/BnX/jpM1CqwcuHM65l3vvCRLOlHacL6u0sLi0vFJeraytb2xu2ds7bRWnktAWiXksuwFWlDNBW5ppTruJpDgKOO0Eo6vc79xRqVgsbvU4oX6EB4KFjGBtpJ6973pV14uwHgZhdj/poWMvGTLoe1UfXkDUs2tO3ZkC/iWoIDVQoNmzP71+TNKICk04VspFTqL9DEvNCKeTipcqmmAywgPqGipwRJWfTf+YwEOj9GEYS1NCw6n6cyLDkVLjKDCd+cVq3svF/zw31eG5nzGRpJoKMlsUphzqGOahwD6TlGg+NgQTycytkAyxxESb6ComBDT/8l/SPqkjp45uTmuNyyKOMtgDB+AIIHAGGuAaNEELEPAAnsALeLUerWfrzXqftZasYmYX/IL18Q1Tf5el</latexit>

30

false

-100

1st trial

537

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

30

Multi-armed bandit••

Multi-armed Bandit problem•

Gambler vs a row of slot machines•

Goal: maximize the reward•

exploitation: focus on a “good” one•

exploration: also consider others

Algorithms based on “Reward”•

n machines, k is index of rounds•✏-greedy: relies on a scalar ✏<latexit sha1_base64="ssxxscrscFDuELeuu/+9O0MDmKI=">AAAB73icbVDLSgNBEOyNrxhfUY9eBoPgKeyKoMegF48RzAOSJcxOepMhszPrzKwQQn7CiwdFvPo73vwbJ8keNLGgoajqprsrSgU31ve/vcLa+sbmVnG7tLO7t39QPjxqGpVphg2mhNLtiBoUXGLDciuwnWqkSSSwFY1uZ37rCbXhSj7YcYphQgeSx5xR66R2F1PDhZK9csWv+nOQVRLkpAI56r3yV7evWJagtExQYzqBn9pwQrXlTOC01M0MppSN6AA7jkqaoAkn83un5MwpfRIr7UpaMld/T0xoYsw4iVxnQu3QLHsz8T+vk9n4OpxwmWYWJVssijNBrCKz50mfa2RWjB2hTHN3K2FDqimzLqKSCyFYfnmVNC+qgV8N7i8rtZs8jiKcwCmcQwBXUIM7qEMDGAh4hld48x69F+/d+1i0Frx85hj+wPv8AUzRkCA=</latexit><latexit<latexit sha1_base64="C/G3NfacETgjbTbhtV7RejazcfU=">AAAB8HicbVDLSgNBEOyNrxhfUY9eBoPgKeyKoMegF48RzEOSJcxOZpMh81hmZoWw5Cu8eFDEq5/jzb9xNtmDJhY0FFXddHdFCWfG+v63V1pb39jcKm9Xdnb39g+qh0dto1JNaIsornQ3woZyJmnLMstpN9EUi4jTTjS5zf3OE9WGKflgpwkNBR5JFjOCrZMe+zQxjCtZGVRrft2fA62SoCA1KNAcVL/6Q0VSQaUlHBvTC/zEhhnWlhFOZ5V+amiCyQSPaM9RiQU1YTY/eIbOnDJEsdKupEVz9fdEhoUxUxG5ToHt2Cx7ufif10ttfB1mTCappZIsFsUpR1ah/Hs0ZJoSy6eOYKKZuxWRMdaYWJdRHkKw/PIqaV/UA78e3F/WGjdFHGU4gVM4hwCuoAF30IQWEBDwDK/w5mnvxXv3PhatJa+YOYY/8D5/AIRBkDQ=</latexit><latexit

High probability

Low probability•

UCB1: balance of exploration and exploitation
The number of times
visiting j

National Institute of Informatics, Tokyo, Japan

9

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Case 1. ⇤I ('1 ^ '2 )<latexit sha1_base64="ko5A7HM161LKjPqzsn9LSSf/BcY=">AAACCHicbVDLSsNAFJ3UV62vqEsXBotQNyUpgi5L3eiugn1AE8JkMmmHTmbCzKRYQpdu/BU3LhRx6ye482+cthG09cCFM+fcy9x7goQSqWz7yyisrK6tbxQ3S1vbO7t75v5BW/JUINxCnHLRDaDElDDcUkRR3E0EhnFAcScYXk39zggLSTi7U+MEezHsMxIRBJWWfPPYbfB7/6bijqBIBsR3XApZ+POqnflm2a7aM1jLxMlJGeRo+uanG3KUxpgpRKGUPcdOlJdBoQiieFJyU4kTiIawj3uaMhhj6WWzQybWqVZCK+JCF1PWTP09kcFYynEc6M4YqoFc9Kbif14vVdGllxGWpAozNP8oSqmluDVNxQqJwEjRsSYQCaJ3tdAACoiUzq6kQ3AWT14m7VrVsavO7Xm53sjjKIIjcAIqwAEXoA6uQRO0AAIP4Am8gFfj0Xg23oz3eWvByGcOwR8YH9/0LJlH</latexit>•

Intuition: it suffices that either [[M(u), '1 ]] < 0 or [[M(u), '2 ]] < 0<latexit sha1_base64="Lprmtx+M2WujtIYXSnwMEFkmJZE=">AAACFHicdVDLSsNAFJ34rPVVdelmahEUpUxqaSu4KLpxI1SwKiQhTKYTOzh5MDMplJCPcOOvuHGhiFsX7vwbJ20FFT1w4XDOvdx7jxdzJhVCH8bU9Mzs3Hxhobi4tLyyWlpbv5RRIgjtkohH4trDknIW0q5iitPrWFAceJxeebcnuX81oEKyKLxQw5g6Ab4Jmc8IVlpyS3uWXbbsAKs+wTw9y3ZG3PPTJNvdtwdYxH3mmo5ddo6QW6qg6mGrUas3IKoi1DRrZk5qzfpBHZpayVEBE3Tc0rvdi0gS0FARjqW0TBQrJ8VCMcJpVrQTSWNMbvENtTQNcUClk46eyuC2VnrQj4SuUMGR+n0ixYGUw8DTnfnJ8reXi395VqL8lpOyME4UDcl4kZ9wqCKYJwR7TFCi+FATTATTt0LSxwITpXMs6hC+PoX/k8ta1URV87xeaR9P4iiATbAFdoAJmqANTkEHdAEBd+ABPIFn4954NF6M13HrlDGZ2QA/YLx9Au22nho=</latexit><latexit sha1_base64="5UxP2k2NKNcYBEGxD1cId4kII8g=">AAACFHicdVDLSsNAFJ34rPVVdelmahEUpUxiaSu4KLpxIyhYFZIQJtOJHZw8mJkUSshHuPFX3LhQxK0Ld/6Nk1pBRQ9cOJxzL/fe4yecSYXQuzExOTU9M1uaK88vLC4tV1ZWL2ScCkK7JOaxuPKxpJxFtKuY4vQqERSHPqeX/s1R4V8OqJAsjs7VMKFuiK8jFjCClZa8yo7tVG0nxKpPMM9O8q0R94Mszbd3nQEWSZ95lutU3QPkVWqovt9uWo0mRHWEWqZlFsRqNfYa0NRKgRoY49SrvDm9mKQhjRThWErbRIlyMywUI5zmZSeVNMHkBl9TW9MIh1S62eipHG5qpQeDWOiKFByp3ycyHEo5DH3dWZwsf3uF+JdnpypouxmLklTRiHwuClIOVQyLhGCPCUoUH2qCiWD6Vkj6WGCidI5lHcLXp/B/cmHVTVQ3zxq1zuE4jhJYBxtgC5igBTrgGJyCLiDgFtyDR/Bk3BkPxrPx8tk6YYxn1sAPGK8f70CeGw==</latexit>'1<latexit sha1_base64="HCaa2KJbduncIFrRI9xRJIsZ4SI=">AAAB8HicbVDLSgNBEOz1GeMr6tHLYBA8hV0R9Bj04jGCeUiyhN7JJBkyM7vMzAbCkq/w4kERr36ON//GSbIHTSxoKKq66e6KEsGN9f1vb219Y3Nru7BT3N3bPzgsHR03TJxqyuo0FrFuRWiY4IrVLbeCtRLNUEaCNaPR3cxvjpk2PFaPdpKwUOJA8T6naJ301BmjToa8G3RLZb/iz0FWSZCTMuSodUtfnV5MU8mUpQKNaQd+YsMMteVUsGmxkxqWIB3hgLUdVSiZCbP5wVNy7pQe6cfalbJkrv6eyFAaM5GR65Roh2bZm4n/ee3U9m/CjKsktUzRxaJ+KoiNyex70uOaUSsmjiDV3N1K6BA1UusyKroQguWXV0njshL4leDhqly9zeMowCmcwQUEcA1VuIca1IGChGd4hTdPey/eu/exaF3z8pkT+APv8welppBK</latexit>'2<latexit sha1_base64="V+2dlzvgn+wvRAsSqZr7cI73/eQ=">AAAB8HicbVBNSwMxEJ3Ur1q/qh69BIvgqewWQY9FLx4r2A9pl5JNs21okl2SbKEs/RVePCji1Z/jzX9j2u5BWx8MPN6bYWZemAhurOd9o8LG5tb2TnG3tLd/cHhUPj5pmTjVlDVpLGLdCYlhgivWtNwK1kk0IzIUrB2O7+Z+e8K04bF6tNOEBZIMFY84JdZJT70J0cmI92v9csWregvgdeLnpAI5Gv3yV28Q01QyZakgxnR9L7FBRrTlVLBZqZcalhA6JkPWdVQRyUyQLQ6e4QunDHAUa1fK4oX6eyIj0pipDF2nJHZkVr25+J/XTW10E2RcJallii4XRanANsbz7/GAa0atmDpCqObuVkxHRBNqXUYlF4K/+vI6adWqvlf1H64q9ds8jiKcwTlcgg/XUId7aEATKEh4hld4Qxq9oHf0sWwtoHzmFP4Aff4ApyqQSw==</latexit>•

Run hill-climbing optimization on two machines•

Schedule them with MAB solvers••✏ -greedy, UCB1, etc.
<latexit sha1_base64="ssxxscrscFDuELeuu/+9O0MDmKI=">AAAB73icbVDLSgNBEOyNrxhfUY9eBoPgKeyKoMegF48RzAOSJcxOepMhszPrzKwQQn7CiwdFvPo73vwbJ8keNLGgoajqprsrSgU31ve/vcLa+sbmVnG7tLO7t39QPjxqGpVphg2mhNLtiBoUXGLDciuwnWqkSSSwFY1uZ37rCbXhSj7YcYphQgeSx5xR66R2F1PDhZK9csWv+nOQVRLkpAI56r3yV7evWJagtExQYzqBn9pwQrXlTOC01M0MppSN6AA7jkqaoAkn83un5MwpfRIr7UpaMld/T0xoYsw4iVxnQu3QLHsz8T+vk9n4OpxwmWYWJVssijNBrCKz50mfa2RWjB2hTHN3K2FDqimzLqKSCyFYfnmVNC+qgV8N7i8rtZs8jiKcwCmcQwBXUIM7qEMDGAh4hld48x69F+/d+1i0Frx85hj+wPv8AUzRkCA=</latexit><latexit

Reward: hill-climbing gain

k: rounds played

Intuition: the morerobustness decrease, the more
promising it is
National Institute of Informatics, Tokyo, Japan

39

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Case 2. ⇤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>•

Not as straightforward as Case 1•

Assumption: it is trivial to falsify only '1 or '2<latexit sha1_base64="HCaa2KJbduncIFrRI9xRJIsZ4SI=">AAAB8HicbVDLSgNBEOz1GeMr6tHLYBA8hV0R9Bj04jGCeUiyhN7JJBkyM7vMzAbCkq/w4kERr36ON//GSbIHTSxoKKq66e6KEsGN9f1vb219Y3Nru7BT3N3bPzgsHR03TJxqyuo0FrFuRWiY4IrVLbeCtRLNUEaCNaPR3cxvjpk2PFaPdpKwUOJA8T6naJ301BmjToa8G3RLZb/iz0FWSZCTMuSodUtfnV5MU8mUpQKNaQd+YsMMteVUsGmxkxqWIB3hgLUdVSiZCbP5wVNy7pQe6cfalbJkrv6eyFAaM5GR65Roh2bZm4n/ee3U9m/CjKsktUzRxaJ+KoiNyex70uOaUSsmjiDV3N1K6BA1UusyKroQguWXV0njshL4leDhqly9zeMowCmcwQUEcA1VuIca1IGChGd4hTdPey/eu/exaF3z8pkT+APv8welppBK</latexit><latexit sha1_base64="V+2dlzvgn+wvRAsSqZr7cI73/eQ=">AAAB8HicbVBNSwMxEJ3Ur1q/qh69BIvgqewWQY9FLx4r2A9pl5JNs21okl2SbKEs/RVePCji1Z/jzX9j2u5BWx8MPN6bYWZemAhurOd9o8LG5tb2TnG3tLd/cHhUPj5pmTjVlDVpLGLdCYlhgivWtNwK1kk0IzIUrB2O7+Z+e8K04bF6tNOEBZIMFY84JdZJT70J0cmI92v9csWregvgdeLnpAI5Gv3yV28Q01QyZakgxnR9L7FBRrTlVLBZqZcalhA6JkPWdVQRyUyQLQ6e4QunDHAUa1fK4oX6eyIj0pipDF2nJHZkVr25+J/XTW10E2RcJallii4XRanANsbz7/GAa0atmDpCqObuVkxHRBNqXUYlF4K/+vI6adWqvlf1H64q9ds8jiKcwTlcgg/XUId7aEATKEh4hld4Qxq9oHf0sWwtoHzmFP4Aff4ApyqQSw==</latexit>•

Robustness restricted to S : [[M(u), ']]SS ✓ [0, T ]<latexit sha1_base64="UUihRRRWgqRHJIqtQNGTJN/yvV0=">AAAB6HicbVBNS8NAEJ3Ur1q/qh69LBbBU0lE0GPRi8cW7Qe0oWy2k3btZhN2N0IJ/QVePCji1Z/kzX/jts1BWx8MPN6bYWZekAiujet+O4W19Y3NreJ2aWd3b/+gfHjU0nGqGDZZLGLVCahGwSU2DTcCO4lCGgUC28H4dua3n1BpHssHM0nQj+hQ8pAzaqzUuO+XK27VnYOsEi8nFchR75e/eoOYpRFKwwTVuuu5ifEzqgxnAqelXqoxoWxMh9i1VNIItZ/ND52SM6sMSBgrW9KQufp7IqOR1pMosJ0RNSO97M3E/7xuasJrP+MySQ1KtlgUpoKYmMy+JgOukBkxsYQyxe2thI2ooszYbEo2BG/55VXSuqh6btVrXFZqN3kcRTiBUzgHD66gBndQhyYwQHiGV3hzHp0X5935WLQWnHzmGP7A+fwBriWM1w==</latexit><latexit<latexit sha1_base64="uDPRfO43fFttS26XXaIx5FVgoKg=">AAACEnicbZDLSsNAFIYn9VbrLerSTWoRWpCSiKDLohs3QkV7gSSEyXTSDp1MwsykUEKfwY2v4saFIm5dufNtnKRZaOsPAx//OYc55/djSoQ0zW+ttLK6tr5R3qxsbe/s7un7B10RJRzhDopoxPs+FJgShjuSSIr7Mccw9Cnu+ePrrN6bYC5IxB7kNMZuCIeMBARBqSxPb9hO1XZCKEcI0vR2Vs/ZD9Jk1jh1JpDHI+I6Vde79/Sa2TRzGctgFVADhdqe/uUMIpSEmElEoRC2ZcbSTSGXBFE8qziJwDFEYzjEtkIGQyzcND9pZpwoZ2AEEVePSSN3f0+kMBRiGvqqM1tYLNYy87+ancjg0k0JixOJGZp/FCTUkJGR5WMMCMdI0qkCiDhRuxpoBDlEUqVYUSFYiycvQ/esaZlN6+681roq4iiDI3AM6sACF6AFbkAbdAACj+AZvII37Ul70d61j3lrSStmDsEfaZ8/tJSdeg==</latexit><latexit sha1_base64="LMAK45tkWVMSxGRBwHgIvknJr1w=">AAAB+XicbVDLSgNBEJyNrxhfqx69DAbBg4RdEfQY9OIxYl6QLGF20psMmX040xsIS/7EiwdFvPon3vwbJ8keNLGgoajqprvLT6TQ6DjfVmFtfWNzq7hd2tnd2z+wD4+aOk4VhwaPZazaPtMgRQQNFCihnShgoS+h5Y/uZn5rDEqLOKrjJAEvZINIBIIzNFLPth+7OvU1IDzRjnNR93p22ak4c9BV4uakTHLUevZXtx/zNIQIuWRad1wnQS9jCgWXMC11Uw0J4yM2gI6hEQtBe9n88ik9M0qfBrEyFSGdq78nMhZqPQl90xkyHOplbyb+53VSDG68TERJihDxxaIglRRjOouB9oUCjnJiCONKmFspHzLFOJqwSiYEd/nlVdK8rLhOxX24Kldv8ziK5IScknPikmtSJfekRhqEkzF5Jq/kzcqsF+vd+li0Fqx85pj8gfX5A4vWku4=</latexit>

Key insight:

•

t
S
=
{t
✓
[0,
T
]|[[M(u), '1 ]] < 0}Let<latexit sha1_base64="s3jSsyfZuao2qyJWrFaxpNuDuQE=">AAACLXicbZDLSiNBFIarHa/xlnGWbkqDoCChWwRdjBAcF24ERaNCVxuqK6eTwuqLVacDoadfyI2vIoILZZitr2ElZuHth4KP/5xDnfOHmZIGXffJGfsxPjE5NT1TmZ2bX1is/lw6N2muBTRFqlJ9GXIDSibQRIkKLjMNPA4VXITXfwb1ix5oI9PkDPsZBDHvJDKSgqO1WtWD0z1WIDN5aADhxnc3z4K/PlvxWcyxK7gqjsr1IYdRkZcbV7hJWY/rrCtbXsBWgt8uK1vVmlt3h6JfwRtBjYx03Ko+sHYq8hgSFIob43tuhkHBNUqhoKyw3EDGxTXvgG8x4TGYoBheW9I167RplGr7EqRD9/1EwWNj+nFoOwd7m8+1gfldzc8x2g0KmWQ5QiLePopyRTGlg+hoW2oQqPoWuNDS7kpFl2su0AZcsSF4n0/+Cudbdc+teyfbtcb+KI5pskxWyTrxyA5pkENyTJpEkFtyT57Is3PnPDr/nP9vrWPOaOYX+SDn5RVZSqgk</latexit>[[M(u), '2 ]]S < 0 implies [[M(u), ⇤I ('1 _ '2 )]] < 0<latexit sha1_base64="eDxmvL8/CSSP0ZojM+ld7BQpgKQ=">AAACFnicbZDLSsNAFIYn9VbrLerSTWoRKmhJiqALF0U3boSK9gJJCJPppB06uTAzKZSQp3Djq7hxoYhbcefbOEmz0NYfBj7+cw5zzu9GlHCh699KaWl5ZXWtvF7Z2Nza3lF397o8jBnCHRTSkPVdyDElAe4IIijuRwxD36W4546vs3pvghknYfAgphG2fTgMiEcQFNJy1FPTqpqWD8UIQZrcpvWcXS+J0+MTawJZNCJO07aqtnN/qTtqTW/oubRFMAqogUJtR/2yBiGKfRwIRCHnpqFHwk4gEwRRnFasmOMIojEcYlNiAH3M7SQ/K9WOpDPQvJDJFwgtd39PJNDnfOq7sjNbms/XMvO/mhkL78JOSBDFAgdo9pEXU02EWpaRNiAMI0GnEiBiRO6qoRFkEAmZZEWGYMyfvAjdZsPQG8bdWa11VcRRBgfgENSBAc5BC9yANugABB7BM3gFb8qT8qK8Kx+z1pJSzOyDP1I+fwAHsp6f</latexit><latexit sha1_base64="0piSGsvIy3oQLl2pRtbkIXZbZLk=">AAACKnicbVDLSgMxFM3UV62vUZduUovQgpSZIujCRa0bXQgV7ANmhiGTZtrQzIMkUyxDv8eNv+KmC6W49UNMH4K23tXJOffe3HO8mFEhDWOiZdbWNza3stu5nd29/QP98KgpooRj0sARi3jbQ4IwGpKGpJKRdswJCjxGWl7/dqq3BoQLGoVPchgTJ0DdkPoUI6koV7+x7LxlB0j2MGLpw6g4w56fJqPSuV2Lnt37oj1APO5R17TVNvjzqpQcO+9cG65eMMrGrOAqMBegABZVd/Wx3YlwEpBQYoaEsEwjlk6KuKSYkVHOTgSJEe6jLrEUDFFAhJPOrI7gmWI60Fd3+FEo4Yz9PZGiQIhh4KnOqRGxrE3J/zQrkf6Vk9IwTiQJ8fwjP2FQRnCaG+xQTrBkQwUQ5lTdCnEPcYSlSjenQjCXLa+CZqVsGmXz8aJQrS3iyIITcAqKwASXoAruQB00AAYv4A28gw/tVRtrE+1z3prRFjPH4E9pX98wtaZy</latexit>

Intuition: it suffices that•either [[M(u), '1 ]]S1 < 0'2'1<latexit sha1_base64="lq8tqR9hW4L2nJDsrVkR3x3s8H8=">AAACGnicbZDLSsNAFIYn9VbrLerSTWoRKkjJiKALF0U3boSK9gJJCJPppB06uTAzKZSQ53Djq7hxoYg7cePbOEm70NYfBj7+cw5zzu/FjAppmt9aaWl5ZXWtvF7Z2Nza3tF39zoiSjgmbRyxiPc8JAijIWlLKhnpxZygwGOk642u83p3TLigUfggJzFxAjQIqU8xkspydWjZVcsOkBxixNLbrF6w56dJdnxijxGPh9SFjl113PTehdml6eo1s2EWMhYBzqAGZmq5+qfdj3ASkFBihoSwoBlLJ0VcUsxIVrETQWKER2hALIUhCohw0uK0zDhSTt/wI65eKI3C/T2RokCISeCpznxxMV/Lzf9qViL9CyelYZxIEuLpR37CDBkZeU5Gn3KCJZsoQJhTtauBh4gjLFWaFRUCnD95ETqnDWg24N1ZrXk1i6MMDsAhqAMIzkET3IAWaAMMHsEzeAVv2pP2or1rH9PWkjab2Qd/pH39ADKXoE4=</latexit><latexit sha1_base64="HCaa2KJbduncIFrRI9xRJIsZ4SI=">AAAB8HicbVDLSgNBEOz1GeMr6tHLYBA8hV0R9Bj04jGCeUiyhN7JJBkyM7vMzAbCkq/w4kERr36ON//GSbIHTSxoKKq66e6KEsGN9f1vb219Y3Nru7BT3N3bPzgsHR03TJxqyuo0FrFuRWiY4IrVLbeCtRLNUEaCNaPR3cxvjpk2PFaPdpKwUOJA8T6naJ301BmjToa8G3RLZb/iz0FWSZCTMuSodUtfnV5MU8mUpQKNaQd+YsMMteVUsGmxkxqWIB3hgLUdVSiZCbP5wVNy7pQe6cfalbJkrv6eyFAaM5GR65Roh2bZm4n/ee3U9m/CjKsktUzRxaJ+KoiNyex70uOaUSsmjiDV3N1K6BA1UusyKroQguWXV0njshL4leDhqly9zeMowCmcwQUEcA1VuIca1IGChGd4hTdPey/eu/exaF3z8pkT+APv8welppBK</latexit><latexit sha1_base64="V+2dlzvgn+wvRAsSqZr7cI73/eQ=">AAAB8HicbVBNSwMxEJ3Ur1q/qh69BIvgqewWQY9FLx4r2A9pl5JNs21okl2SbKEs/RVePCji1Z/jzX9j2u5BWx8MPN6bYWZemAhurOd9o8LG5tb2TnG3tLd/cHhUPj5pmTjVlDVpLGLdCYlhgivWtNwK1kk0IzIUrB2O7+Z+e8K04bF6tNOEBZIMFY84JdZJT70J0cmI92v9csWregvgdeLnpAI5Gv3yV28Q01QyZakgxnR9L7FBRrTlVLBZqZcalhA6JkPWdVQRyUyQLQ6e4QunDHAUa1fK4oX6eyIj0pipDF2nJHZkVr25+J/XTW10E2RcJallii4XRanANsbz7/GAa0atmDpCqObuVkxHRBNqXUYlF4K/+vI6adWqvlf1H64q9ds8jiKcwTlcgg/XUId7aEATKEh4hld4Qxq9oHf0sWwtoHzmFP4Aff4ApyqQSw==</latexit>or [[M(u), '2 ]]S2 < 0<latexit sha1_base64="pZtXH0qxmgubYq53u5PXmeefRgY=">AAACGnicbZDLSsNAFIYn9VbrLerSzdQiVJCSFEEXLopu3AgV7QWSECbTSTt0cmFmUighz+HGV3HjQhF34sa3cZJ2odUfBj7+cw5zzu/FjAppGF9aaWl5ZXWtvF7Z2Nza3tF397oiSjgmHRyxiPc9JAijIelIKhnpx5ygwGOk542v8npvQrigUXgvpzFxAjQMqU8xkspyddOyq5YdIDnCiKU3Wb1gz0+T7PjEniAej6jbdOyq46Z3bjO7MFy9ZjSMQvAvmHOogbnarv5hDyKcBCSUmCEhLNOIpZMiLilmJKvYiSAxwmM0JJbCEAVEOGlxWgaPlDOAfsTVCyUs3J8TKQqEmAae6swXF4u13PyvZiXSP3dSGsaJJCGefeQnDMoI5jnBAeUESzZVgDCnaleIR4gjLFWaFRWCuXjyX+g2G6bRMG9Pa63LeRxlcAAOQR2Y4Ay0wDVogw7A4AE8gRfwqj1qz9qb9j5rLWnzmX3wS9rnNzWuoFA=</latexit>t

Si = {t 2 [0, T ]|[[M(u ), 'ī ]] < 0}<latexit sha1_base64="Is4GgGsZ0MALbThGyW7399WFboI=">AAACM3icbZBNSxxBEIZ7TDRm/dqYYy6ti6Agy4wEkkMEiZcQEBRdFabHoaa3Z7exp2forhGWzvynXPwjOQRCDhHxmv+Q3nUP8eOFhoe3quiqN6uUtBiGv4KZFy9n517Nv24tLC4tr7TfrJ7asjZc9HipSnOegRVKatFDiUqcV0ZAkSlxll3uj+tnV8JYWeoTHFUiKWCgZS45oLfS9tfjVNJdyhwyqeNw+yT5FrO1mBWAQw7KHTSbE85yVzcXuLVN2RWYaihTxzIwTjZNwtaSTyFr0nYn7IYT0acQTaFDpjpM2z9Yv+R1ITRyBdbGUVhh4sCg5Eo0LVZbUQG/hIGIPWoohE3c5OaGbninT/PS+KeRTtz/JxwU1o6KzHeO97ePa2PzuVpcY/4xcVJXNQrN7z/Ka0WxpOMAaV8awVGNPAA30u9K+RAMcPQxt3wI0eOTn8LpTjcKu9HR+87e52kc8+QdWSebJCIfyB75Qg5Jj3Dynfwkf8hNcB38Dm6Du/vWmWA685Y8UPD3H/Wbqow=</latexit>

National Institute of Informatics, Tokyo, Japan

40

when

i = 1, ī = 2
i = 2, ī = 1<latexit sha1_base64="x/HVFlkYIRjmF7ZMn8WCiWMuuqU=">AAAB+3icbVDLSsNAFL2pr1pfsS7dDBbBhZSkCLoRim5cVrAPaEOZTCft0MkkzEzEEvIrblwo4tYfceffOGmz0NYDF86ccy9z7/FjzpR2nG+rtLa+sblV3q7s7O7tH9iH1Y6KEklom0Q8kj0fK8qZoG3NNKe9WFIc+px2/elt7ncfqVQsEg96FlMvxGPBAkawNtLQrjJ0jdxzNPCxTFlmHo2hXXPqzhxolbgFqUGB1tD+GowikoRUaMKxUn3XibWXYqkZ4TSrDBJFY0ymeEz7hgocUuWl890zdGqUEQoiaUpoNFd/T6Q4VGoW+qYzxHqilr1c/M/rJzq48lIm4kRTQRYfBQlHOkJ5EGjEJCWazwzBRDKzKyITLDHRJq6KCcFdPnmVdBp116m79xe15k0RRxmO4QTOwIVLaMIdtKANBJ7gGV7hzcqsF+vd+li0lqxi5gj+wPr8AeCLkmM=</latexit>

when<latexit sha1_base64="vRhCjXD59o59vVm1RkKRecz/7UM=">AAAB+3icbVDLSsNAFL2pr1pfsS7dDBbBhZSkCLoRim5cVrAPaEOZTCft0MkkzEzEEvIrblwo4tYfceffOGmz0NYDF86ccy9z7/FjzpR2nG+rtLa+sblV3q7s7O7tH9iH1Y6KEklom0Q8kj0fK8qZoG3NNKe9WFIc+px2/elt7ncfqVQsEg96FlMvxGPBAkawNtLQrjJ0jRrnaOBjmbLMPNyhXXPqzhxolbgFqUGB1tD+GowikoRUaMKxUn3XibWXYqkZ4TSrDBJFY0ymeEz7hgocUuWl890zdGqUEQoiaUpoNFd/T6Q4VGoW+qYzxHqilr1c/M/rJzq48lIm4kRTQRYfBQlHOkJ5EGjEJCWazwzBRDKzKyITLDHRJq6KCcFdPnmVdBp116m79xe15k0RRxmO4QTOwIVLaMIdtKANBJ7gGV7hzcqsF+vd+li0lqxi5gj+wPr8AeCYkmM=</latexit>

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Experimental evaluation•

Benchmark set 1: efficacy and efficiency•

Simulink models & specifications:••

Automatic transmission [Hoxha et al. ARCH’15]•

Abstract fuel control [Jin et al. HSCC’14]•

NARMA-L2 neurocontroller [Beale et al. ’92]

Algorithms:•

Breach (with CMA-ES)•

MAB- ✏-greedy

General boolean
connectives, not necessarily
with scale problem<latexit sha1_base64="ssxxscrscFDuELeuu/+9O0MDmKI=">AAAB73icbVDLSgNBEOyNrxhfUY9eBoPgKeyKoMegF48RzAOSJcxOepMhszPrzKwQQn7CiwdFvPo73vwbJ8keNLGgoajqprsrSgU31ve/vcLa+sbmVnG7tLO7t39QPjxqGpVphg2mhNLtiBoUXGLDciuwnWqkSSSwFY1uZ37rCbXhSj7YcYphQgeSx5xR66R2F1PDhZK9csWv+nOQVRLkpAI56r3yV7evWJagtExQYzqBn9pwQrXlTOC01M0MppSN6AA7jkqaoAkn83un5MwpfRIr7UpaMld/T0xoYsw4iVxnQu3QLHsz8T+vk9n4OpxwmWYWJVssijNBrCKz50mfa2RWjB2hTHN3K2FDqimzLqKSCyFYfnmVNC+qgV8N7i8rtZs8jiKcwCmcQwBXUIM7qEMDGAh4hld48x69F+/d+1i0Frx85hj+wPv8AUzRkCA=</latexit><latexit••

MAB-UCBMisc:•

30 trials for each•

Timeout: 600s•

HC: CMA-ES

National Institute of Informatics, Tokyo, Japan

41

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Breachsuccess rate•

MAB-UCB<latexit sha1_base64="7SVxXIh8rW9DOBcOGEhTn8dG9b8=">AAAB73icdVBNS8NAEN3Ur1q/qh69LBbBU0hEqL0VvXisYD+gDWWznbRLN7txdyOU0D/hxYMiXv073vw3btMIKvpg4PHeDDPzwoQzbTzvwymtrK6tb5Q3K1vbO7t71f2DjpapotCmkkvVC4kGzgS0DTMceokCEoccuuH0auF370FpJsWtmSUQxGQsWMQoMVbqDSDRjEsxrNY8t5EDL0n9vCANH/uul6OGCrSG1ffBSNI0BmEoJ1r3fS8xQUaUYZTDvDJINSSETskY+pYKEoMOsvzeOT6xyghHUtkSBufq94mMxFrP4tB2xsRM9G9vIf7l9VMTXQQZE0lqQNDloijl2Ei8eB6PmAJq+MwSQhWzt2I6IYpQYyOq2BC+PsX/k86Z63uuf3Nea14WcZTRETpGp8hHddRE16iF2ogijh7QE3p27pxH58V5XbaWnGLmEP2A8/YJIguQsw==</latexit><latexit

success ratetime

success ratetime

RQ1: Which is the best MAB algorithm for our purpose?
•

•

time

MAB- ✏-greedy

MAB-UCB

RQ2: How is the performance of the proposed process•

Generally more effective and efficient compared to Breach•Works very well even on examples free of scale problem

National Institute of Informatics, Tokyo, Japan

42

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Experimental evaluation•

Benchmark set 2: scale problem•

Experiment setting•e.g., Automatic transmission [Hoxha, ARCH’15]

e.g., when scaling speed and k = 3,⇤[0,30] (gear = 3 ! speed > 20000)<latexit sha1_base64="YWFg3o8oB6Tgb4/SHW5n5OHVOrM=">AAACD3icbVDLSgMxFM3UV62vUZdugkWpICXTCrpRSt24rGAf0A4lk962oZkHSUYsQ//Ajb/ixoUibt26829MHwttPRA4nHMvN+d4keBKE/JtpZaWV1bX0uuZjc2t7R17d6+mwlgyqLJQhLLhUQWCB1DVXAtoRBKo7wmoe4PrsV+/B6l4GNzpYQSuT3sB73JGtZHa9nGrHD60kyY5LRJ3lOsBlfgSF1s6xCoC6FwViMFJ286SPJkALxJnRrJohkrb/mp1Qhb7EGgmqFJNh0TaTajUnAkYZVqxgoiyAe1B09CA+qDcZJJnhI+M0sHdUJoXaDxRf28k1Fdq6Htm0qe6r+a9sfif14x198JNeBDFGgI2PdSNBTZpx+XgDpfAtBgaQpnk5q+Y9amkTJsKM6YEZz7yIqkV8g7JO7dn2VJ5VkcaHaBDlEMOOkcldIMqqIoYekTP6BW9WU/Wi/VufUxHU9ZsZx/9gfX5A3Tkmbo=</latexit>

National Institute of Informatics, Tokyo, Japan43

speed*10k

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

BREACH

30

MAB-UCB

23
15
8
0

-2

0

1
AT 15

3

<latexit sha1_base64="zPmKpKB6QoRBxgjGyHZseozwWxw=">AAAB7HicbVBNS8NAEJ3Ur1q/qh69LBbBU0lE0WPVi8cKTVtoQ9lsJ+3SzSbsboRS+hu8eFDEqz/Im//GbZuDtj4YeLw3w8y8MBVcG9f9dgpr6xubW8Xt0s7u3v5B+fCoqZNMMfRZIhLVDqlGwSX6hhuB7VQhjUOBrXB0P/NbT6g0T2TDjFMMYjqQPOKMGiv5tw2vd9UrV9yqOwdZJV5OKpCj3it/dfsJy2KUhgmqdcdzUxNMqDKcCZyWupnGlLIRHWDHUklj1MFkfuyUnFmlT6JE2ZKGzNXfExMaaz2OQ9sZUzPUy95M/M/rZCa6CSZcpplByRaLokwQk5DZ56TPFTIjxpZQpri9lbAhVZQZm0/JhuAtv7xKmhdVz616j5eV2l0eRxFO4BTOwYNrqMED1MEHBhye4RXeHOm8OO/Ox6K14OQzx/AHzucP0zyOBg==</latexit>

BREACH30

MAB-UCB

22.5
15
7.5
0

-2

0

AT 58

1

3

<latexit sha1_base64="GSUk2vN7ifCj6BC074HXF8OK4Jw=">AAAB7HicbVBNS8NAEJ3Ur1q/qh69LBbBU0lEsceqF48VGltoQ9lsJ+3SzSbsboRS+hu8eFDEqz/Im//GbZuDtj4YeLw3w8y8MBVcG9f9dgpr6xubW8Xt0s7u3v5B+fDoUSeZYuizRCSqHVKNgkv0DTcC26lCGocCW+Hobua3nlBpnsimGacYxHQgecQZNVbyb5pXvVqvXHGr7hxklXg5qUCORq/81e0nLItRGiao1h3PTU0wocpwJnBa6mYaU8pGdIAdSyWNUQeT+bFTcmaVPokSZUsaMld/T0xorPU4Dm1nTM1QL3sz8T+vk5moFky4TDODki0WRZkgJiGzz0mfK2RGjC2hTHF7K2FDqigzNp+SDcFbfnmVPF5UPbfqPVxW6rd5HEU4gVM4Bw+uoQ730AAfGHB4hld4c6Tz4rw7H4vWgpPPHMMfOJ8/3eCODQ==</latexit>•

RQ3: Does the proposed approach effectively solve the scale problem?
••—— yes, ours is not subject to the change of the scale.

RQ4: Is the proposed approach more effective than normalization?
•

1
AT
5
——yes, e.g.,
5 is normalized to the same scale, but Breach<latexit sha1_base64="oFSpelcmcLIH15vJGJJcFiqaUDo=">AAAB7nicbVDLSgNBEOyNrxhfUY9eBoPgKeyKQY9RLx4j5AXJGmYnvcmQ2dllZlYIIR/hxYMiXv0eb/6Nk2QPmljQUFR1090VJIJr47rfTm5tfWNzK79d2Nnd2z8oHh41dZwqhg0Wi1i1A6pRcIkNw43AdqKQRoHAVjC6m/mtJ1Sax7Juxgn6ER1IHnJGjZVaN/XKo9er9Iolt+zOQVaJl5ESZKj1il/dfszSCKVhgmrd8dzE+BOqDGcCp4VuqjGhbEQH2LFU0gi1P5mfOyVnVumTMFa2pCFz9ffEhEZaj6PAdkbUDPWyNxP/8zqpCa/9CZdJalCyxaIwFcTEZPY76XOFzIixJZQpbm8lbEgVZcYmVLAheMsvr5LmRdlzy97DZal6m8WRhxM4hXPw4AqqcA81aACDETzDK7w5ifPivDsfi9ack80cwx84nz//CY6t</latexit>

performs badly

National Institute of Informatics, Tokyo, Japan

44

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Conclusion and future work••

Conclusion•

We propose an approach for solving the scale problem•

Multi-armed bandit solver + hill-climbing gain reward•

Experiments show the effectiveness and efficiency

Future work•

Extension to a more general class of STL formula•

Extension to robustness semantics other than the spatial one

Thanks!

National Institute of Informatics, Tokyo, Japan

45

Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Hierarchical Optimization in
Hybrid System Falsification[Zhang, Ernst, Sedwards, Arcaini & Hasuo, EMSOFT’18][Zhang, Hasuo & Arcaini, CAV’19] …

Another example [EMSOFT’18]

more robustly
true

??

true

utilizing time-causal structures

false

for search capabilities,

inputThis way toclimb down :)less so

input

quantitativerobust semantics

Boolean semantics

but also for coverage and exploration
Monte-Carlo Tree Search

Discrete Optim.
Feed search
results backFocus
searchdomain

Domainsequence for
guidingsearchContinuous Optim.
Stochastic gradient descent(simulated annealing, CMA-ES, …)
46

Problem•Falsification problem:M : black-box modelu : input signal (piecewise constant)M(u) : output signal' : specification in Temporal Logic•

Goal: to find a u s.t. M(u) 2 'Example:throttle

speed
60
45
30

⇤[0,30] (speed < 120)
AlwaysBounded-time

Proposition

15
0

0

10

20

30

10

20

30

time
brake

RPM
70
52.5
35
17.5
0

time
National Institute of Informatics, Tokyo, Japan

47

0

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions•

Quantitative robustness semantics of STL [Donze, Maler FORMATS’10]e.g.,' = ⇤[0,30] (speed < 120)<latexit sha1_base64="X60qa9y9hXjW3qtSUsD+SLjhwhI=">AAAB8HicbVBNSwMxEJ2tX7V+VT16CRbBU9kVQS9C0YvHCvZD2qVk02wbmmRDki2Upb/CiwdFvPpzvPlvTNs9aOuDgcd7M8zMixRnxvr+t1dYW9/Y3Cpul3Z29/YPyodHTZOkmtAGSXii2xE2lDNJG5ZZTttKUywiTlvR6G7mt8ZUG5bIRztRNBR4IFnMCLZOeuqOsVZDhm565Ypf9edAqyTISQVy1Hvlr24/Iamg0hKOjekEvrJhhrVlhNNpqZsaqjAZ4QHtOCqxoCbM5gdP0ZlT+ihOtCtp0Vz9PZFhYcxERK5TYDs0y95M/M/rpDa+DjMmVWqpJItFccqRTdDse9RnmhLLJ45gopm7FZEh1phYl1HJhRAsv7xKmhfVwK8GD5eV2m0eRxFO4BTOIYArqME91KEBBAQ8wyu8edp78d69j0VrwctnjuEPvM8fWBuQFw==</latexit>

130

OutputSignals

Quantitative•
Robustness

30

130

120

130

120

97.5

97.5

65

65

65

32.5

32.5

32.5

97.5

0

BooleanSatisfaction

120

0

10

20

30

0

0
0

10

20

30

0

10

20

True

True
Boolean

False

30

Real number-5

National Institute of Informatics, Tokyo, Japan

10

48

30

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions•

falsification => optimization•

robustness

Objective function: [[M, u]]<latexit sha1_base64="FNHFR/j1kusT/N2u2Fn1G8jrWbs=">AAACCnicbVDLSsNAFL3xWesr6tLN1CK4kJKIoMuiGzdCBfuAJJTJdNIOnTyYmQglZO3GX3HjQhG3foE7/8ZJm4W2Hhg4c8693HuPn3AmlWV9G0vLK6tr65WN6ubW9s6uubffkXEqCG2TmMei52NJOYtoWzHFaS8RFIc+p11/fF343QcqJIujezVJqBfiYcQCRrDSUt+sOW7NQW6I1Yhgnt3mp7OPH2Rpjjy35vXNutWwpkCLxC5JHUq0+uaXO4hJGtJIEY6ldGwrUV6GhWKE07zqppImmIzxkDqaRjik0sump+ToWCsDFMRCv0ihqfq7I8OhlJPQ15XFmnLeK8T/PCdVwaWXsShJFY3IbFCQcqRiVOSCBkxQovhEE0wE07siMsICE6XTq+oQ7PmTF0nnrGFbDfvuvN68KuOowCEcwQnYcAFNuIEWtIHAIzzDK7wZT8aL8W58zEqXjLLnAP7A+PwBtXOZoQ==</latexit>•

Goal: min ([[M, u]]) to see if it can be negative<latexit sha1_base64="K8ydQCy1/sHHSzjHJbvi00KB+vQ=">AAACC3icbZDLSsNAFIYn9VbrLerSzbRFqCAlEUGXRTduhAr2Akkok+mkHTqZhJmJUEL3bnwVNy4UcesLuPNtnKRZaOsPAx//OYc55/djRqWyrG+jtLK6tr5R3qxsbe/s7pn7B10ZJQKTDo5YJPo+koRRTjqKKkb6sSAo9Bnp+ZPrrN57IELSiN+raUy8EI04DShGSlsDs9Zw3KoD3RCpMUYsvZ2d5uwHaTKDnlv1TgZm3WpaueAy2AXUQaH2wPxyhxFOQsIVZkhKx7Zi5aVIKIoZmVXcRJIY4QkaEUcjRyGRXprfMoPH2hnCIBL6cQVz9/dEikIpp6GvO7M95WItM/+rOYkKLr2U8jhRhOP5R0HCoIpgFgwcUkGwYlMNCAuqd4V4jATCSsdX0SHYiycvQ/esaVtN++683roq4iiDI1ADDWCDC9ACN6ANOgCDR/AMXsGb8WS8GO/Gx7y1ZBQzh+CPjM8fLeOZ3A==</latexit>

robustness•“Hill-climbing” optimization algorithms•

Decide next sample based on history•

More intelligent than random sampling•Tools: Breach [Donze CAV’10] (CMA-ES, NM, etc.)

sampleS-TALIRO [Annapureddy et al. TACAS’11] (SA etc.)

National Institute of Informatics, Tokyo, Japan49

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions
Time-staging heuristics [Ernst+SNR’18]•

Divide time into many intervals•

Take local optimum of each stage•

Combine them as whole input
…

•

speed

t

National Institute of Informatics, Tokyo, Japan

50

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions
Time-staging heuristics [Ernst+SNR’18]•

Divide time into many intervals•

Take local optimum of each stage•

Combine them as whole input
…

•

speed

t

National Institute of Informatics, Tokyo, Japan

5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions•

Divide time into many intervals•

Take local optimum of each stage•

Combine them as whole input…

Time-staging heuristics [Ernst+SNR’18]

…

•

speed

t

National Institute of Informatics, Tokyo, Japan

5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions•

Divide time into many intervals•

Take local optimum of each stage•

Combine them as whole input…

Time-staging heuristics [Ernst+SNR’18]

…

•

speed

t

National Institute of Informatics, Tokyo, Japan

5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions
Divide time into many intervals•

Take local optimum of each stage•

Combine them as whole input

…

•

…

Time-staging heuristics [Ernst+SNR’18]

…

•

speed

t

National Institute of Informatics, Tokyo, Japan

5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions
Divide time into many intervals•

Take local optimum of each stage•

Combine them as whole input

…

•

…

Time-staging heuristics [Ernst+SNR’18]

…

•

speed

t

National Institute of Informatics, Tokyo, Japan

5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions•

Take local optimum of each stage•

Combine them as whole input……

Divide time into many intervals

…

•

…

Time-staging heuristics [Ernst+SNR’18]

…

•

speed

t

National Institute of Informatics, Tokyo, Japan

5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Existing solutions•

Take local optimum of each stage•

Combine them as whole input……

Divide time into many intervals

…

•

…

Time-staging heuristics [Ernst+SNR’18]

…

•

speed

t

Weakness: How about this situation?
130

120

97.5

65

We need trackback mechanism,

32.5

0

0

10

20

National Institute of Informatics, Tokyo, Japan30

we need a tree-search structure…
5

Zhang, Ernst, Sedwards, Arcaini, Hasuo

•

But…

•

Our search space is infinite…

National Institute of Informatics, Tokyo, Japan

6

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Monte Carlo Tree Search
1
2 3 4

Go game
UCB1•

Pay much attention on “promising” branches•

Playout (simulation) to give each node a reward•

UCB1 [Kocsis+ECML’06] for exploration and exploitation

National Institute of Informatics, Tokyo, Japan

7

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Application of MCTS•

Naive idea of applying MCTS to falsification
1. Divide time
2. Take a value as child
3. Randomly pick child to
do playout …

…

…

…

……

speed

t
•

Challenges•

Q1: How to select children from infinite input space•

Q2: How to define reward•

Q3: How does playout work

National Institute of Informatics, Tokyo, Japan

8

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Q1: Infinite input space
A=

{

,

,

,

}

brake

where
325
162.5

throttle
0 50 100•

Partition input space at each stage•

Treat each sub-region as a child•

Reward evaluates each sub-region

National Institute of Informatics, Tokyo, Japan

9

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Q2: reward
Original MCTS:•v 0 : expanded child<latexit sha1_base64="W27MaUSEXeKSjGyiG9VsBCq4Tb0=">AAAB6XicbVBNS8NAEJ3Ur1q/qh69LBbRU0lE0GPRi8cq9gPaUDbbTbt0swm7k0IJ/QdePCji1X/kzX/jts1BWx8MPN6bYWZekEhh0HW/ncLa+sbmVnG7tLO7t39QPjxqmjjVjDdYLGPdDqjhUijeQIGStxPNaRRI3gpGdzO/NebaiFg94SThfkQHSoSCUbTS4/i8V664VXcOskq8nFQgR71X/ur2Y5ZGXCGT1JiO5yboZ1SjYJJPS93U8ISyER3wjqWKRtz42fzSKTmzSp+EsbalkMzV3xMZjYyZRIHtjCgOzbI3E//zOimGN34mVJIiV2yxKEwlwZjM3iZ9oTlDObGEMi3srYQNqaYMbTglG4K3/PIqaV5WPbfqPVxVard5HEU4gVO4AA+uoQb3UIcGMAjhGV7hzRk5L86787FoLTj5zDH8gfP5A0O2jSs=</latexit>Q(v 0 ) : winning times<latexit sha1_base64="RAGnjq6uneSYC2LX7Lqj60Tw6ac=">AAAB7HicbVBNTwIxEJ3FL8Qv1KOXRmLEC9k1JnokevEIiQsksCHd0oWGbrtpuyRkw2/w4kFjvPqDvPlvLLAHBV8yyct7M5mZFyacaeO6305hY3Nre6e4W9rbPzg8Kh+ftLRMFaE+kVyqTog15UxQ3zDDaSdRFMchp+1w/DD32xOqNJPiyUwTGsR4KFjECDZW8pvVyeVVv1xxa+4CaJ14OalAjka//NUbSJLGVBjCsdZdz01MkGFlGOF0VuqlmiaYjPGQdi0VOKY6yBbHztCFVQYoksqWMGih/p7IcKz1NA5tZ4zNSK96c/E/r5ua6C7ImEhSQwVZLopSjoxE88/RgClKDJ9agoli9lZERlhhYmw+JRuCt/ryOmld1zy35jVvKvX7PI4inME5VMGDW6jDIzTABwIMnuEV3hzhvDjvzseyteDkM6fwB87nD6pejes=</latexit>

N (v 0 ) : visiting times<latexit sha1_base64="b0RTBbzmVp9K+zHJoAPEz41Awk4=">AAAB7HicbVBNSwMxEJ3Ur1q/qh69BItYL2VXBD0WvXiSCm5baJeSTbNtaDa7JNlCWfobvHhQxKs/yJv/xrTdg7Y+GHi8N8PMvCARXBvH+UaFtfWNza3idmlnd2//oHx41NRxqijzaCxi1Q6IZoJL5hluBGsnipEoEKwVjO5mfmvMlOaxfDKThPkRGUgeckqMlbyH6vj8oleuODVnDrxK3JxUIEejV/7q9mOaRkwaKojWHddJjJ8RZTgVbFrqppolhI7IgHUslSRi2s/mx07xmVX6OIyVLWnwXP09kZFI60kU2M6ImKFe9mbif14nNeGNn3GZpIZJulgUpgKbGM8+x32uGDViYgmhittbMR0SRaix+ZRsCO7yy6ukeVlznZr7eFWp3+ZxFOEETqEKLlxDHe6hAR5Q4PAMr/CGJHpB7+hj0VpA+cwx/AH6/AGlxo3o</latexit>

N (v) : visiting times to<latexit sha1_base64="lyPZIiHwUswFKdLMupVjyM9G22E=">AAAB63icbVBNSwMxEJ2tX7V+VT16CRahXsquFPRY9OJJKtgPaJeSTbNtaJJdkmyhLP0LXjwo4tU/5M1/Y7bdg7Y+GHi8N8PMvCDmTBvX/XYKG5tb2zvF3dLe/sHhUfn4pK2jRBHaIhGPVDfAmnImacsww2k3VhSLgNNOMLnL/M6UKs0i+WRmMfUFHkkWMoJNJj1Up5eDcsWtuQugdeLlpAI5moPyV38YkURQaQjHWvc8NzZ+ipVhhNN5qZ9oGmMywSPas1RiQbWfLm6dowurDFEYKVvSoIX6eyLFQuuZCGynwGasV71M/M/rJSa88VMm48RQSZaLwoQjE6HscTRkihLDZ5Zgopi9FZExVpgYG0/JhuCtvrxO2lc1z615j/VK4zaPowhncA5V8OAaGnAPTWgBgTE8wyu8OcJ5cd6dj2VrwclnTuEPnM8fRK2Ntw==</latexit>

Reward: an estimatedwinning rate

the parent

Our definition:•

R(v 0 ) : robustness<latexit sha1_base64="iG6OAst6t22wZzYjJ56mzQS9GRE=">AAAB7HicbVBNTwIxEJ3iF+IX6tFLIzHihewaEz0SvXhE4wIJbEi3dKGh2920XRKy4Td48aAxXv1B3vw3FtiDgi+Z5OW9mczMCxLBtXGcb1RYW9/Y3Cpul3Z29/YPyodHTR2nijKPxiJW7YBoJrhknuFGsHaiGIkCwVrB6G7mt8ZMaR7LJzNJmB+RgeQhp8RYyXusjs8veuWKU3PmwKvEzUkFcjR65a9uP6ZpxKShgmjdcZ3E+BlRhlPBpqVuqllC6IgMWMdSSSKm/Wx+7BSfWaWPw1jZkgbP1d8TGYm0nkSB7YyIGeplbyb+53VSE974GZdJapiki0VhKrCJ8exz3OeKUSMmlhCquL0V0yFRhBqbT8mG4C6/vEqalzXXqbkPV5X6bR5HEU7gFKrgwjXU4R4a4AEFDs/wCm9Iohf0jj4WrQWUzxzDH6DPH6vmjew=</latexit>

max R(w): the max (worst)<latexit sha1_base64="E0TJfYKFkN8wiSm+xvsYus0hm6c=">AAACBHicbZC7TsMwFIYdrqXcAoxdLCqkslQJQoKxgoWxoN6kJooc12mtOk5kO5QqysDCq7AwgBArD8HG2+C0GaDllyx9+s858jm/HzMqlWV9Gyura+sbm6Wt8vbO7t6+eXDYkVEiMGnjiEWi5yNJGOWkrahipBcLgkKfka4/vs7r3XsiJI14S01j4oZoyGlAMVLa8syKE6IHL504lEONaoQRS1tZdlebnHpm1apbM8FlsAuogkJNz/xyBhFOQsIVZkjKvm3Fyk2RUBQzkpWdRJIY4TEakr5GjkIi3XR2RAZPtDOAQST04wrO3N8TKQqlnIa+7sz3lIu13Pyv1k9UcOmmlMeJIhzPPwoSBlUE80TggAqCFZtqQFhQvSvEIyQQVjq3sg7BXjx5GTpndduq27fn1cZVEUcJVMAxqAEbXIAGuAFN0AYYPIJn8ArejCfjxXg3PuatK0YxcwT+yPj8Aa+XmBg=</latexit>

w2T

Reward: negatively
correlated to robustness

robustness over
the whole tree

National Institute of Informatics, Tokyo, Japan

10

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Q3: playout
…

…

…

…

…
time (d-1)T/K

ud(1)

ud(2)

ud

time dT/K…
ud+1(1)

ud+1(2)time (d+1)T/K

ud+1

ud+2(1)

uK(2)

ud+2
…

uK(1)

…

…

…

Newly
expandedchild

ud+2(2)

RewardJM(u1 . . . uK ), 'K

uKtime T

Playout by hill-climbing optimization•

Goal: evaluate the expanded child•

Steps:•

Collect the sequence of sub-regions from the root to the expanded child•

Include all the input region of the remaining stages•

Run hill-climbing optimization within a timeout

National Institute of Informatics, Tokyo, Japan

11

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Basic Alg.: Two-layered optimization•

Two-layered optimization framework:•

MCTS: decide the directions of the search based on the
reward given by hill-climbing•

Hill-climbing: compute the concrete robustness values of thepath assigned by MCTS

National Institute of Informatics, Tokyo, Japan

12

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Biased Alg.: Progressive widening•

Without progressive widening [Coulom’07]
100 children
in total…
…
100 nodes•

With progressive widening

Expand this only after
expanding all thechildren on 1st level

100 children
in total

C · N (v)↵<latexit sha1_base64="8QeXbNY9k0wlsNjoAjW1TOmrMJg=">AAAB+3icbVBNS8NAEJ34WetXrEcvi0Wol5KIoMdiL56kgv2AJpbNZtsu3WzC7qZYQv+KFw+KePWPePPfuG1z0NYHA4/3ZpiZFyScKe0439ba+sbm1nZhp7i7t39waB+VWipOJaFNEvNYdgKsKGeCNjXTnHYSSXEUcNoORvWZ3x5TqVgsHvQkoX6EB4L1GcHaSD27VPdIGGt0VxmfP3qYJ0Pcs8tO1ZkDrRI3J2XI0ejZX14YkzSiQhOOleq6TqL9DEvNCKfTopcqmmAywgPaNVTgiCo/m98+RWdGCVE/lqaERnP190SGI6UmUWA6I6yHatmbif953VT3r/2MiSTVVJDFon7KkY7RLAgUMkmJ5hNDMJHM3IrIEEtMtImraEJwl19eJa2LqutU3fvLcu0mj6MAJ3AKFXDhCmpwCw1oAoEneIZXeLOm1ov1bn0sWtesfOYY/sD6/AHGiZOd</latexit>

Possible to expand
this node firstly
National Institute of Informatics, Tokyo, Japan

13

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Experimental evaluation••

Evaluated algorithms:•

Breach (Hill-climbing)•

Basic algorithm (MCTS + Hill-climbing)•

Biased algorithm (MCTS + Hill-climbing + progressive widening)

Benchmarks:•

Automatic transmission•

Abstract fuel control•

Free floating robot

National Institute of Informatics, Tokyo, Japan

14

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Experimental evaluation

National Institute of Informatics, Tokyo, Japan

15

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Experimental evaluation
Model: Automatic transmission:
Property:⇤[0,29] (speed < 100) _ ⇤[29,30] (speed > 65)<latexit sha1_base64="P1vh/Xi2QjwrQwoGDbqW+Wsm7M4=">AAACH3icbVDLSgNBEJyNrxhfUY9eBoOQQAizUaMBkRAvHhWMBjZLmJ10kiGzD2Zmg2HJn3jxV7x4UES8+TfuxhV8FTQUVd10dzmB4EoT8m5k5uYXFpeyy7mV1bX1jfzm1rXyQ8mgxXzhy7ZDFQjuQUtzLaAdSKCuI+DGGZ0l/s0YpOK+d6UnAdguHXi8zxnVsdTN1zpN/7YbWaRcrdvTogoAeicmIaXOGACnZrVe3idf7mntsJTr5gukQmbAf4mZkgJKcdHNv3V6Pgtd8DQTVCnLJIG2Iyo1ZwKmuU6oIKBsRAdgxdSjLig7mv03xXux0sN9X8blaTxTv09E1FVq4jpxp0v1UP32EvE/zwp1/9iOuBeEGjz2uagfCqx9nISFe1wC02ISE8okj2/FbEglZTqONAnB/P3yX3JdrZikYl4eFBrNNI4s2kG7qIhMdIQa6BxdoBZi6A49oCf0bNwbj8aL8frZmjHSmW30A8b7B9CAn7A=</latexit>

FA L S I F I C AT I O N R AT E ( N / 1 0 ) our algorithm
10

7 7

7.5

8

7

8

900900900

7our algorithm

TIME (S)767.8 795.4

786.8

675
505.3

4

5

450

2.5

225

0 0

0

313

261.9

208.8

0

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

ED

AS

BI

C
SI

H
C

ED

EA

BA

BR

AS

BI

C
SI

BA

H
C

EA

BR

16

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

National Institute of Informatics, Tokyo, Japan

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Experimental evaluation
Model: Automatic transmission
Property: ⇤[0,30] (rpm < 4700 _ ⇤[0,1] (rpm > 600))<latexit sha1_base64="Jd26TtSHmNyLoMt7zJKNsv1bYiA=">AAACHHicbVBNS0JBFJ1nX2ZfVss2QxIohMxLyRYRYpuWBvkB+pB541UH530wM0+Shz+kTX+lTYsi2rQI+jc99RGlHbhwOOde7r3H9gVXmpAvI7Gyura+kdxMbW3v7O6l9w/qygskgxrzhCebNlUguAs1zbWApi+BOraAhj28nvqNEUjFPfdOj32wHNp3eY8zqiOpky60K959J2yR0wKxJlnpO5fFEiG4PQLAP545t67OCcnlUp10huTJDHiZmDHJoBjVTvqj3fVY4ICrmaBKtUziayukUnMmYJJqBwp8yoa0D62IutQBZYWz5yb4JFK6uOfJqFyNZ+rviZA6So0dO+p0qB6oRW8q/ue1At27sELu+oEGl80X9QKBtYenSeEul8C0GEeEMsmjWzEbUEmZjvKchmAuvrxM6md5k+TN22KmXInjSKIjdIyyyEQlVEY3qIpqiKEH9IRe0KvxaDwbb8b7vDVhxDOH6A+Mz2/xWJ4e</latexit>

our algorithm

FA L S I F I C AT I O N R AT E ( N / 1 0 )10TIME (S)10 10 10

9

900

7 7

7.5
5

3

648.1 624.2

675

3

2.5

0

0

More time!!

900

450

384.4 341.2

225

163.7

80.4

75.5

178.7

0

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

ED

AS

BI

C
SI

H
C

ED

EA

BA

BR

AS

BI

C
SI

BA

H
C

EA

BR

17

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

National Institute of Informatics, Tokyo, Japan

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Experimental evaluation
Model: Free floating robot
Property: ¬⌃[0,5] (x, y 2 [3.9, 4.1] ^ ẋ, ẏ 2 [ 1, 1])<latexit sha1_base64="ZKNx6csbsiwp9tK62hC233dsdTQ=">AAACLXicbVBNS+wwFE196tPxa3wu3yY4CAq1NOrD93aDunCp4KjQliFN74zBNC1JqpbSP+TGvyKCi3mIW/+GmXEWfh0IOZxz703uiXPBtfH9gTPxY3Jq+ufMbGNufmFxqbn861RnhWLQYZnI1HlMNQguoWO4EXCeK6BpLOAsvtwf+mdXoDTP5Ikpc4hS2pe8xxk1Vuo2D0IJ/fCA0zSTSbcKfPdPVK/fuGXIZbDt/XN3PBKF15D0AYdJZqqb2h3dZT2s2CQuiTa6zZbv+SPgr4SMSQuNcdRtPtgZrEhBGiao1gHxcxNVVBnOBNSNsNCQU3ZJ+xBYKmkKOqpG29Z4zSoJ7mXKHmnwSH3fUdFU6zKNbWVKzYX+7A3F77ygML2/UcVlXhiQ7O2hXiGwyfAwOpxwBcyI0hLKFLd/xeyCKsqMDbhhQyCfV/5KTrc84nvkeKfV3hvHMYN+o1W0jgjaRW10iI5QBzF0i+7RAP137pxH58l5fiudcMY9K+gDnJdXJyim1A==</latexit>

TIME (S)FA L S I F I C AT I O N R AT E ( N / 1 0 )10

10

10 10 10

10

7.5

10

900

900
675

6

473.9

450

5

3

338

225 119.8

2.5

0

0

More time!!

273.2
162.2

92.8

390.9

197.4

0

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

ED

AS

BI

C
SI

ED

H
C

AS

EA

BA

BR

BI

C
SI

BA

H
C

EA

BR

18

C

M

SA
M
N
G ES
A-

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

SA
M
N
G ES
A-

M

C

National Institute of Informatics, Tokyo, Japan

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Experimental evaluation•

Our approach improves the falsification rate in most cases•

Sometimes our approach takes more time to find the solution•

MCTS takes more time on exploration and it is acceptable.

National Institute of Informatics, Tokyo, Japan

19

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Conclusion and Future work•

This paper proposes a two-layered framework:•

High level: Monte Carlo Tree Search to guide the search
direction•

Low level: Hill-climbing to do playout to give reward to eachnode•

Experimental evaluation shows that our approach can solve some
hard problems within acceptable time.

•

Future work:•

THANK YOU!

Quantitative coverage metric

National Institute of Informatics, Tokyo, Japan

20

Zhang, Ernst, Sedwards, Arcaini, Hasuo

Verification, Control, Testing, …
Reduction to Optimization
Verification ➜ testingFight complexity. Accommodate black-box systems/models
Rigorous graph algorithms, convex optimization ➜ statistical machine learning
FasterMaybe imprecise. But do we need that much precision?
Formal methods techniques are still important
Formal verification:translation
spec ↦ automaton

Verif.
Problemmodel ↦ prop. formula…

FM-assisted testingtranslation
Often to MDPs
What are costs/
rewards?
What are states?

Testing
Problem
73

Optimization
ProblemSAT
graphreachability
LP, SDP, …

Optimization
Problem
Can be solved
statistically,
this time

Hasuo (NII, Tokyo)

Outline
Cyber-physical systems under uncertainties
Formal methods and testing for CPS
Hybrid system falsification
Logical connectives [CAV’19]
Causality in time [EMSOFT’18]… as demonstration of combining
logical and statistical

Other topics
74

Hasuo (NII, Tokyo)

arXiv:1704.04759v1 [cs.SY] 16 Apr 201

Abstract—We present Component-Based Simplex Architecture(CBSA), a new framework for assuring the runtime safety ofcomponent-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based
CPSs to run advanced, uncertified controllers while still providing
runtime assurance that A-G contracts and global properties are
satisfied. In CBSA, multiple Simplex instances, which can becomposed in a nested, serial or parallel manner, coordinate toassure system-wide properties.
Example: simplex
architecture(right)Combining
A-G reasoning
and the Simplex architecture is achallenging problem that yields significant benefits. By utilizing
AC is
A-G contracts, we are able to compositionally determine theswitching logic for CBSAs, thereby alleviating the state explosion
complex, performance-oriented,
encountered by other approaches. black-box
Another benefit is that we
can use A-G proof rules to decompose the proof of system-wide
BC issafety assurance into sub-proofs corresponding to the componentbased structure of the(hopefully)
system architecture.
We also introduce thesimple, safety-oriented,
white-box
notion of coordinated switching between Simplex instances, a key
component of our compositional approach to reasoning about
CBSA switching logic.
Idea: we can verify
the whole system
We illustrate our framework with a component-based control
system for a ground rover. We formally prove that the CBSA foreven if AC is a black-box!
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides with
Enough to show:
a stationary obstacle). We also consider a CBSA for the roverthat andguarantees
mission completion:
all target destinations visited
safety of BC,
correctnessof DM
within a prescribed amount of time.
Index Terms—Simplex
architecture;
We impose certain
contracts
on AC Assume-guarantee reasoning; Component-based system architecture; Cyber-physicalsystems; Collision avoidanceAs such, Simplex is a very powerful architecture. It assuresthat the plant is properly controlled even if the advanced controller has bugs. As advanced controllers are increasingly more
complex, more adaptive with the use of unverified algorithms
such as machine-learning’s, runtime assurance techniques like
Simplex are becoming more important. Figure 1 illustrates the
Simplex architecture.

Formal Safety Architecture

RelatedI. I NTRODUCTION

FM4AI (ML/AI
components
as AC)
Simplex[1]–[3] is a softwarearchitecture for high-assurance
process-control systems. It traditionally consists of a phys-

Monitoring ical
(checkingcontracts
plant and two
versions of on
the AC)
controller: an advanced

controller (AC) and a baseline controller (BC). The AC isin control
One promising way
to of the plant under nominal operating conditions,and is designed to achieve high-performance according to
make formal verification
down-scalable
certain metrics(e.g., maneuverability, fuel economy, missioncompletion time). The BC is pre-certified to keep the plant
Weaker contractson ACwithin a prescribed safety region, i.e., a region of safe op➜ weaker safetyeration. Aguarantee
decision module(but(DM),hopefully
which is alsonon-zero)pre-certified,continually monitors the state of the plant and 75
switches controlof the plant to the BC should the plant be in imminent danger

Phan
et al.,and
ACSD’17
Fig. 1. The Simplex architecture. The Decision
ModuleBaseline
Controller are pre-certified.

The Simplex architecture was developed 20 years ago. Since
then, control systems have evolved to take on a more complex
structure consisting of multiple controllers, each with a distinct
functionality. For example, an autonomous vehicle might havea hierarchical control system consisting of controllers for (inorder of decreasing level of abstraction) mission-planning,
guidance, navigation, and inner-loop control. A system ofthis form is illustrated in Fig. 2. Furthermore, some of thesecontrollers themselves may have a hierarchical or nested
structure.
Advanced control systems are not necessarily hierarchical,
but are better understood as having a component-based architecture. A “component” may be a software module or the
distinguished physical-plant node (we do not consider multiple
physical plants, because a physical plant can be arbitrarily
complex). It is important to have runtime assurance techniques
for component-based control systems that are equally modular,
to reduce their associated complexity and cost.
Components may have different update periods (or execution periods). For the autonomous-vehicle example, themission-planning component’s update period may be a multi-

arXiv:1704.04759v1 [cs.SY] 16 Apr 20

Abstract—We present Component-Based Simplex Architecture As such, Simplex is a very powerful architecture. It assures(CBSA), a new framework for assuring the runtime safety of that the plant is properly controlled even if the advanced concomponent-based cyber-physical systems (CPSs). CBSA inte- troller has bugs. As advanced controllers are increasingly more
grates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based complex, more adaptive with the use of unverified algorithms
CPSs to run advanced, uncertified controllers while still providing such as machine-learning’s, runtime assurance techniques likeruntime assurance that A-G contracts and global properties are Simplex are becoming more important. Figure 1 illustrates thesatisfied. In CBSA, multiple Simplex instances, which can be Simplex architecture.
composed in a nested, serial or parallel manner, coordinate toassure system-wide properties.
Combining A-G reasoning and the Simplex architecture is achallenging problem that yields significant benefits. By utilizing
A-G contracts, we are able to compositionally determine theswitching logic for CBSAs, thereby alleviating the state explosion
encountered by other approaches. Another benefit is that we
can use A-G proof rules to decompose the proof of system-widesafety assurance into sub-proofs corresponding to the componentbased structure of the system architecture. We also introduce thenotion of coordinated switching between Simplex instances, a key
component of our compositional approach to reasoning about
Phan
et al.,and
ACSD’17
Fig. 1. The Simplex architecture. The Decision
ModuleBaseline[Abrial, CBSA“The switching
Event-B logic.
Book”, 2010 CUP] [Kobayashi+, ICFEM’18]
Controller are pre-certified.
We illustrate our framework with a component-based control
system for a ground rover. We formally prove that the CBSA for
The Simplex architecture was developed 20 years ago. Since
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides with then, control systems have evolved to take on a more complex
a stationary obstacle). We also consider a CBSA for the rover structure consisting of multiple controllers, each with a distinct
that guarantees mission completion: all target destinations visited functionality. For example, an autonomous vehicle might havewithin a prescribed amount of time.
a hierarchical control system consisting of controllers for (inIndex Terms—Simplex architecture; Assume-guarantee reasoning; Component-based system architecture; Cyber-physical order of decreasing level of abstraction) mission-planning,
guidance, navigation, and inner-loop control. A system ofsystems; Collision avoidanceFormal Safety Architecture
At ERATO MMSD:
we formalize, verify and refine
safety architectures

Event-B: a formal modeling language
Based on state transition systems.
A tool Rodin supports:
Safety proofs

Incremental modeling by refinements
Flexibility in choosing model
I NTRODUCTION
fidelity ➜I. down-scaling

Simplex [1]–[3] is a software architecture for high-assurance
process-control
systems. general
It traditionallymodel
consists oftoa physFrom (our)ical plant and two versions of the controller: an advanced(industry
individual
controller(AC) and apartner’s)baseline controller(BC). The AC isin control of the plant under nominal operating conditions,model
and is designed to achieve high-performance according tocertain metrics (e.g., maneuverability, fuel economy, mission76
completion time). The BC is pre-certified to keep the plant

this form is illustrated in Fig. 2. Furthermore, some of thesecontrollers themselves may have a hierarchical or nested
structure.
Advanced control systems are not necessarily hierarchical,
but are better understood as having a component-based architecture. A “component” may be a software module or the
distinguished physical-plant node (we do not consider multiple
physical plants, because a physical plant can be arbitrarily
complex). It is important to have runtime assurance techniques
for component-based control systems that are equally modular,

Pattern Matching against Timed Automata,
Monitoring
Specification“Frequent gear changes within 3 sec after shifting up to 4th”

60
45
30
15
0

Runningsystem

0

10

20

30

Log

Monitor

Runtime verification, monitoring
Not straightforward, esp. when specs involve timing constraints
Speed requirements (GBs of log per second)
Computing resource (embedded)…
Industry needs
Technically: theory of (parametrized) timed automata

Monitoring
result“From 18.9 sec. to
23.2 sec.”

Pattern Matching against Timed Automata,
Monitoring
Specification“Frequent gear changes within 3 sec after shifting up to 4th”

60
45
30
15
0

Runningsystem

0

10

Log

20

30

MonitorMonitoring
result“From 18.9 sec. to
23.2 sec.”

Use cases“Here is 1 PB of log, and I want to extract its relevant parts”“Raise an alert if this specific type of anomaly occurs”

Monitoring: Problem Formulations
Given: a log, discrete time w = abaaacb…bbc
a spec φ”no occurrence of c for 6 steps after b”
Answer: all subsequences of w that satisfy φNontrivial due to temporalcausality

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a spec φ ”no occurrence of c for 6 seconds after b”
Answer: all subsequences of w that satisfy φ[Ulus, CAV’17] [Waga+, FORMATS’17]

Infinitely many such subsequences(starting at t=1? t = 1.01? t = 1.001? …)➜ Efficient representation & computation by zones

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a parametrized spec φ(p)”no occurrence of c for p seconds after b” “b occurs with a period of p seconds”

Answer: all the pairs of (p, (a subseq. of w that satisfies φ)))[Andre+, ICECCS’18] [Waga+, NFM’19] [Waga+, CAV’19] …

In industry, fixing a spec is a big challenge.
Parameters ➜ flexibility in specs
79
Hasuo (NII, Tokyo)

Monitoring: Our Achievements
Efficient algorithm from
Given: a log, discrete time w = abaaacb…bbc
theory of timed automata.
a spec φ”no occurrence of c for 6 steps after b” Processes ~ 1M events/
second (laptop).
Answer: all subsequences of w that satisfy φ[Waga+, FORMATS’17]

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a spec φ ”no occurrence of c for 6 seconds after b”
Answer: all subsequences of w that satisfy φ[Ulus, CAV’17] [Waga+, FORMATS’17]

https://github.com/maswag/monaa

Also implemented onRenesas RH850

Efficient algorithm using parametrized timed automata.
Processes ~ 10K events/second (laptop). [Waga+, NFM’19]
https://github.com/maswag/symon

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a parametrized spec φ(p)”no occurrence of c for p seconds after b” “b occurs with a period of p seconds”

Answer: all the pairs of (p, (a subseq. of w that satisfies φ)))[Andre+, ICECCS’18] [Waga+, NFM’19] [Waga+, CAV’19] …
80

Hasuo (NII, Tokyo)

Outline
Cyber-physical systems under uncertainties
Formal methods and testing for CPS
Hybrid system falsification
Logical connectives [CAV’19]
Causality in time [EMSOFT’18]… as demonstration of combining
logical and statistical

Other topics
81

Hasuo (NII, Tokyo)

Conclusions
Focused on safety-critical CPS withstatistical ML components
Don’t trust statistical AI.
Use them with precaution
System-level safety
Formal methods are not applicable
per se➜ combine logical and statisticalreasoning
Hierarchical optimization in
falsification, as an example
Quality assurance under uncertainties
A scientific and engineering
problem,that is challenging but rewarding!
82

Hasuo (NII, Tokyo)