Bounding Errors Due to Switching Delays
in Incrementally Stable Switched Systems

Kengo Kido

Sean Sedwards

Ichiro Hasuo

Univ. Tokyo
JSPS Research Fellow(Currently TOYOTA)

Univ. Waterloo

National Inst. Informatics
SOKENDAI

Supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and JSPS Grant-in-Aid No. 15K11984. K.K.
is supported by Grant-in-Aid for JSPS Fellows No. 15J05580.
1Outline
The approximate bisimulation workflow
Our use: delays in switched systems
Simper setting ➜ applicability
Technical contributions
Two-step synthesis,
via state-space discretization
Case study
Hasuo (NII, JP) 2

Approximate Bisimulation[Girard & Pappas, IEEE Transactions on Automatic Control’07]

Ti = (Qi , L, !, O, Hi ) for i = 1, 2i(O equipped with a metric d)Def.
R" ✓ Q1 ⇥ Q2 is an εapproximate bisimulation
relation between T1 and T2 if
for all (q1 , q2 ) 2 R" ,

T1

T2

R"
l

l
R"

• d(H1 (q1 ), H2 (q2 ))  ✏
l

l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
1
2
1
2
1 2 ) 2 R"
1
2
l
l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
2
1
2
1
1 2 ) 2 R"
2
1
Hasuo (NII, JP) 3

Approximate Bisimulation[Girard & Pappas, IEEE Transactions on Automatic Control’07]

Ti = (Qi , L, !, O, Hi ) for i = 1, 2i(O equipped with a metric d)Def.
R" ✓ Q1 ⇥ Q2 is an εapproximate bisimulation
relation between T1 and T2 if
for all (q1 , q2 ) 2 R" ,

T1

T2

R"
l

l
R"

• d(H1 (q1 ), H2 (q2 ))  ✏
l

l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
1
2
1
2
1 2 ) 2 R"
1
2
l
l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
2
1
2
1
1 2 ) 2 R"
2
1

Once in a relationship,
always henceforthHasuo (NII, JP) 3

Approximate Bisimulation[Girard & Pappas, IEEE Transactions on Automatic Control’07]

Ti = (Qi , L, !, O, Hi ) for i = 1, 2i(O equipped with a metric d)Def.
R" ✓ Q1 ⇥ Q2 is an εapproximate bisimulation
relation between T1 and T2 if
for all (q1 , q2 ) 2 R" ,

T1

T2

R"
l

l
R"

• d(H1 (q1 ), H2 (q2 ))  ✏
l

l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
1
2
1
2
1 2 ) 2 R"
1
2
l
l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
2
1
2
1
1 2 ) 2 R"
2
1

Once in a relationship,
always henceforthHasuo (NII, JP) 3

Incremental Stability (δ-GUAS)
Incrementally Globally Uniformly Asymptotically StableDef.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)x(y, t)



kx

yk, t

where x(x, ) is the trajectory starting at x.
<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>

Hasuo (NII, JP) 4

Incremental Stability (δ-GUAS)
Incrementally Globally Uniformly Asymptotically StableDef.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)x(y, t)



kx

GAS

yk, t

where x(x, ) is the trajectory starting at x.
<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>

t
δ-GAS

t

Hasuo (NII, JP) 4

• increasing in kx

ykIncremental Stability (δ-GUAS)– 0 if kx

yk = 0– ! 1 if kx• decreasing in t
<latexit sha1_base64="W1f9wnRLwEWTp6zmbeqHVz00R7M=">AAADP3ichVJNb9NAEF2bj5bwlcKRy4oEiUsju6oEF6QKLhyLRNpKcRSt12NnVHtt7Y4pxvU/48Jf4MaVCwcQ4sqNdWqiJiliJEvP7719Mx5vWKRoyPO+OO616zdubm3f6t2+c/fe/f7OgyOTl1rCWOZprk9CYSBFBWNCSuGk0CCyMIXj8PRVqx+/A20wV2+pKmCaiURhjFKQpWY7zjgIIUFVZ6iwEAk0te/JrOl1NBJk+AGawIDNVgnN66DlDBRNvTvaB2vlC4ajkrazQZVYyIfB+fvdKjgfrif9tQ+9Icd46XvhDZdKoDGZk9A6PwtQxVStODfVXgAq2mgQwco89O9JLiXybir6b5cr3pY77M36A2/kLYpvAr8DA9bV4az/OYhyWWagSKbCmInvFTSthSaUaZtf2o0LeWrTJxYqkYGZ1ov/3/Anlol4nGv7KOIL9vKJWmTGVFlonZmguVnXWvIqbVJS/HxaoypKAiUvGsVlyinn7WXiEWqQlFYWCKnRzsrlXGghyV65dgn++idvgqO9ke+N/Df7g4OX3Tq22SP2mD1lPnvGDthrdsjGTDofna/Od+eH+8n95v50f11YXac785CtlPv7D4LXDTY=</latexit>

yk ! 1

Incrementally Globally Uniformly Asymptotically Stable– ! 0 if t ! 1

Def.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)x(y, t)



kx

GAS

yk, t

where x(x, ) is the trajectory starting at x.
<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>

t
δ-GAS

t

Hasuo (NII, JP) 4

• increasing in kx

ykIncremental Stability (δ-GUAS)– 0 if kx

yk = 0– ! 1 if kx• decreasing in t
<latexit sha1_base64="W1f9wnRLwEWTp6zmbeqHVz00R7M=">AAADP3ichVJNb9NAEF2bj5bwlcKRy4oEiUsju6oEF6QKLhyLRNpKcRSt12NnVHtt7Y4pxvU/48Jf4MaVCwcQ4sqNdWqiJiliJEvP7719Mx5vWKRoyPO+OO616zdubm3f6t2+c/fe/f7OgyOTl1rCWOZprk9CYSBFBWNCSuGk0CCyMIXj8PRVqx+/A20wV2+pKmCaiURhjFKQpWY7zjgIIUFVZ6iwEAk0te/JrOl1NBJk+AGawIDNVgnN66DlDBRNvTvaB2vlC4ajkrazQZVYyIfB+fvdKjgfrif9tQ+9Icd46XvhDZdKoDGZk9A6PwtQxVStODfVXgAq2mgQwco89O9JLiXybir6b5cr3pY77M36A2/kLYpvAr8DA9bV4az/OYhyWWagSKbCmInvFTSthSaUaZtf2o0LeWrTJxYqkYGZ1ov/3/Anlol4nGv7KOIL9vKJWmTGVFlonZmguVnXWvIqbVJS/HxaoypKAiUvGsVlyinn7WXiEWqQlFYWCKnRzsrlXGghyV65dgn++idvgqO9ke+N/Df7g4OX3Tq22SP2mD1lPnvGDthrdsjGTDofna/Od+eH+8n95v50f11YXac785CtlPv7D4LXDTY=</latexit>

yk ! 1

Incrementally Globally Uniformly Asymptotically Stable– ! 0 if t ! 1

Def.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)x(y, t)



kx

GAS

yk, t

where x(x, ) is the trajectory starting at x.
<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>Def.
For a dynamics ẋ = f (x) in Rn , a smooth function
V : Rn ⇥ Rn ! R+ is a common -GAS Lyapunov function if
there exist K1 functions ↵, ↵ and  > 0 such that↵(kx
@V<latexit sha1_base64="pUU+6u+ntJzXpLhbmdZ1Cl9XY9U=">AAAE6HicfVTPb9s2FFZib021H03aYy8PjTIkS2PYAYoWDVqk3bAN2A5ZsjgFTCegKMpiQ5GKSCUWGF26f2C3Ydf9V7vvuD9ij7bnZM4wnp7er+97H58YF1IY2+3+sbTcan/08b2V++Enn372+YPVtYd9o6uS8WOmpS7fxdRwKRQ/tsJK/q4oOc1jyU/i8698/OSSl0Zo9ZOtCz7M6UiJVDBq0XW2tvwXiflIKJcLJQo64o3rdVnehETxK6bznKrEkcPGkZzaLI7dYbMYK2RlbsdPt5sQiOVjG6eOVCrhpWfnvuZpp2nIxUVFEwi/0SVQSGpFc8EMRCTR1o2bV+nmeCsCodBzeKqipxBimsm1tlkIkFaKeeIQ9YkfXoHPQjSRczOzSzHKLC1LfQVTctjOAADFesLzInOeu+9BEi4tjXa+fXMEP9S0qJS+nEM0IFKwGS851vExXgUW+CEZle775owIldo6muf7GW6GJVQWGW2Qf0T05YITG6J0GDmnRUFfdyMwFcsQjNpwAzwopFpKfSXUCDItE/xEtaSEaPwUakDoyaxRJ5zdHpVipL5swi/gLodNcj3eqcn1Ftkjkl+QPehv+jZbMHfcoTivCTeIpDGXjl+8THjan4Sn+uEekMF25xnPhx43LSlzpKClFVRCv7mxx80Uz18tbIf/l1rPU2/T25kKNee9SGoSnZPiuJX/6DH5mK92eLa63u10JwfuGr2ZsR7MzsHZ6p+4l6zKubJMUmMGvW5hh86zZRIbkspwhD7H7gM0cZm5GbrJb9nABnqmV5dqZWHivV3haG5MnceY6ffKLMa8879ig8qmL4ZOqKKyXLEpUFpJsBr8Pw6JKDmzskaDslIgV2AZRdEtvgThZIlnb4KLcbsalKW3KMJdo7/b6XU7vR931/ffzgRaCR4HT4LNoBc8D/aD74KD4DhgraNW3frQ+rn9vv1L+9f2b9PU5aVZzaPgX6f9+99NTp12</latexit>@xyk)  V (x, y)  ↵(kx

(x, y)f (x) +@V@y(x, y)f (y) 

t
δ-GAS

yk)
V (x, y)t

Hasuo (NII, JP) 4

• increasing in kx

ykIncremental Stability (δ-GUAS)– 0 if kx

yk = 0– ! 1 if kx• decreasing in t
<latexit sha1_base64="W1f9wnRLwEWTp6zmbeqHVz00R7M=">AAADP3ichVJNb9NAEF2bj5bwlcKRy4oEiUsju6oEF6QKLhyLRNpKcRSt12NnVHtt7Y4pxvU/48Jf4MaVCwcQ4sqNdWqiJiliJEvP7719Mx5vWKRoyPO+OO616zdubm3f6t2+c/fe/f7OgyOTl1rCWOZprk9CYSBFBWNCSuGk0CCyMIXj8PRVqx+/A20wV2+pKmCaiURhjFKQpWY7zjgIIUFVZ6iwEAk0te/JrOl1NBJk+AGawIDNVgnN66DlDBRNvTvaB2vlC4ajkrazQZVYyIfB+fvdKjgfrif9tQ+9Icd46XvhDZdKoDGZk9A6PwtQxVStODfVXgAq2mgQwco89O9JLiXybir6b5cr3pY77M36A2/kLYpvAr8DA9bV4az/OYhyWWagSKbCmInvFTSthSaUaZtf2o0LeWrTJxYqkYGZ1ov/3/Anlol4nGv7KOIL9vKJWmTGVFlonZmguVnXWvIqbVJS/HxaoypKAiUvGsVlyinn7WXiEWqQlFYWCKnRzsrlXGghyV65dgn++idvgqO9ke+N/Df7g4OX3Tq22SP2mD1lPnvGDthrdsjGTDofna/Od+eH+8n95v50f11YXac785CtlPv7D4LXDTY=</latexit>

yk ! 1

Incrementally Globally Uniformly Asymptotically Stable– ! 0 if t ! 1

Def.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)V(x,y) is more or less|| x - y ||…

x(y, t)



kx

GAS

yk, t

where x(x, ) is the trajectory starting at x.

<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>Def.
For a dynamics ẋ = f (x) in Rn , a smooth function
V : Rn ⇥ Rn ! R+ is a common -GAS Lyapunov function if
there exist K1 functions ↵, ↵ and  > 0 such that↵(kx
that decreases
along thedynamics<latexit sha1_base64="pUU+6u+ntJzXpLhbmdZ1Cl9XY9U=">AAAE6HicfVTPb9s2FFZib021H03aYy8PjTIkS2PYAYoWDVqk3bAN2A5ZsjgFTCegKMpiQ5GKSCUWGF26f2C3Ydf9V7vvuD9ij7bnZM4wnp7er+97H58YF1IY2+3+sbTcan/08b2V++Enn372+YPVtYd9o6uS8WOmpS7fxdRwKRQ/tsJK/q4oOc1jyU/i8698/OSSl0Zo9ZOtCz7M6UiJVDBq0XW2tvwXiflIKJcLJQo64o3rdVnehETxK6bznKrEkcPGkZzaLI7dYbMYK2RlbsdPt5sQiOVjG6eOVCrhpWfnvuZpp2nIxUVFEwi/0SVQSGpFc8EMRCTR1o2bV+nmeCsCodBzeKqipxBimsm1tlkIkFaKeeIQ9YkfXoHPQjSRczOzSzHKLC1LfQVTctjOAADFesLzInOeu+9BEi4tjXa+fXMEP9S0qJS+nEM0IFKwGS851vExXgUW+CEZle775owIldo6muf7GW6GJVQWGW2Qf0T05YITG6J0GDmnRUFfdyMwFcsQjNpwAzwopFpKfSXUCDItE/xEtaSEaPwUakDoyaxRJ5zdHpVipL5swi/gLodNcj3eqcn1Ftkjkl+QPehv+jZbMHfcoTivCTeIpDGXjl+8THjan4Sn+uEekMF25xnPhx43LSlzpKClFVRCv7mxx80Uz18tbIf/l1rPU2/T25kKNee9SGoSnZPiuJX/6DH5mK92eLa63u10JwfuGr2ZsR7MzsHZ6p+4l6zKubJMUmMGvW5hh86zZRIbkspwhD7H7gM0cZm5GbrJb9nABnqmV5dqZWHivV3haG5MnceY6ffKLMa8879ig8qmL4ZOqKKyXLEpUFpJsBr8Pw6JKDmzskaDslIgV2AZRdEtvgThZIlnb4KLcbsalKW3KMJdo7/b6XU7vR931/ffzgRaCR4HT4LNoBc8D/aD74KD4DhgraNW3frQ+rn9vv1L+9f2b9PU5aVZzaPgX6f9+99NTp12</latexit>@V@xyk)  V (x, y)  ↵(kx

(x, y)f (x) +@V@y(x, y)f (y) 

t
δ-GAS

yk)
V (x, y)t

Hasuo (NII, JP) 4

• increasing in kx

ykIncremental Stability (δ-GUAS)– 0 if kx

yk = 0– ! 1 if kx• decreasing in t
<latexit sha1_base64="W1f9wnRLwEWTp6zmbeqHVz00R7M=">AAADP3ichVJNb9NAEF2bj5bwlcKRy4oEiUsju6oEF6QKLhyLRNpKcRSt12NnVHtt7Y4pxvU/48Jf4MaVCwcQ4sqNdWqiJiliJEvP7719Mx5vWKRoyPO+OO616zdubm3f6t2+c/fe/f7OgyOTl1rCWOZprk9CYSBFBWNCSuGk0CCyMIXj8PRVqx+/A20wV2+pKmCaiURhjFKQpWY7zjgIIUFVZ6iwEAk0te/JrOl1NBJk+AGawIDNVgnN66DlDBRNvTvaB2vlC4ajkrazQZVYyIfB+fvdKjgfrif9tQ+9Icd46XvhDZdKoDGZk9A6PwtQxVStODfVXgAq2mgQwco89O9JLiXybir6b5cr3pY77M36A2/kLYpvAr8DA9bV4az/OYhyWWagSKbCmInvFTSthSaUaZtf2o0LeWrTJxYqkYGZ1ov/3/Anlol4nGv7KOIL9vKJWmTGVFlonZmguVnXWvIqbVJS/HxaoypKAiUvGsVlyinn7WXiEWqQlFYWCKnRzsrlXGghyV65dgn++idvgqO9ke+N/Df7g4OX3Tq22SP2mD1lPnvGDthrdsjGTDofna/Od+eH+8n95v50f11YXac785CtlPv7D4LXDTY=</latexit>

yk ! 1

Incrementally Globally Uniformly Asymptotically Stable– ! 0 if t ! 1

Def.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)V(x,y) is more or less|| x - y ||…

x(y, t)



kx

GAS

yk, t

where x(x, ) is the trajectory starting at x.

<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>Def.
For a dynamics ẋ = f (x) in Rn , a smooth function
V : Rn ⇥ Rn ! R+ is a common -GAS Lyapunov function if
there exist K1 functions ↵, ↵ and  > 0 such that↵(kx
that decreases
along thedynamics<latexit sha1_base64="pUU+6u+ntJzXpLhbmdZ1Cl9XY9U=">AAAE6HicfVTPb9s2FFZib021H03aYy8PjTIkS2PYAYoWDVqk3bAN2A5ZsjgFTCegKMpiQ5GKSCUWGF26f2C3Ydf9V7vvuD9ij7bnZM4wnp7er+97H58YF1IY2+3+sbTcan/08b2V++Enn372+YPVtYd9o6uS8WOmpS7fxdRwKRQ/tsJK/q4oOc1jyU/i8698/OSSl0Zo9ZOtCz7M6UiJVDBq0XW2tvwXiflIKJcLJQo64o3rdVnehETxK6bznKrEkcPGkZzaLI7dYbMYK2RlbsdPt5sQiOVjG6eOVCrhpWfnvuZpp2nIxUVFEwi/0SVQSGpFc8EMRCTR1o2bV+nmeCsCodBzeKqipxBimsm1tlkIkFaKeeIQ9YkfXoHPQjSRczOzSzHKLC1LfQVTctjOAADFesLzInOeu+9BEi4tjXa+fXMEP9S0qJS+nEM0IFKwGS851vExXgUW+CEZle775owIldo6muf7GW6GJVQWGW2Qf0T05YITG6J0GDmnRUFfdyMwFcsQjNpwAzwopFpKfSXUCDItE/xEtaSEaPwUakDoyaxRJ5zdHpVipL5swi/gLodNcj3eqcn1Ftkjkl+QPehv+jZbMHfcoTivCTeIpDGXjl+8THjan4Sn+uEekMF25xnPhx43LSlzpKClFVRCv7mxx80Uz18tbIf/l1rPU2/T25kKNee9SGoSnZPiuJX/6DH5mK92eLa63u10JwfuGr2ZsR7MzsHZ6p+4l6zKubJMUmMGvW5hh86zZRIbkspwhD7H7gM0cZm5GbrJb9nABnqmV5dqZWHivV3haG5MnceY6ffKLMa8879ig8qmL4ZOqKKyXLEpUFpJsBr8Pw6JKDmzskaDslIgV2AZRdEtvgThZIlnb4KLcbsalKW3KMJdo7/b6XU7vR931/ffzgRaCR4HT4LNoBc8D/aD74KD4DhgraNW3frQ+rn9vv1L+9f2b9PU5aVZzaPgX6f9+99NTp12</latexit>@V@xyk)  V (x, y)  ↵(kx

(x, y)f (x) +@V@y(x, y)f (y) 

t
δ-GAS

yk)
V (x, y)Thm.
There is a -GAS Lyapunov function=) incrementally stable ( -GAS).

t<latexit sha1_base64="oEMlW7WLHpaWjokmXb+5B6tSEZc=">AAACrXicbVFNb9QwEHXCVwlfC1yQuFjsIpUD26QXOKECh/bQQxG7baX1spo4k8SqY6e2U1hF+VP8G+78EJxtJErLSCM9vZl5M3qT1lJYF8e/gvDW7Tt3723djx48fPT4yejps2OrG8NxzrXU5jQFi1IonDvhJJ7WBqFKJZ6kZ5/7+skFGiu0mrl1jcsKCiVywcF5ajX6yVIshGoroUQNBXZtEvOqiyhz+MOlecsalaHp5dtZWU27jp2fN5DRaFaiQSoshYhOWIbSweTt/sev9HANdaP0Bc0bxfstUTRhh1oVRhSlA2P09wnrNSIqFDdYoXIg5ZpaB/5sun1V7c2URgxV9vfAaDUax9N4E/QmSAYwJkMcrUa/WaZ50+/hEqxdJHHtli0YJ7j0gqyxWAM/8+oLDxVUaJftxtuOvvZMRnNtfCpHN+zViRYqa9dV6jsrcKW9XuvJ/9UWjcvfL1uh6sah4peL8kZSp2n/KJoJg9x5WzIB3Ah/K+UlGODOvzNiveDw2DbVMuu8Lcl1E26C491pEk+TL7vjvU+DQVvkJXlFtklC3pE9ckCOyJzw4EXwIdgPDsKdcB6y8NtlaxgMM8/JPxEWfwCKNdIs</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="O08Hfc9BE+RGoZ8s+Ex+MQtO/00=">AAAConicbVFNb9QwEHXCVwkFFk5IXCy6SOVASLjQUwXi0B56KGK3rbReVhNnsrHq2Kk/Cqsof4p/w50fgrNdidIy0khPb+z3Rm+KVgrrsuxXFN+5e+/+g62HyaPtx0+ejp5tn1jtDccp11KbswIsSqFw6oSTeNYahKaQeFqcfx7mp5dorNBq4lYtzhtYKlEJDi5Qi9FPVuBSqK4RSrSwxL7LM970CWUOf7ii6phXJZpBvpvUTdr37OLCQ0mTSY0GqbAUEjpmJUoH47cHn77SoxW0XulLWnnFB5ckGbMjrZZGLGsHxujvYzZoJFQobrBB5UDKFbUOwtp097ram5QmDFX5d8FkMdrJ0mxd9DbIN2CHbOp4MfrNSs394MMlWDvLs9bNOzBOcBkEmbfYAj8P6rMAFTRo5906256+DkxJK21CK0fX7PUfHTTWrpoivGzA1fbmbCD/N5t5V+3NO6Fa71DxK6PKS+o0HQ5FS2GQuxBLKYAbEXalvAYD3IVzJmwQ3By2K7Qs+xBLfjOE2+DkfZpnaf4lI1vkJXlFdklOPpCP5JAckynh0YtoPzqIDuN38TRmVwHG0SbJ5+Sfir/9AWnt0RU=</latexit>
sha1_base64="JLiFGLmTh9P6RbTY5Fh1IdMUH4w=">AAACrXicbVFNb9QwEHXCVwlfC1yQuFjsIpUDS8KlPaECh/bQQxG7baX1spo4k8SqY6e2U1hF+VP8G+78EJxtJErLSCM9vZl5M3qT1lJYF8e/gvDW7Tt3723djx48fPT4yejps2OrG8NxzrXU5jQFi1IonDvhJJ7WBqFKJZ6kZ5/7+skFGiu0mrl1jcsKCiVywcF5ajX6yVIshGoroUQNBXZtEvOqiyhz+MOlecsalaHp5dtZWU27jp2fN5DRaFaiQSoshYhOWIbSweTt/sev9HANdaP0Bc0bxfstUTRhh1oVRhSlA2P09wnrNSIqFDdYoXIg5ZpaB/5sun1V7c2URgxV9vfAaDUax9N4E/QmSAYwJkMcrUa/WaZ50+/hEqxdJHHtli0YJ7j0gqyxWAM/8+oLDxVUaJftxtuOvvZMRnNtfCpHN+zViRYqa9dV6jsrcKW9XuvJ/9UWjct3l61QdeNQ8ctFeSOp07R/FM2EQe68LZkAboS/lfISDHDn3xmxXnB4bJtqmXXeluS6CTfB8ftpEk+TL/F479Ng0BZ5SV6RbZKQHbJHDsgRmRMevAg+BPvBQfgunIcs/HbZGgbDzHPyT4TFH4mV0io=</latexit>

Hasuo (NII, JP) 4

• increasing in kx

ykIncremental Stability (δ-GUAS)– 0 if kx

yk = 0– ! 1 if kx• decreasing in t
<latexit sha1_base64="W1f9wnRLwEWTp6zmbeqHVz00R7M=">AAADP3ichVJNb9NAEF2bj5bwlcKRy4oEiUsju6oEF6QKLhyLRNpKcRSt12NnVHtt7Y4pxvU/48Jf4MaVCwcQ4sqNdWqiJiliJEvP7719Mx5vWKRoyPO+OO616zdubm3f6t2+c/fe/f7OgyOTl1rCWOZprk9CYSBFBWNCSuGk0CCyMIXj8PRVqx+/A20wV2+pKmCaiURhjFKQpWY7zjgIIUFVZ6iwEAk0te/JrOl1NBJk+AGawIDNVgnN66DlDBRNvTvaB2vlC4ajkrazQZVYyIfB+fvdKjgfrif9tQ+9Icd46XvhDZdKoDGZk9A6PwtQxVStODfVXgAq2mgQwco89O9JLiXybir6b5cr3pY77M36A2/kLYpvAr8DA9bV4az/OYhyWWagSKbCmInvFTSthSaUaZtf2o0LeWrTJxYqkYGZ1ov/3/Anlol4nGv7KOIL9vKJWmTGVFlonZmguVnXWvIqbVJS/HxaoypKAiUvGsVlyinn7WXiEWqQlFYWCKnRzsrlXGghyV65dgn++idvgqO9ke+N/Df7g4OX3Tq22SP2mD1lPnvGDthrdsjGTDofna/Od+eH+8n95v50f11YXac785CtlPv7D4LXDTY=</latexit>

yk ! 1

Incrementally Globally Uniformly Asymptotically Stable– ! 0 if t ! 1

Def.
A dynamics is said to be -GAS if
9 KL function s.t.
x(x, t)V(x,y) is more or less|| x - y ||…

x(y, t)



kx

GAS

yk, t

where x(x, ) is the trajectory starting at x.

<latexit sha1_base64="+Jgywg36ygy/4moXYL2t6vqxoYY=">AAADk3icbVJbT9RAFC67XrBeWDQ++XIiJYFkt9nlQUx4EJBEEzVBlEvCrGQ6Pd0dmU7LzFS2Kf1B/h3f/DeeLmtA8Dw0X79z+c45c6JcSev6/d9zrfadu/fuzz/wHz56/GShs/j0wGaFEbgvMpWZo4hbVFLjvpNO4VFukKeRwsPo9G3jP/yBxspMf3VljsOUj7RMpOCOqJPFuZ8swpHUVSq1zPkI62o9XBNp7QNzOHFRUrFCx2gagWoHk7Cu2dlZwWPYgrjUPJXCgrRguYzBZRAhZWKajysWJRaNRAsBi1E5HvTebX2pQSbg+8ThhMazAaGUu7HgqvrwsQ4gKbRoeiM+QkoCG7qQ+csASaZUdi71CMaZii1RSWaAKwXBpAslMKmB7X3TQRcCRz9sL1cFCXAdz0RomrxuPLvZeRBSE6QhR4pdsK7/N2BSr0y6brV3nSiJ8Fm3CTYUvMEUntG36W9aYIV8F5NeyS66rAtuFrkaBP75GA1eqU+L91aDZmNujOAM/47CZaYE67hxzXDc0TxBCD5DHV+9i3/SWeqH/anBbTCYgSVvZrsnnV8szkSRonZCcWuPB/3cDatGRigqyAqLORenVP2YIL0l2mE1vakalomJpwtOMu1gyl7PqHhqbZlGFNnMZm/6GvJ/vuPCJa+HldR54VCLS6GkUM3tNAcKsTS0EVUS4MJI6hXEmBsuHJ1xs4TBzZFvg4O1cNAPB5/Xlja3Z+uY9154L70Vb+Cte5vee2/X2/dEq9N61XrT2mw/b2+0t9s7l6GtuVnOM+8fa3/6A4gBG+k=</latexit>Def.
For a dynamics ẋ = f (x) in Rn , a smooth function
V : Rn ⇥ Rn ! R+ is a common -GAS Lyapunov function if
there exist K1 functions ↵, ↵ and  > 0 such that↵(kx
that decreases
along thedynamics<latexit sha1_base64="pUU+6u+ntJzXpLhbmdZ1Cl9XY9U=">AAAE6HicfVTPb9s2FFZib021H03aYy8PjTIkS2PYAYoWDVqk3bAN2A5ZsjgFTCegKMpiQ5GKSCUWGF26f2C3Ydf9V7vvuD9ij7bnZM4wnp7er+97H58YF1IY2+3+sbTcan/08b2V++Enn372+YPVtYd9o6uS8WOmpS7fxdRwKRQ/tsJK/q4oOc1jyU/i8698/OSSl0Zo9ZOtCz7M6UiJVDBq0XW2tvwXiflIKJcLJQo64o3rdVnehETxK6bznKrEkcPGkZzaLI7dYbMYK2RlbsdPt5sQiOVjG6eOVCrhpWfnvuZpp2nIxUVFEwi/0SVQSGpFc8EMRCTR1o2bV+nmeCsCodBzeKqipxBimsm1tlkIkFaKeeIQ9YkfXoHPQjSRczOzSzHKLC1LfQVTctjOAADFesLzInOeu+9BEi4tjXa+fXMEP9S0qJS+nEM0IFKwGS851vExXgUW+CEZle775owIldo6muf7GW6GJVQWGW2Qf0T05YITG6J0GDmnRUFfdyMwFcsQjNpwAzwopFpKfSXUCDItE/xEtaSEaPwUakDoyaxRJ5zdHpVipL5swi/gLodNcj3eqcn1Ftkjkl+QPehv+jZbMHfcoTivCTeIpDGXjl+8THjan4Sn+uEekMF25xnPhx43LSlzpKClFVRCv7mxx80Uz18tbIf/l1rPU2/T25kKNee9SGoSnZPiuJX/6DH5mK92eLa63u10JwfuGr2ZsR7MzsHZ6p+4l6zKubJMUmMGvW5hh86zZRIbkspwhD7H7gM0cZm5GbrJb9nABnqmV5dqZWHivV3haG5MnceY6ffKLMa8879ig8qmL4ZOqKKyXLEpUFpJsBr8Pw6JKDmzskaDslIgV2AZRdEtvgThZIlnb4KLcbsalKW3KMJdo7/b6XU7vR931/ffzgRaCR4HT4LNoBc8D/aD74KD4DhgraNW3frQ+rn9vv1L+9f2b9PU5aVZzaPgX6f9+99NTp12</latexit>@V@xyk)  V (x, y)  ↵(kx

(x, y)f (x) +@V@y(x, y)f (y) 

t
δ-GAS

yk)
V (x, y)Thm.
There is a -GAS Lyapunov function=) incrementally stable ( -GAS).

t<latexit sha1_base64="oEMlW7WLHpaWjokmXb+5B6tSEZc=">AAACrXicbVFNb9QwEHXCVwlfC1yQuFjsIpUD26QXOKECh/bQQxG7baX1spo4k8SqY6e2U1hF+VP8G+78EJxtJErLSCM9vZl5M3qT1lJYF8e/gvDW7Tt3723djx48fPT4yejps2OrG8NxzrXU5jQFi1IonDvhJJ7WBqFKJZ6kZ5/7+skFGiu0mrl1jcsKCiVywcF5ajX6yVIshGoroUQNBXZtEvOqiyhz+MOlecsalaHp5dtZWU27jp2fN5DRaFaiQSoshYhOWIbSweTt/sev9HANdaP0Bc0bxfstUTRhh1oVRhSlA2P09wnrNSIqFDdYoXIg5ZpaB/5sun1V7c2URgxV9vfAaDUax9N4E/QmSAYwJkMcrUa/WaZ50+/hEqxdJHHtli0YJ7j0gqyxWAM/8+oLDxVUaJftxtuOvvZMRnNtfCpHN+zViRYqa9dV6jsrcKW9XuvJ/9UWjcvfL1uh6sah4peL8kZSp2n/KJoJg9x5WzIB3Ah/K+UlGODOvzNiveDw2DbVMuu8Lcl1E26C491pEk+TL7vjvU+DQVvkJXlFtklC3pE9ckCOyJzw4EXwIdgPDsKdcB6y8NtlaxgMM8/JPxEWfwCKNdIs</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="O08Hfc9BE+RGoZ8s+Ex+MQtO/00=">AAAConicbVFNb9QwEHXCVwkFFk5IXCy6SOVASLjQUwXi0B56KGK3rbReVhNnsrHq2Kk/Cqsof4p/w50fgrNdidIy0khPb+z3Rm+KVgrrsuxXFN+5e+/+g62HyaPtx0+ejp5tn1jtDccp11KbswIsSqFw6oSTeNYahKaQeFqcfx7mp5dorNBq4lYtzhtYKlEJDi5Qi9FPVuBSqK4RSrSwxL7LM970CWUOf7ii6phXJZpBvpvUTdr37OLCQ0mTSY0GqbAUEjpmJUoH47cHn77SoxW0XulLWnnFB5ckGbMjrZZGLGsHxujvYzZoJFQobrBB5UDKFbUOwtp097ram5QmDFX5d8FkMdrJ0mxd9DbIN2CHbOp4MfrNSs394MMlWDvLs9bNOzBOcBkEmbfYAj8P6rMAFTRo5906256+DkxJK21CK0fX7PUfHTTWrpoivGzA1fbmbCD/N5t5V+3NO6Fa71DxK6PKS+o0HQ5FS2GQuxBLKYAbEXalvAYD3IVzJmwQ3By2K7Qs+xBLfjOE2+DkfZpnaf4lI1vkJXlFdklOPpCP5JAckynh0YtoPzqIDuN38TRmVwHG0SbJ5+Sfir/9AWnt0RU=</latexit>
sha1_base64="JLiFGLmTh9P6RbTY5Fh1IdMUH4w=">AAACrXicbVFNb9QwEHXCVwlfC1yQuFjsIpUDS8KlPaECh/bQQxG7baX1spo4k8SqY6e2U1hF+VP8G+78EJxtJErLSCM9vZl5M3qT1lJYF8e/gvDW7Tt3723djx48fPT4yejps2OrG8NxzrXU5jQFi1IonDvhJJ7WBqFKJZ6kZ5/7+skFGiu0mrl1jcsKCiVywcF5ajX6yVIshGoroUQNBXZtEvOqiyhz+MOlecsalaHp5dtZWU27jp2fN5DRaFaiQSoshYhOWIbSweTt/sev9HANdaP0Bc0bxfstUTRhh1oVRhSlA2P09wnrNSIqFDdYoXIg5ZpaB/5sun1V7c2URgxV9vfAaDUax9N4E/QmSAYwJkMcrUa/WaZ50+/hEqxdJHHtli0YJ7j0gqyxWAM/8+oLDxVUaJftxtuOvvZMRnNtfCpHN+zViRYqa9dV6jsrcKW9XuvJ/9UWjct3l61QdeNQ8ctFeSOp07R/FM2EQe68LZkAboS/lfISDHDn3xmxXnB4bJtqmXXeluS6CTfB8ftpEk+TL/F479Ng0BZ5SV6RbZKQHbJHDsgRmRMevAg+BPvBQfgunIcs/HbZGgbDzHPyT4TFH4mV0io=</latexit>

Switched extension: δ-GUAS, common Lyapunov func.
[Girard, Pola, Tabuada, IEEE TAC ’10]

Hasuo (NII, JP) 4

Discrete Abstraction via Incremental Stability[Girard, Pola, Tabuada, IEEE TAC ’10]

For a switched dynamics ẋ = fp (x) …
<latexit sha1_base64="b1aAoYEKuxppQ5RIx5a34r84bUQ=">AAACC3icbZDLSgMxGIUz9VbrbdSlm2AR6qbMiKAboejGZQV7gXYYMmmmDc0kQ5IpLcM8gm/gVl/Anbj1Idz7IGbaWWjrgcDh/Jf8fEHMqNKO82WV1tY3NrfK25Wd3b39A/vwqK1EIjFpYcGE7AZIEUY5aWmqGenGkqAoYKQTjO/yemdCpKKCP+pZTLwIDTkNKUbaRL5t9wdCp9PsJvTTOKtNz3276tSdueCqcQtTBYWavv1tVuAkIlxjhpTquU6svRRJTTEjWaWfKBIjPEZD0jOWo4goL51fnsEzkwxgKKR5XMN5+nsiRZFSsygwnRHSI7Vcy8P/ar1Eh9deSnmcaMLx4qMwYVALmGOAAyoJ1mxmDMKSmlshHiGJsDawKv18YYEtDQQbZAaLuwxh1bQv6q5Tdx8uq43bAlAZnIBTUAMuuAINcA+aoAUwmIBn8AJerSfrzXq3PhatJauYOQZ/ZH3+ANncm6I=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="LH3bPeus+w+du5iygLcEFAPh56Y=">AAACAHicbZDNSsNAFIVv6l+tVaNbN4NFqJuSuNGNILhxWcH+QBvCZDpph04mYWZSWkIewTdwqy/gTnwR9z6IkzYLbT0wcDhn5s7lCxLOlHacL6uytb2zu1fdrx3UD4+O7ZN6V8WpJLRDYh7LfoAV5UzQjmaa034iKY4CTnvB9L7oezMqFYvFk14k1IvwWLCQEaxN5Nv2cBTrbJ7fhn6W5M35pW83nJazFNo0bmkaUKrt299mBEkjKjThWKmB6yTay7DUjHCa14apogkmUzymA2MFjqjysuXmObowyQiFsTRHaLRMf7/IcKTUIgrMzQjriVrvivC/bpDq8MbLmEhSTQVZfRSmHOkYFRjQiElKNF8Yg4lkZldEJlhiog2s2rAYWGLLgpiPcoPFXYewabpXLddpuY8OVOEMzqEJLlzDHTxAGzpAYAYv8Apv1rP1bn2sAFaskuQp/JH1+QMn1pos</latexit>
sha1_base64="o/SdJbZfj+PjZWcm6LvkTzckCEw=">AAACC3icbZC7TsMwGIUdrqXcAowsFhVSWaqEBRakChbGItGL1EaR4zitVceObKdqFeUReANWeAE2xMpDsPMgOG0GaDmSpaPzX/zrCxJGlXacL2ttfWNza7uyU93d2z84tI+OO0qkEpM2FkzIXoAUYZSTtqaakV4iCYoDRrrB+K6odydEKir4o54lxIvRkNOIYqRN5Nv2IBQ6m+Y3kZ8leX164ds1p+HMBVeNW5oaKNXy7W+zAqcx4RozpFTfdRLtZUhqihnJq4NUkQThMRqSvrEcxUR52fzyHJ6bJISRkOZxDefp74kMxUrN4sB0xkiP1HKtCP+r9VMdXXsZ5UmqCceLj6KUQS1ggQGGVBKs2cwYhCU1t0I8QhJhbWBVB8XCElsWCBbmBou7DGHVdC4brtNwH5xa87YEVAGn4AzUgQuuQBPcgxZoAwwm4Bm8gFfryXqz3q2PReuaVc6cgD+yPn8A2Jybng==</latexit>

Commonwitnesses
δ-GAS
Lyapunov func.

V

Incremental
stability(δ-GUAS)

Hasuo (NII, JP) 5

Discrete Abstraction via Incremental Stability[Girard, Pola, Tabuada, IEEE TAC ’10]

For a switched dynamics ẋ = fp (x) …
<latexit sha1_base64="b1aAoYEKuxppQ5RIx5a34r84bUQ=">AAACC3icbZDLSgMxGIUz9VbrbdSlm2AR6qbMiKAboejGZQV7gXYYMmmmDc0kQ5IpLcM8gm/gVl/Anbj1Idz7IGbaWWjrgcDh/Jf8fEHMqNKO82WV1tY3NrfK25Wd3b39A/vwqK1EIjFpYcGE7AZIEUY5aWmqGenGkqAoYKQTjO/yemdCpKKCP+pZTLwIDTkNKUbaRL5t9wdCp9PsJvTTOKtNz3276tSdueCqcQtTBYWavv1tVuAkIlxjhpTquU6svRRJTTEjWaWfKBIjPEZD0jOWo4goL51fnsEzkwxgKKR5XMN5+nsiRZFSsygwnRHSI7Vcy8P/ar1Eh9deSnmcaMLx4qMwYVALmGOAAyoJ1mxmDMKSmlshHiGJsDawKv18YYEtDQQbZAaLuwxh1bQv6q5Tdx8uq43bAlAZnIBTUAMuuAINcA+aoAUwmIBn8AJerSfrzXq3PhatJauYOQZ/ZH3+ANncm6I=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="LH3bPeus+w+du5iygLcEFAPh56Y=">AAACAHicbZDNSsNAFIVv6l+tVaNbN4NFqJuSuNGNILhxWcH+QBvCZDpph04mYWZSWkIewTdwqy/gTnwR9z6IkzYLbT0wcDhn5s7lCxLOlHacL6uytb2zu1fdrx3UD4+O7ZN6V8WpJLRDYh7LfoAV5UzQjmaa034iKY4CTnvB9L7oezMqFYvFk14k1IvwWLCQEaxN5Nv2cBTrbJ7fhn6W5M35pW83nJazFNo0bmkaUKrt299mBEkjKjThWKmB6yTay7DUjHCa14apogkmUzymA2MFjqjysuXmObowyQiFsTRHaLRMf7/IcKTUIgrMzQjriVrvivC/bpDq8MbLmEhSTQVZfRSmHOkYFRjQiElKNF8Yg4lkZldEJlhiog2s2rAYWGLLgpiPcoPFXYewabpXLddpuY8OVOEMzqEJLlzDHTxAGzpAYAYv8Apv1rP1bn2sAFaskuQp/JH1+QMn1pos</latexit>
sha1_base64="o/SdJbZfj+PjZWcm6LvkTzckCEw=">AAACC3icbZC7TsMwGIUdrqXcAowsFhVSWaqEBRakChbGItGL1EaR4zitVceObKdqFeUReANWeAE2xMpDsPMgOG0GaDmSpaPzX/zrCxJGlXacL2ttfWNza7uyU93d2z84tI+OO0qkEpM2FkzIXoAUYZSTtqaakV4iCYoDRrrB+K6odydEKir4o54lxIvRkNOIYqRN5Nv2IBQ6m+Y3kZ8leX164ds1p+HMBVeNW5oaKNXy7W+zAqcx4RozpFTfdRLtZUhqihnJq4NUkQThMRqSvrEcxUR52fzyHJ6bJISRkOZxDefp74kMxUrN4sB0xkiP1HKtCP+r9VMdXXsZ5UmqCceLj6KUQS1ggQGGVBKs2cwYhCU1t0I8QhJhbWBVB8XCElsWCBbmBou7DGHVdC4brtNwH5xa87YEVAGn4AzUgQuuQBPcgxZoAwwm4Bm8gFfryXqz3q2PReuaVc6cgD+yPn8A2Jybng==</latexit>

Commonwitnesses
δ-GAS
Lyapunov func.

V

Incremental
stability(δ-GUAS)

induces8

Approximate bisimulation

Statespace abstraction

ANTOINE GIRARD, GIORDANO
AND PAULO TABUADA(Fig. from POLA,[GirardPT’10])Thm.
Let V be a common -GAS Lyapunov func. lower-bounded by ↵. Then<latexit sha1_base64="Zdv1yJRAdPhY+PP3Zak2zOsE5lU=">AAAD0HicbVLLbhMxFJ0mPMrwSmHJxqJBagUdJd0UqZsCC1h0UUKbVqpD5fHcSUz9qu1pM7JGiC3fx4Y9H4JnMqIvrmTp6p7jc5+p5sy6weD3Uqd75+69+8sP4oePHj952lt5NraqMBQOqOLKHKXEAmcSDhxzHI60ASJSDofp6YcaPzwHY5mS+67UMBFkKlnOKHEhdLKy9AunMGXSCyaZJlOo/BYVVYwlXFAlBJGZx6PKY0HcLE39qLqJaV7Yq/jX11WMrlEyyFmeB842to7QUwN8wTfCBywoooV5vKvklEPuDJvOHDFGXVR4u9ZzMHdp7nEhMzB1s35/JpKqwmdnBclQvAsO9cd9lAIiqM6sJOqHzNyR/sbHd1/Qbkl0IdU5ygtJE4y4ugCzkapaMENpGdiX2phwPSNVP0Hx/gwkitshZcxqTsq69lDU2vxNuY6ZRCOE6yraRhs/RuMFzOG27ho+Jwa0ZVzJ9RhDGNI15ZIBzywidQuXzP4G0dqoOQskQCmzTBS8WWOy0Pi3wviktzpIBo2h286wdVaj1vZOen9wpmghQDrKibXHw4F2E0+MY5QHQVxY0GF1Qf04uJIIsBPfnF+FXoVIhnJlwpMONdGrPzwR1pYiDcy6P3sTa5r+D3ZcuPztxDOpCweSLhLlBUdOofqWUcYMUMfL4BBqWKgV0RkxhLpw8XFzYu3t+1TxrApjGd4cwm1nvJkMB8nw8+bqzvt2QMvRi+hltBYNo61oJ/oU7UUHEe1sd0jnW+e0O+rOu9+7PxbUzlL753l0zbo//wI6xUIy</latexit>

def

()

V (x, y)  ↵(")

yields an "-approximate bisimulation.

ses
ctn eerre ntco aragu(x, y) 2 R

q0

||x

q 0 ||  ⌘x(⌧s , q, p)qHasuo (NII, JP) 5

Discrete Abstraction via Incremental Stability[Girard, Pola, Tabuada, IEEE TAC ’10]

Discrete verification,
synthesis, supervisory control,…

For a switched dynamics ẋ = fp (x) …
<latexit sha1_base64="b1aAoYEKuxppQ5RIx5a34r84bUQ=">AAACC3icbZDLSgMxGIUz9VbrbdSlm2AR6qbMiKAboejGZQV7gXYYMmmmDc0kQ5IpLcM8gm/gVl/Anbj1Idz7IGbaWWjrgcDh/Jf8fEHMqNKO82WV1tY3NrfK25Wd3b39A/vwqK1EIjFpYcGE7AZIEUY5aWmqGenGkqAoYKQTjO/yemdCpKKCP+pZTLwIDTkNKUbaRL5t9wdCp9PsJvTTOKtNz3276tSdueCqcQtTBYWavv1tVuAkIlxjhpTquU6svRRJTTEjWaWfKBIjPEZD0jOWo4goL51fnsEzkwxgKKR5XMN5+nsiRZFSsygwnRHSI7Vcy8P/ar1Eh9deSnmcaMLx4qMwYVALmGOAAyoJ1mxmDMKSmlshHiGJsDawKv18YYEtDQQbZAaLuwxh1bQv6q5Tdx8uq43bAlAZnIBTUAMuuAINcA+aoAUwmIBn8AJerSfrzXq3PhatJauYOQZ/ZH3+ANncm6I=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="LH3bPeus+w+du5iygLcEFAPh56Y=">AAACAHicbZDNSsNAFIVv6l+tVaNbN4NFqJuSuNGNILhxWcH+QBvCZDpph04mYWZSWkIewTdwqy/gTnwR9z6IkzYLbT0wcDhn5s7lCxLOlHacL6uytb2zu1fdrx3UD4+O7ZN6V8WpJLRDYh7LfoAV5UzQjmaa034iKY4CTnvB9L7oezMqFYvFk14k1IvwWLCQEaxN5Nv2cBTrbJ7fhn6W5M35pW83nJazFNo0bmkaUKrt299mBEkjKjThWKmB6yTay7DUjHCa14apogkmUzymA2MFjqjysuXmObowyQiFsTRHaLRMf7/IcKTUIgrMzQjriVrvivC/bpDq8MbLmEhSTQVZfRSmHOkYFRjQiElKNF8Yg4lkZldEJlhiog2s2rAYWGLLgpiPcoPFXYewabpXLddpuY8OVOEMzqEJLlzDHTxAGzpAYAYv8Apv1rP1bn2sAFaskuQp/JH1+QMn1pos</latexit>
sha1_base64="o/SdJbZfj+PjZWcm6LvkTzckCEw=">AAACC3icbZC7TsMwGIUdrqXcAowsFhVSWaqEBRakChbGItGL1EaR4zitVceObKdqFeUReANWeAE2xMpDsPMgOG0GaDmSpaPzX/zrCxJGlXacL2ttfWNza7uyU93d2z84tI+OO0qkEpM2FkzIXoAUYZSTtqaakV4iCYoDRrrB+K6odydEKir4o54lxIvRkNOIYqRN5Nv2IBQ6m+Y3kZ8leX164ds1p+HMBVeNW5oaKNXy7W+zAqcx4RozpFTfdRLtZUhqihnJq4NUkQThMRqSvrEcxUR52fzyHJ6bJISRkOZxDefp74kMxUrN4sB0xkiP1HKtCP+r9VMdXXsZ5UmqCceLj6KUQS1ggQGGVBKs2cwYhCU1t0I8QhJhbWBVB8XCElsWCBbmBou7DGHVdC4brtNwH5xa87YEVAGn4AzUgQuuQBPcgxZoAwwm4Bm8gFfryXqz3q2PReuaVc6cgD+yPn8A2Jybng==</latexit>

Commonwitnesses
δ-GAS
Lyapunov func.

V

Incremental
stability(δ-GUAS)

induces8

Approximate bisimulation

Statespace abstraction

ANTOINE GIRARD, GIORDANO
AND PAULO TABUADA(Fig. from POLA,[GirardPT’10])Thm.
Let V be a common -GAS Lyapunov func. lower-bounded by ↵. Then<latexit sha1_base64="Zdv1yJRAdPhY+PP3Zak2zOsE5lU=">AAAD0HicbVLLbhMxFJ0mPMrwSmHJxqJBagUdJd0UqZsCC1h0UUKbVqpD5fHcSUz9qu1pM7JGiC3fx4Y9H4JnMqIvrmTp6p7jc5+p5sy6weD3Uqd75+69+8sP4oePHj952lt5NraqMBQOqOLKHKXEAmcSDhxzHI60ASJSDofp6YcaPzwHY5mS+67UMBFkKlnOKHEhdLKy9AunMGXSCyaZJlOo/BYVVYwlXFAlBJGZx6PKY0HcLE39qLqJaV7Yq/jX11WMrlEyyFmeB842to7QUwN8wTfCBywoooV5vKvklEPuDJvOHDFGXVR4u9ZzMHdp7nEhMzB1s35/JpKqwmdnBclQvAsO9cd9lAIiqM6sJOqHzNyR/sbHd1/Qbkl0IdU5ygtJE4y4ugCzkapaMENpGdiX2phwPSNVP0Hx/gwkitshZcxqTsq69lDU2vxNuY6ZRCOE6yraRhs/RuMFzOG27ho+Jwa0ZVzJ9RhDGNI15ZIBzywidQuXzP4G0dqoOQskQCmzTBS8WWOy0Pi3wviktzpIBo2h286wdVaj1vZOen9wpmghQDrKibXHw4F2E0+MY5QHQVxY0GF1Qf04uJIIsBPfnF+FXoVIhnJlwpMONdGrPzwR1pYiDcy6P3sTa5r+D3ZcuPztxDOpCweSLhLlBUdOofqWUcYMUMfL4BBqWKgV0RkxhLpw8XFzYu3t+1TxrApjGd4cwm1nvJkMB8nw8+bqzvt2QMvRi+hltBYNo61oJ/oU7UUHEe1sd0jnW+e0O+rOu9+7PxbUzlL753l0zbo//wI6xUIy</latexit>

def

()

V (x, y)  ↵(")

yields an "-approximate bisimulation.

ses
ctn eerre ntco aragu(x, y) 2 R

q0

||x

q 0 ||  ⌘x(⌧s , q, p)qHasuo (NII, JP) 5

Outline
The approximate bisimulation workflow
Our use: delays in switched systems
Simper setting ➜ applicability
Technical contributions
Two-step synthesis, via state-space
discretization
Case study
Hasuo (NII, JP) 6

Time Delays in Control
Networked control, IoT, …

Hasuo (NII, JP) 7

Time Delays in Control
Networked control, IoT, …

Cloud control

Hasuo (NII, JP) 7

Switched System ẋ = fp (x)<latexit sha1_base64="b1aAoYEKuxppQ5RIx5a34r84bUQ=">AAACC3icbZDLSgMxGIUz9VbrbdSlm2AR6qbMiKAboejGZQV7gXYYMmmmDc0kQ5IpLcM8gm/gVl/Anbj1Idz7IGbaWWjrgcDh/Jf8fEHMqNKO82WV1tY3NrfK25Wd3b39A/vwqK1EIjFpYcGE7AZIEUY5aWmqGenGkqAoYKQTjO/yemdCpKKCP+pZTLwIDTkNKUbaRL5t9wdCp9PsJvTTOKtNz3276tSdueCqcQtTBYWavv1tVuAkIlxjhpTquU6svRRJTTEjWaWfKBIjPEZD0jOWo4goL51fnsEzkwxgKKR5XMN5+nsiRZFSsygwnRHSI7Vcy8P/ar1Eh9deSnmcaMLx4qMwYVALmGOAAyoJ1mxmDMKSmlshHiGJsDawKv18YYEtDQQbZAaLuwxh1bQv6q5Tdx8uq43bAlAZnIBTUAMuuAINcA+aoAUwmIBn8AJerSfrzXq3PhatJauYOQZ/ZH3+ANncm6I=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="LH3bPeus+w+du5iygLcEFAPh56Y=">AAACAHicbZDNSsNAFIVv6l+tVaNbN4NFqJuSuNGNILhxWcH+QBvCZDpph04mYWZSWkIewTdwqy/gTnwR9z6IkzYLbT0wcDhn5s7lCxLOlHacL6uytb2zu1fdrx3UD4+O7ZN6V8WpJLRDYh7LfoAV5UzQjmaa034iKY4CTnvB9L7oezMqFYvFk14k1IvwWLCQEaxN5Nv2cBTrbJ7fhn6W5M35pW83nJazFNo0bmkaUKrt299mBEkjKjThWKmB6yTay7DUjHCa14apogkmUzymA2MFjqjysuXmObowyQiFsTRHaLRMf7/IcKTUIgrMzQjriVrvivC/bpDq8MbLmEhSTQVZfRSmHOkYFRjQiElKNF8Yg4lkZldEJlhiog2s2rAYWGLLgpiPcoPFXYewabpXLddpuY8OVOEMzqEJLlzDHTxAGzpAYAYv8Apv1rP1bn2sAFaskuQp/JH1+QMn1pos</latexit>
sha1_base64="o/SdJbZfj+PjZWcm6LvkTzckCEw=">AAACC3icbZC7TsMwGIUdrqXcAowsFhVSWaqEBRakChbGItGL1EaR4zitVceObKdqFeUReANWeAE2xMpDsPMgOG0GaDmSpaPzX/zrCxJGlXacL2ttfWNza7uyU93d2z84tI+OO0qkEpM2FkzIXoAUYZSTtqaakV4iCYoDRrrB+K6odydEKir4o54lxIvRkNOIYqRN5Nv2IBQ6m+Y3kZ8leX164ds1p+HMBVeNW5oaKNXy7W+zAqcx4RozpFTfdRLtZUhqihnJq4NUkQThMRqSvrEcxUR52fzyHJ6bJISRkOZxDefp74kMxUrN4sB0xkiP1HKtCP+r9VMdXXsZ5UmqCceLj6KUQS1ggQGGVBKs2cwYhCU1t0I8QhJhbWBVB8XCElsWCBbmBou7DGHVdC4brtNwH5xa87YEVAGn4AzUgQuuQBPcgxZoAwwm4Bm8gFfryXqz3q2PReuaVc6cgD+yPn8A2Jybng==</latexit>

Def.
n
(R
, P, P, F )A switched system is a quadruple• Rn: state space• P = {1, · · · , m} : finite set of modes• P ✓ R+ ! P : the set of switching signals(piecewise constant functions that arecontinuous from the right and non-Zeno)• F = {f1 , · · · , fm } : a set of functions( fp : R ! R for each mode p )nnNotationp : modep : switching signal
Hasuo (NII, JP) 8

Trajectory of Switched Systems
Given a switching signal p ,• x(t) 2 Rnbehaves according to ẋ(t) = fp (x(t))

while p(t) = p .
• x(t) 2 Rnis continuous even at switching

Hasuo (NII, JP) 9

Periodic Switched Systems

cf. [Al Khatib et al., HSCC’16]

Periodic: k-th switching occurs at
t = k⌧ (k 2 N)
Nearly periodic: k-th switching occurs at
t 2 [k⌧, k⌧ + 0 ](k 2 N)

Our assumption:
Switching delays do not accumulatekτ(k+1)τ

(k+2)τ
t

≤δ0

≤δ0

≤δ0
Hasuo (NII, JP) 10

Periodic Switched Systems

cf. [Al Khatib et al., HSCC’16]

Periodic: k-th switching occurs at
t = k⌧ (k 2 N)
Nearly periodic: k-th switching occurs at
t 2 [k⌧, k⌧ + 0 ]Our assumption:
Switching delays do not accumulatekτ(k+1)τ

(k 2 N)≤δ0(k+2)τ

exactly kτ
Plant

t

actuator

sensorController

≤δ0

≤δ0

≤δ0
Hasuo (NII, JP) 10

Switched System with Actuation Delaysẋ = f1 (x)ẋ = f2 (x)

≤δ0

≤δ0

≤δ0

Ideal, without delay≤δ0

Actual, with delay

τ

2τ

3τ

4τ

t
Hasuo (NII, JP) 11

ẋ = f1 (x)ẋ = f2 (x)
≤δ0

≤δ0
τ

2τ

≤δ0
3τ

≤δ0
4τ

Ideal, without delayt

Actual, with delay

Hasuo (NII, JP) 12

ẋ = f1 (x)ẋ = f2 (x)
≤δ0

≤δ0
τ

2τ

≤δ0
3τ

≤δ0
4τ

Ideal, without delayt

Actual, with delayThm. If the switched system has a common δ-GAS
Lyapunov function V, then the gap (L∞ dist.,
✓
◆
⌫ 0
1
↵
1 e (⌧ 0 )) is bounded by<latexit sha1_base64="QtOVjoJ4nsLHd/3PcZICSmWaF54=">AAACWHicbVHLjtMwFHXDY2bCqwxLNhEVUmfRKhkhwXIEG5aDRGdGqkN149y0Vh3Hsm+QKitfx1fAmg1b+AGcTiRghitZOjqPa+u4MEo6StOvo+jO3Xv3Dw6P4gcPHz1+Mn56fOGa1gpciEY19qoAh0pqXJAkhVfGItSFwsti+67XLz+jdbLRH2lnMK9hrWUlBVCgVuM84a0u0fZ5z0GZDXSf/CzrYq6womnMKwvCc93yEhXByqdd57MZBhPfgjEw5QTt7I960oWslesNncSr8SSdp/tJboNsABM2zPlq/J2XjWhr1CQUOLfMUkO5B0tSKAyLW4cGxBbWuAxQQ40u9/sauuRlYMqkamw4mpI9+3fCQ+3cri6CswbauJtaT/5PW7ZUvcm91KYl1OL6oqpVCTVJ32lSSouC1C4AEFaGtyZiA6E3Cs3HvF84/IEvGlV2oZbsZgm3wcXpPEvn2YdXk7O3Q0GH7Dl7waYsY6/ZGXvPztmCCfaF/WA/2a/Rt4hFB9HRtTUaDZln7J+Jjn8D7/y2gA==</latexit>

Here α, κ, ν are param’s of the dynamics and V.

Hasuo (NII, JP) 12

ẋ = f1 (x)ẋ = f2 (x)
≤δ0

≤δ0
τ

2τ

≤δ0
3τ

≤δ0
4τ

Ideal, without delayt

Actual, with delayThm. If the switched system has a common δ-GAS
Lyapunov function V, then the gap (L∞ dist.,
✓
◆
⌫ 0
1
↵
1 e (⌧ 0 )) is bounded by<latexit sha1_base64="QtOVjoJ4nsLHd/3PcZICSmWaF54=">AAACWHicbVHLjtMwFHXDY2bCqwxLNhEVUmfRKhkhwXIEG5aDRGdGqkN149y0Vh3Hsm+QKitfx1fAmg1b+AGcTiRghitZOjqPa+u4MEo6StOvo+jO3Xv3Dw6P4gcPHz1+Mn56fOGa1gpciEY19qoAh0pqXJAkhVfGItSFwsti+67XLz+jdbLRH2lnMK9hrWUlBVCgVuM84a0u0fZ5z0GZDXSf/CzrYq6womnMKwvCc93yEhXByqdd57MZBhPfgjEw5QTt7I960oWslesNncSr8SSdp/tJboNsABM2zPlq/J2XjWhr1CQUOLfMUkO5B0tSKAyLW4cGxBbWuAxQQ40u9/sauuRlYMqkamw4mpI9+3fCQ+3cri6CswbauJtaT/5PW7ZUvcm91KYl1OL6oqpVCTVJ32lSSouC1C4AEFaGtyZiA6E3Cs3HvF84/IEvGlV2oZbsZgm3wcXpPEvn2YdXk7O3Q0GH7Dl7waYsY6/ZGXvPztmCCfaF/WA/2a/Rt4hFB9HRtTUaDZln7J+Jjn8D7/y2gA==</latexit>

Here α, κ, ν are param’s of the dynamics and V.

No accumulationofHasuo (NII, JP) 12

Approximate Bisimulation[Girard & Pappas, IEEE Transactions on Automatic Control’07]

Ti = (Qi , L, !, O, Hi ) for i = 1, 2i(O equipped with a metric d)Def.
R" ✓ Q1 ⇥ Q2 is an εapproximate bisimulation
relation between T1 and T2 if
for all (q1 , q2 ) 2 R" ,

T1

T2

R"
l

l
R"

• d(H1 (q1 ), H2 (q2 ))  ✏
l

l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
1
2
1
2
1 2 ) 2 R"
1
2
l
l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
2
1
2
1
1 2 ) 2 R"
2
1
Hasuo (NII, JP) 13

Approximate Bisimulation[Girard & Pappas, IEEE Transactions on Automatic Control’07]

Ti = (Qi , L, !, O, Hi ) for i = 1, 2i(O equipped with a metric d)Def.
R" ✓ Q1 ⇥ Q2 is an εapproximate bisimulation
relation between T1 and T2 if
for all (q1 , q2 ) 2 R" ,

T1

T2

R"
l

l
R"

• d(H1 (q1 ), H2 (q2 ))  ✏
l

l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
1
2
1
2
1 2 ) 2 R"
1
2
l
l
0
0
0
0
8q
!
q
,
9q
!
q
,
s.t.
(q
,
q
•
2
1
2
1
1 2 ) 2 R"
2
1

Our proof is by approximate
bisimulation…
Key: what are states q1, q2?
Hasuo (NII, JP) 13

Transition Systems for Switched Systems
delayed systemdelay-free model

T (⌃⌧ )

T (⌃⌧, 0 )

p

R✏

p

R✏

Hasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free model

T (⌃⌧ )

T (⌃⌧, 0 )

p

R✏

R✏

0

(x , k⌧, p)p(x(⌧, x0 , p), (k + 1)⌧, p0 )Hasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free model

T (⌃⌧ )

T (⌃⌧, 0 )

p

R✏

R✏

0

(x , k⌧, p)p(x(⌧, x0 , p), (k + 1)⌧, p0 )States are switching
pointsHasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

T (⌃⌧ )

T (⌃⌧, 0 )(x, t 2 [k⌧, k⌧ + 0 ], p)
(x(t0

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free modelt, x, p),

p

R✏

0

(x , k⌧, p)p

t0 2 [(k + 1)⌧, (k + 1)⌧ + 0 ],
p0 )

R✏

(x(⌧, x0 , p), (k + 1)⌧, p0 )States are switching
pointsHasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

T (⌃⌧ )

T (⌃⌧, 0 )(x, t 2 [k⌧, k⌧ + 0 ], p)
(x(t0

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free modelpt, x, p),R✏0(x , k⌧, p)p

t0 2 [(k + 1)⌧, (k + 1)⌧ + 0 ],p0 )R✏… that can delay(x(⌧, x0 , p), (k + 1)⌧, p0 )States are switching
pointsHasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

T (⌃⌧ )

T (⌃⌧, 0 )(x, t 2 [k⌧, k⌧ + 0 ], p)
(x(t0

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free modelpt, x, p),R✏0(x , k⌧, p)p

t0 2 [(k + 1)⌧, (k + 1)⌧ + 0 ],
p0 )

R✏

x

x’

… that can delay(x(⌧, x0 , p), (k + 1)⌧, p0 )States are switching
pointst’tHasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

T (⌃⌧ )

T (⌃⌧, 0 )(x, t 2 [k⌧, k⌧ + 0 ], p)
(x(t0

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free modelpt, x, p),R✏0(x , k⌧, p)p

t0 2 [(k + 1)⌧, (k + 1)⌧ + 0 ],
p0 )

R✏

x

x’

States are switching
pointsnott’… that can delay(x(⌧, x0 , p), (k + 1)⌧, p0 )tHasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

T (⌃⌧ )

T (⌃⌧, 0 )(x, t 2 [k⌧, k⌧ + 0 ], p)
(x(t0

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free modelpt, x, p),R✏0(x , k⌧, p)p

t0 2 [(k + 1)⌧, (k + 1)⌧ + 0 ],
p0 )

R✏

x

x’

not

t’

but

t

… that can delay(x(⌧, x0 , p), (k + 1)⌧, p0 )States are switching
pointsHasuo (NII, JP) 14

Transition Systems for Switched Systems
delayed system

T (⌃⌧ )

T (⌃⌧, 0 )(x, t 2 [k⌧, k⌧ + 0 ], p)
(x(t0

L=P
O = R n ⇥ R+ ⇥ P
H : canonical embedding

delay-free modelpt, x, p),R✏0(x , k⌧, p)p

t0 2 [(k + 1)⌧, (k + 1)⌧ + 0 ],
p0 )

R✏

x

x’

not

t’

but

t

… that can delay(x(⌧, x0 , p), (k + 1)⌧, p0 )States are switching
pointsHasuo (NII, JP) 14

Example I: Boost DC-DC Converter[BeccutiPM, CDC’05] [GirardPT, IEEE Tranc. Autom. Ctrl. ’10]

rl

xl

il
rc
ro

Vs
xc

vc

<latexit sha1_base64="E5ol5769kg4bNOn1iEpnmklYYBM=">AAADcHicbVLLbtNAFB3HPIp5pXSDxIKBBKmtUssOSlupCqooCxYsCiJppdiyxuNJMsr4oZlx2mDl6/gKPoFt2bJg/EBx2lxppKtzzj33ztX1E0aFtKxfWkO/d//Bw61HxuMnT589b26/GIo45ZgMcMxifukjQRiNyEBSychlwgkKfUYu/NlZzl/MCRc0jr7LRULcEE0iOqYYSQV525rjCIwY8ePrzDxaZtDxyYRGGaYcp1TS2Y+lAZ2AoysD7lodaO1BGY+G/fbQE223gLpmb8/I0W8dyPpt7rGcsM33NepLQV0rqgPph36blqK6RFxRiaclaCno4KBqeGKsJii4guqVKlV4Vnlj5T1X3nOVuYXAXp/rP1y2zE0ON0wf56rD1Qy9DTPkRXnNp5XhiRKQKKgvbml4zZZlWkXAu4ldJS1QxbnX/OsEMU5DEknMkBAj20qkmyEuKWZkaTipIAnCMzQhI5VGKCTCzYozWMJ3CgngOObqRRIWaL0iQ6EQi9BXyhDJqbjN5eAmbpTK8bGb0ShJJYlw2WicMrUBmN8UDCgnWLKFShDm6vMY4iniCEt1eYaTG1Y3mPkxC9a+UV+YWpd9ezl3k2HXtC3T/tptnX6sFrcFXoG3YBfY4Aicgs/gHAwA1n5qv7Ub7U/jRn+pv9bflNKGVtXsgLXQ9/8BeAb3Nw==</latexit>

for p 2 {ON, OFF} , where
#
 vs
rl
0
xl
xl
AON =
,
b
=
and
1
0
0
xc (ro +rc )" r r +r r +r r#
r r +r r +r r
ẋ(t) = Ap x(t) + b"l o

AOFF =l co c

xl (ro +rc )roxc (ro +rc )

l o

l c

o c

xl (ro +rc )1
xc (ro +rc ).

<latexit sha1_base64="IFCsVCwiaU2fd5CocaXUsxVbL2M=">AAAEVnicjVNbTxQxFB6WRXC8gT76ciKRgMBmhhd9IYImG58EE7kkdDPpdLpLw0w7th1YbOYX+Kr/Tf8M8cwFgYVE+tB8Pdevp1/jPBXGBsGfqc50d+bB7NxD/9HjJ0+fzS883zeq0IzvMZUqfRhTw1Mh+Z4VNuWHueY0i1N+EJ98rPwHp1wboeRXe57zQUZHUgwFoxZN0cLUBYn5SEhHUzGSb0p/CUiirBuXy3YFNmE7ymFcwVWIgXwraEIsH1s3VBrKnAhJHNn5vAZkp98nJeHS5JTxtSYIzo655qVPCJbdjqrIEjZ9aFvGGbVajEsfYJ0MNWVOR2npxrjBEgSYBRAgap1h5WLLOlKrOmIrmIbtkn9V1vyGn49E7+zRVDmNTNOiKT9RBFriVCblFet+/7+0AWnhjBrEaqQqVPe64nx1m/vn1EQvk9TEEO49nsun6fm1+fK5o/nFoBfUC26DsAWLXrt2UTHvUSCsyLi0LKXGHIVBbgeOaitYWj12YTg2OqEjfoRQ0oybgauVWsJrtCRQiWeopIXaej3D0cyY8yzGSOR9bCZ9lfEu31Fhh+8GTsi8sFyyptGwSMEqqGQPidCc2fQcAWVaIFdgxxTnZvFz+KQq2H4TF6s0uXENx4RmBeacfEe75GdMZRkqpNazc7VkhHV4KCf9qJxrAXgq65GHkwO+DfY3emHQC79sLG59aIc/5730XnnLXui99ba8T96ut+exDu/86Pzs/Jr+PX3RnenONqGdqTbnhXdjdef/AiOjZps=</latexit>

Hasuo (NII, JP) 15

Example I: Boost DC-DC Converter[BeccutiPM, CDC’05] [GirardPT, IEEE TAC ’10]

rl

xl

il
rc
ro

Vs
xc

vc

for p 2 {ON, OFF} , where
#
 vs
rl
0
xl
AON =
, b = xl and
100xc (ro +rc )" r r +r r +r r#
r r +r r +r r
ẋ(t) = Ap x(t) + b"
l o<latexit sha1_base64="E5ol5769kg4bNOn1iEpnmklYYBM=">AAADcHicbVLLbtNAFB3HPIp5pXSDxIKBBKmtUssOSlupCqooCxYsCiJppdiyxuNJMsr4oZlx2mDl6/gKPoFt2bJg/EBx2lxppKtzzj33ztX1E0aFtKxfWkO/d//Bw61HxuMnT589b26/GIo45ZgMcMxifukjQRiNyEBSychlwgkKfUYu/NlZzl/MCRc0jr7LRULcEE0iOqYYSQV525rjCIwY8ePrzDxaZtDxyYRGGaYcp1TS2Y+lAZ2AoysD7lodaO1BGY+G/fbQE223gLpmb8/I0W8dyPpt7rGcsM33NepLQV0rqgPph36blqK6RFxRiaclaCno4KBqeGKsJii4guqVKlV4Vnlj5T1X3nOVuYXAXp/rP1y2zE0ON0wf56rD1Qy9DTPkRXnNp5XhiRKQKKgvbml4zZZlWkXAu4ldJS1QxbnX/OsEMU5DEknMkBAj20qkmyEuKWZkaTipIAnCMzQhI5VGKCTCzYozWMJ3CgngOObqRRIWaL0iQ6EQi9BXyhDJqbjN5eAmbpTK8bGb0ShJJYlw2WicMrUBmN8UDCgnWLKFShDm6vMY4iniCEt1eYaTG1Y3mPkxC9a+UV+YWpd9ezl3k2HXtC3T/tptnX6sFrcFXoG3YBfY4Aicgs/gHAwA1n5qv7Ub7U/jRn+pv9bflNKGVtXsgLXQ9/8BeAb3Nw==</latexit>

AOFF =l co c

xl (ro +rc )roxc (ro +rc )

l o

l c

o c

xl (ro +rc )1
xc (ro +rc ).

<latexit sha1_base64="IFCsVCwiaU2fd5CocaXUsxVbL2M=">AAAEVnicjVNbTxQxFB6WRXC8gT76ciKRgMBmhhd9IYImG58EE7kkdDPpdLpLw0w7th1YbOYX+Kr/Tf8M8cwFgYVE+tB8Pdevp1/jPBXGBsGfqc50d+bB7NxD/9HjJ0+fzS883zeq0IzvMZUqfRhTw1Mh+Z4VNuWHueY0i1N+EJ98rPwHp1wboeRXe57zQUZHUgwFoxZN0cLUBYn5SEhHUzGSb0p/CUiirBuXy3YFNmE7ymFcwVWIgXwraEIsH1s3VBrKnAhJHNn5vAZkp98nJeHS5JTxtSYIzo655qVPCJbdjqrIEjZ9aFvGGbVajEsfYJ0MNWVOR2npxrjBEgSYBRAgap1h5WLLOlKrOmIrmIbtkn9V1vyGn49E7+zRVDmNTNOiKT9RBFriVCblFet+/7+0AWnhjBrEaqQqVPe64nx1m/vn1EQvk9TEEO49nsun6fm1+fK5o/nFoBfUC26DsAWLXrt2UTHvUSCsyLi0LKXGHIVBbgeOaitYWj12YTg2OqEjfoRQ0oybgauVWsJrtCRQiWeopIXaej3D0cyY8yzGSOR9bCZ9lfEu31Fhh+8GTsi8sFyyptGwSMEqqGQPidCc2fQcAWVaIFdgxxTnZvFz+KQq2H4TF6s0uXENx4RmBeacfEe75GdMZRkqpNazc7VkhHV4KCf9qJxrAXgq65GHkwO+DfY3emHQC79sLG59aIc/5730XnnLXui99ba8T96ut+exDu/86Pzs/Jr+PX3RnenONqGdqTbnhXdjdef/AiOjZps=</latexit>

After rescaling, a common Lyapunov func. is found[GirardPT’10]

V (x, y) =<latexit sha1_base64="w6nwXzR2EK8LaYfuRSBHzqzeR4k=">AAACx3icbVFdb9MwFHUCGyN8rINHXixaUCdBlZRJ7GViYtIED4Mhrd2kulSO47ZWHTvYzpZg5WF/ctL+Cw84XSS2jitZOj7nXH+cG2ecaROG157/4OHa+qONx8GTp8+eb7a2Xgy1zBWhAyK5VGcx1pQzQQeGGU7PMkVxGnN6Gi8Oav30nCrNpDgxZUbHKZ4JNmUEG0dNWlln2C3ewXIb7kGkfylju8X7cvvnCTyCS1R1ggtm5kHnaC9AMZ0xYeMUG8WKKoBRL+z3d+BbGPbCcHcHoaBBjnJa+CGCAaIi+dfSmbTataUueB9EDWiDpo4nW94nlEiSp1QYwrHWoyjMzNhiZRjhtApQrmmGyQLP6MhBgVOqx3YZTQXfOCaBU6ncEgYu2dsdFqdal2nsnO6Jc72q1eT/tFFuprtjy0SWGyrIzUXTnEMjYZ0zTJiixPDSAUwUc2+FZI4VJsZNI0D1gc1cbCx5cucbljBFctez+O14QS+ITFPsYkTfv1XWIkMLN2rrNtWqfnh42+B2zuEij1YDvg+G/V4U9qIf/fb+5yb8DfAKvAZdEIGPYB98AcdgAAi4An+8NW/d/+pL/9wvbqy+1/S8BHfKv/wLsw/Wmg==</latexit>
sha1_base64="7YvT2DCF4Bp8tPLi94D0htDgI+k=">AAACR3icbVHLSgMxFM20Vmut2q7dDBbBVZlxozsFobjSCvYBnVIymds2NI8hyag19Afc+m+C/+LC9LHowwuBc8+5N7n3JE4Z1SYIfrxcfq+wf1A8LB2VS8cnp5VyW8tMEWgRyaTqxlgDowJahhoG3VQB5jGDTjy5n+udV1CaSvFipin0OR4JOqQEG0c1B5VaUA8W4e+CcAVqaBWDqncbJZJkHIQhDGvdC4PU9C1WhhIGs1KUaUgxmeAR9BwUmIPu28WcM//CMYk/lModYfwFu95hMdd6ymNXybEZ621tTv6n9TIzvOlbKtLMgCDLh4YZ843050v7CVVADJs6gImiblafjLHCxDhrStH8wpVJNpYs2VjDEqpI5nomH44X8EYk51gkNnp6nFkbGXh3vluXzLb1RmO9wGWuwjkebvu7C9pX9TCoh88BKqIzdI4uUYiu0R16QE3UQgQl6BN9ed/eby6//Jmct/qiKtqIXOEP2Mu1Sg==</latexit>
sha1_base64="+ils4kwJ7Kdc+6AiEYqnwZyXGFk=">AAACvHicbVFdb9MwFHUCGyMM6PbKi8UK6iSonDKJvUwgIU3wMBjS2k2qS+U4bmvVsTPb2RKs/E0k/gsPOF0kto4rWTo+515/nJPkghuL0O8gfPBwY/PR1uPoyfbTZ887O9sjowpN2ZAqofRFQgwTXLKh5Vawi1wzkiWCnSfLT41+fsW04Uqe2Spnk4zMJZ9xSqynpp28O+qVb2C1D48gNpfaul75ttr/cQZP4ArV3eia20XUPTmKcMLmXLokI1bzso5g3EeDwQF8DVEfocMDjKMWecpr6F0MI8xk+m+kO+3sNS1NwfsgbsEeaOt0uhN8wKmiRcakpYIYM45RbieOaMupYHWEC8NyQpdkzsYeSpIxM3Era2r4yjMpnCntl7Rwxd6ecCQzpsoS3+mfuDDrWkP+TxsXdnY4cVzmhWWS3lw0KwS0CjY+w5RrRq2oPCBUc/9WSBdEE2p9GhFuDmxzcYkS6Z1vOMo1LfzM8qfnJbumKsuItxF/+1o7hy0rfdTOb+p1/fj4doPf+Q5vebxu8H0wGvRj1I+/I7AFXoCXoAdi8B58BJ/BKRgCCn6BP8FGsBl+CVV4dRNOGLQp7YI7FZZ/AWu31Wk=</latexit>
sha1_base64="KooJ+21LneRo9UJlY0kAWRWNPDU=">AAACx3icbVFdb9MwFHUCGyN8rINHXixaUCdB5ZRJ7GViAmmCh8GQ1m5SXSrHcVurjh1sZ0ux8sCfROK/8IDTRWLruJKl43PO9ce5SS64sQj9DsI7dzc2723djx48fPR4u7XzZGhUoSkbUCWUPk+IYYJLNrDcCnaea0ayRLCzZPGh1s8umDZcyVO7zNk4IzPJp5wS66lJK+8Mu+UruNyFBxCb79q6bvl6ufvtFB7DFao60SW386hzfBDhhM24dElGrOZlFcG4h/r9PfgSoh5C+3sYRw3ylNfQmxhGmMn0X0tn0mrXlrrgbRA3oA2aOpnsBO9wqmiRMWmpIMaMYpTbsSPacipYFeHCsJzQBZmxkYeSZMyM3SqaCr7wTAqnSvslLVyx1zscyYxZZol3+ifOzbpWk//TRoWd7o8dl3lhmaRXF00LAa2Cdc4w5ZpRK5YeEKq5fyukc6IJtX4aEa4PbObiEiXSG99wlGta+J7FD89LdklVlhEfI/7yuXIOW1b6UTu/qdb1o6PrBr/zDh95vB7wbTDs92LUi7+i9uH7Jvwt8Aw8B10Qg7fgEHwEJ2AAKPgF/gQbwWb4KVThRVheWcOg6XkKblT48y+yb9aY</latexit>p(xy)T M (x

1.0224 0.0084y) with M =0.0084 1.0031

with parameters ↵(s) = s, ↵(s) = 1.0127s and  = 0.014.
<latexit sha1_base64="/6+ObFXTi2Z4vRhvfOwGPr8IQ6Y=">AAACuXicbVFda9swFFW8ry77SrvHvYglgw5GsMOggzFaVih72jpY2kIcwrWs1GpkSUhyu0z4/+0v9E/sdXvcdeqHNu0FwdE5515JR5mRwvk4vuxE9+4/ePho43H3ydNnz1/0NreOnK4s42OmpbYnGTguheJjL7zkJ8ZyKDPJj7PFfqMfn3PrhFY//NLwaQmnSswFA4/UrJddCF9QAxZK7tHXpYO0Ujm3zcCQgjQF1NvuLf1E3Tua6vO7lGQYJ6MdN6CgcuxfgDGAdIz0+8Fw1usjWhW9DZIW9Elbh7PNzm6aa1aVXHkmwblJEhs/DWC9YJLX3bRy3ABbwCmfIFR4dzcNqzBq+gaZnM61xaU8XbHXOwKUzi3LDJ0l+MKtaw15lzap/PzDNAhlKs8VuzpoXknqNW2SpbmwnHm5RADMCrwrZQUGy1a5ps3A9idCpmV+4xmBCcsq7Fn8Ql7xC6bLEtMM6bevdQip5z/xcwNu6nX94OC6AXfowMiT9YBvg6PRMImHyfdRf+9zG/4GeUVek22SkB2yR76QQzImjPwmf8hf8i/6GEFURGdX1qjT9rwkNypy/wHoX9i3</latexit>⌧
switchinginterval
⌧
=
0.5
and
the
maximumdelay=
Now with01000
we use our main theorem to derive the error bound "1 = 0.0294176<latexit sha1_base64="SN5FjIm4ZFEe4tl/MVjKmEpjIpc=">AAACr3icbZHNbhMxFIWd4a+EvxSWbCwSJFaRp1IFG0QFUsUKikSaSEkIdzw3iRXbM7I9bYM1r8Z7sGcLz8BNOos25UqjOT73XI/9TVZq5YMQv1rJrdt37t7bu99+8PDR4yed/aenvqicxIEsdOFGGXjUyuIgqKBxVDoEk2kcZqsPm/7wDJ1Xhf0a1iVODSysmisJgaxZZ+TPVZBLZRdc2YDuDDTvTQJU/C0X/cMeb3OwOQ9L5AYulKkMz1HDmkL0DjCLoqboZO5Axs1cHVMhRN2bdbqiL7bFb4q0EV3W1Mlsv/VukheyMmiD1OD9OBVlmEZwQUmNdXtSeSxBrmCBY5IWDPpp3CKo+Utycj4vHD028K17dSKC8X5tMkoaCEu/29uY/+uNqzB/M43KllVAKy8/NK80DwXf8OS5ciiDXpMA6RSdlcslEA2CSTttNmz4x6zQ+bVrRKmcrGhm9YN8i+eyMIZwx8nnT3UknHhBvzTSot7tHx9fDdCKEoQ83QV8U5we9FPRT78cdI/eN/D32HP2gr1iKXvNjthHdsIGTLKf7Df7w/4maTJMviXfL6NJq5l5xq5Vov4BIvTWWw==</latexit><latexit sha1_base64="semIRilsKDcDEdhHYdwykPu1c2o=">AAACdHicbVHLThsxFHWG0kJaaKDLtpLVgMQqmomqAgsEohLqqqVSA0iZKPJ4bsCKHyPbA6TWrPiabsvX8COsexNmAaFXsnQe9/pxnBVSOB/Hd41o4cXiy1dLy83Xb1ZW37bW1k+cKS2HHjfS2LOMOZBCQ88LL+GssMBUJuE0G3+d+qeXYJ0w+pefFDBQ7FyLkeDMozRsfdxIL5mFwgmJNCQV3aNxJ+7ufk62v2wMW20ks6LPQVKDNqnreLjW2E9zw0sF2nPJnOsnceEHgVkvuISqmZYOCsbH7Bz6CDVT4AZh9o6KbqKS05GxuLSnM/XxRGDKuYnKsFMxf+Hmvan4P69f+tHOIAhdlB40fzhoVErqDZ2GQnNhgXs5QcC4FXhXyi+YZdxjdM10umEdYsiMzJ88I3BheYkz49+oa7jiRimm85D++F6FkHq4xn8JSKp5/+jocQMy7MDIk/mAn4OTbieJO8nPbvvgsA5/ibwnn8gWScg2OSDfyDHpEU5uyB/yl9w27qMPUTvafGiNGvXMO/Kkos4/FkzABA==</latexit>

Hasuo (NII, JP) 16

Example I: Boost DC-DC Converter[BeccutiPM, CDC’05] [GirardPT, IEEE TAC ’10]

rl

xl

il
rc
ro

Vs
xc

vc

for p 2 {ON, OFF} , where
#
 vs
rl
0
xl
AON =
, b = xl and
100xc (ro +rc )" r r +r r +r r#
r r +r r +r r
ẋ(t) = Ap x(t) + b"
l o<latexit sha1_base64="E5ol5769kg4bNOn1iEpnmklYYBM=">AAADcHicbVLLbtNAFB3HPIp5pXSDxIKBBKmtUssOSlupCqooCxYsCiJppdiyxuNJMsr4oZlx2mDl6/gKPoFt2bJg/EBx2lxppKtzzj33ztX1E0aFtKxfWkO/d//Bw61HxuMnT589b26/GIo45ZgMcMxifukjQRiNyEBSychlwgkKfUYu/NlZzl/MCRc0jr7LRULcEE0iOqYYSQV525rjCIwY8ePrzDxaZtDxyYRGGaYcp1TS2Y+lAZ2AoysD7lodaO1BGY+G/fbQE223gLpmb8/I0W8dyPpt7rGcsM33NepLQV0rqgPph36blqK6RFxRiaclaCno4KBqeGKsJii4guqVKlV4Vnlj5T1X3nOVuYXAXp/rP1y2zE0ON0wf56rD1Qy9DTPkRXnNp5XhiRKQKKgvbml4zZZlWkXAu4ldJS1QxbnX/OsEMU5DEknMkBAj20qkmyEuKWZkaTipIAnCMzQhI5VGKCTCzYozWMJ3CgngOObqRRIWaL0iQ6EQi9BXyhDJqbjN5eAmbpTK8bGb0ShJJYlw2WicMrUBmN8UDCgnWLKFShDm6vMY4iniCEt1eYaTG1Y3mPkxC9a+UV+YWpd9ezl3k2HXtC3T/tptnX6sFrcFXoG3YBfY4Aicgs/gHAwA1n5qv7Ub7U/jRn+pv9bflNKGVtXsgLXQ9/8BeAb3Nw==</latexit>

AOFF =

l c

Lyapunovfunctiono cxl (ro +rc )roxc (ro +rc )

l o

l c

o c

xl (ro +rc )1
xc (ro +rc ).

<latexit sha1_base64="IFCsVCwiaU2fd5CocaXUsxVbL2M=">AAAEVnicjVNbTxQxFB6WRXC8gT76ciKRgMBmhhd9IYImG58EE7kkdDPpdLpLw0w7th1YbOYX+Kr/Tf8M8cwFgYVE+tB8Pdevp1/jPBXGBsGfqc50d+bB7NxD/9HjJ0+fzS883zeq0IzvMZUqfRhTw1Mh+Z4VNuWHueY0i1N+EJ98rPwHp1wboeRXe57zQUZHUgwFoxZN0cLUBYn5SEhHUzGSb0p/CUiirBuXy3YFNmE7ymFcwVWIgXwraEIsH1s3VBrKnAhJHNn5vAZkp98nJeHS5JTxtSYIzo655qVPCJbdjqrIEjZ9aFvGGbVajEsfYJ0MNWVOR2npxrjBEgSYBRAgap1h5WLLOlKrOmIrmIbtkn9V1vyGn49E7+zRVDmNTNOiKT9RBFriVCblFet+/7+0AWnhjBrEaqQqVPe64nx1m/vn1EQvk9TEEO49nsun6fm1+fK5o/nFoBfUC26DsAWLXrt2UTHvUSCsyLi0LKXGHIVBbgeOaitYWj12YTg2OqEjfoRQ0oybgauVWsJrtCRQiWeopIXaej3D0cyY8yzGSOR9bCZ9lfEu31Fhh+8GTsi8sFyyptGwSMEqqGQPidCc2fQcAWVaIFdgxxTnZvFz+KQq2H4TF6s0uXENx4RmBeacfEe75GdMZRkqpNazc7VkhHV4KCf9qJxrAXgq65GHkwO+DfY3emHQC79sLG59aIc/5730XnnLXui99ba8T96ut+exDu/86Pzs/Jr+PX3RnenONqGdqTbnhXdjdef/AiOjZps=</latexit>

After rescaling, a common Lyapunov func. is found[GirardPT’10]

V (x, y) =<latexit sha1_base64="w6nwXzR2EK8LaYfuRSBHzqzeR4k=">AAACx3icbVFdb9MwFHUCGyN8rINHXixaUCdBlZRJ7GViYtIED4Mhrd2kulSO47ZWHTvYzpZg5WF/ctL+Cw84XSS2jitZOj7nXH+cG2ecaROG157/4OHa+qONx8GTp8+eb7a2Xgy1zBWhAyK5VGcx1pQzQQeGGU7PMkVxGnN6Gi8Oav30nCrNpDgxZUbHKZ4JNmUEG0dNWlln2C3ewXIb7kGkfylju8X7cvvnCTyCS1R1ggtm5kHnaC9AMZ0xYeMUG8WKKoBRL+z3d+BbGPbCcHcHoaBBjnJa+CGCAaIi+dfSmbTataUueB9EDWiDpo4nW94nlEiSp1QYwrHWoyjMzNhiZRjhtApQrmmGyQLP6MhBgVOqx3YZTQXfOCaBU6ncEgYu2dsdFqdal2nsnO6Jc72q1eT/tFFuprtjy0SWGyrIzUXTnEMjYZ0zTJiixPDSAUwUc2+FZI4VJsZNI0D1gc1cbCx5cucbljBFctez+O14QS+ITFPsYkTfv1XWIkMLN2rrNtWqfnh42+B2zuEij1YDvg+G/V4U9qIf/fb+5yb8DfAKvAZdEIGPYB98AcdgAAi4An+8NW/d/+pL/9wvbqy+1/S8BHfKv/wLsw/Wmg==</latexit>
sha1_base64="7YvT2DCF4Bp8tPLi94D0htDgI+k=">AAACR3icbVHLSgMxFM20Vmut2q7dDBbBVZlxozsFobjSCvYBnVIymds2NI8hyag19Afc+m+C/+LC9LHowwuBc8+5N7n3JE4Z1SYIfrxcfq+wf1A8LB2VS8cnp5VyW8tMEWgRyaTqxlgDowJahhoG3VQB5jGDTjy5n+udV1CaSvFipin0OR4JOqQEG0c1B5VaUA8W4e+CcAVqaBWDqncbJZJkHIQhDGvdC4PU9C1WhhIGs1KUaUgxmeAR9BwUmIPu28WcM//CMYk/lModYfwFu95hMdd6ymNXybEZ621tTv6n9TIzvOlbKtLMgCDLh4YZ843050v7CVVADJs6gImiblafjLHCxDhrStH8wpVJNpYs2VjDEqpI5nomH44X8EYk51gkNnp6nFkbGXh3vluXzLb1RmO9wGWuwjkebvu7C9pX9TCoh88BKqIzdI4uUYiu0R16QE3UQgQl6BN9ed/eby6//Jmct/qiKtqIXOEP2Mu1Sg==</latexit>
sha1_base64="+ils4kwJ7Kdc+6AiEYqnwZyXGFk=">AAACvHicbVFdb9MwFHUCGyMM6PbKi8UK6iSonDKJvUwgIU3wMBjS2k2qS+U4bmvVsTPb2RKs/E0k/gsPOF0kto4rWTo+515/nJPkghuL0O8gfPBwY/PR1uPoyfbTZ887O9sjowpN2ZAqofRFQgwTXLKh5Vawi1wzkiWCnSfLT41+fsW04Uqe2Spnk4zMJZ9xSqynpp28O+qVb2C1D48gNpfaul75ttr/cQZP4ArV3eia20XUPTmKcMLmXLokI1bzso5g3EeDwQF8DVEfocMDjKMWecpr6F0MI8xk+m+kO+3sNS1NwfsgbsEeaOt0uhN8wKmiRcakpYIYM45RbieOaMupYHWEC8NyQpdkzsYeSpIxM3Era2r4yjMpnCntl7Rwxd6ecCQzpsoS3+mfuDDrWkP+TxsXdnY4cVzmhWWS3lw0KwS0CjY+w5RrRq2oPCBUc/9WSBdEE2p9GhFuDmxzcYkS6Z1vOMo1LfzM8qfnJbumKsuItxF/+1o7hy0rfdTOb+p1/fj4doPf+Q5vebxu8H0wGvRj1I+/I7AFXoCXoAdi8B58BJ/BKRgCCn6BP8FGsBl+CVV4dRNOGLQp7YI7FZZ/AWu31Wk=</latexit>
sha1_base64="KooJ+21LneRo9UJlY0kAWRWNPDU=">AAACx3icbVFdb9MwFHUCGyN8rINHXixaUCdB5ZRJ7GViAmmCh8GQ1m5SXSrHcVurjh1sZ0ux8sCfROK/8IDTRWLruJKl43PO9ce5SS64sQj9DsI7dzc2723djx48fPR4u7XzZGhUoSkbUCWUPk+IYYJLNrDcCnaea0ayRLCzZPGh1s8umDZcyVO7zNk4IzPJp5wS66lJK+8Mu+UruNyFBxCb79q6bvl6ufvtFB7DFao60SW386hzfBDhhM24dElGrOZlFcG4h/r9PfgSoh5C+3sYRw3ylNfQmxhGmMn0X0tn0mrXlrrgbRA3oA2aOpnsBO9wqmiRMWmpIMaMYpTbsSPacipYFeHCsJzQBZmxkYeSZMyM3SqaCr7wTAqnSvslLVyx1zscyYxZZol3+ifOzbpWk//TRoWd7o8dl3lhmaRXF00LAa2Cdc4w5ZpRK5YeEKq5fyukc6IJtX4aEa4PbObiEiXSG99wlGta+J7FD89LdklVlhEfI/7yuXIOW1b6UTu/qdb1o6PrBr/zDh95vB7wbTDs92LUi7+i9uH7Jvwt8Aw8B10Qg7fgEHwEJ2AAKPgF/gQbwWb4KVThRVheWcOg6XkKblT48y+yb9aY</latexit>p(xy)T M (x

1.0224 0.0084y) with M =0.0084 1.0031

with parameters ↵(s) = s, ↵(s) = 1.0127s and  = 0.014.
<latexit sha1_base64="/6+ObFXTi2Z4vRhvfOwGPr8IQ6Y=">AAACuXicbVFda9swFFW8ry77SrvHvYglgw5GsMOggzFaVih72jpY2kIcwrWs1GpkSUhyu0z4/+0v9E/sdXvcdeqHNu0FwdE5515JR5mRwvk4vuxE9+4/ePho43H3ydNnz1/0NreOnK4s42OmpbYnGTguheJjL7zkJ8ZyKDPJj7PFfqMfn3PrhFY//NLwaQmnSswFA4/UrJddCF9QAxZK7tHXpYO0Ujm3zcCQgjQF1NvuLf1E3Tua6vO7lGQYJ6MdN6CgcuxfgDGAdIz0+8Fw1usjWhW9DZIW9Elbh7PNzm6aa1aVXHkmwblJEhs/DWC9YJLX3bRy3ABbwCmfIFR4dzcNqzBq+gaZnM61xaU8XbHXOwKUzi3LDJ0l+MKtaw15lzap/PzDNAhlKs8VuzpoXknqNW2SpbmwnHm5RADMCrwrZQUGy1a5ps3A9idCpmV+4xmBCcsq7Fn8Ql7xC6bLEtMM6bevdQip5z/xcwNu6nX94OC6AXfowMiT9YBvg6PRMImHyfdRf+9zG/4GeUVek22SkB2yR76QQzImjPwmf8hf8i/6GEFURGdX1qjT9rwkNypy/wHoX9i3</latexit>⌧
switchinginterval
⌧
=
0.5
and
the
maximumdelay=
Now with01000
we use our main theorem to derive the error bound "1 = 0.0294176<latexit sha1_base64="SN5FjIm4ZFEe4tl/MVjKmEpjIpc=">AAACr3icbZHNbhMxFIWd4a+EvxSWbCwSJFaRp1IFG0QFUsUKikSaSEkIdzw3iRXbM7I9bYM1r8Z7sGcLz8BNOos25UqjOT73XI/9TVZq5YMQv1rJrdt37t7bu99+8PDR4yed/aenvqicxIEsdOFGGXjUyuIgqKBxVDoEk2kcZqsPm/7wDJ1Xhf0a1iVODSysmisJgaxZZ+TPVZBLZRdc2YDuDDTvTQJU/C0X/cMeb3OwOQ9L5AYulKkMz1HDmkL0DjCLoqboZO5Axs1cHVMhRN2bdbqiL7bFb4q0EV3W1Mlsv/VukheyMmiD1OD9OBVlmEZwQUmNdXtSeSxBrmCBY5IWDPpp3CKo+Utycj4vHD028K17dSKC8X5tMkoaCEu/29uY/+uNqzB/M43KllVAKy8/NK80DwXf8OS5ciiDXpMA6RSdlcslEA2CSTttNmz4x6zQ+bVrRKmcrGhm9YN8i+eyMIZwx8nnT3UknHhBvzTSot7tHx9fDdCKEoQ83QV8U5we9FPRT78cdI/eN/D32HP2gr1iKXvNjthHdsIGTLKf7Df7w/4maTJMviXfL6NJq5l5xq5Vov4BIvTWWw==</latexit><latexit sha1_base64="semIRilsKDcDEdhHYdwykPu1c2o=">AAACdHicbVHLThsxFHWG0kJaaKDLtpLVgMQqmomqAgsEohLqqqVSA0iZKPJ4bsCKHyPbA6TWrPiabsvX8COsexNmAaFXsnQe9/pxnBVSOB/Hd41o4cXiy1dLy83Xb1ZW37bW1k+cKS2HHjfS2LOMOZBCQ88LL+GssMBUJuE0G3+d+qeXYJ0w+pefFDBQ7FyLkeDMozRsfdxIL5mFwgmJNCQV3aNxJ+7ufk62v2wMW20ks6LPQVKDNqnreLjW2E9zw0sF2nPJnOsnceEHgVkvuISqmZYOCsbH7Bz6CDVT4AZh9o6KbqKS05GxuLSnM/XxRGDKuYnKsFMxf+Hmvan4P69f+tHOIAhdlB40fzhoVErqDZ2GQnNhgXs5QcC4FXhXyi+YZdxjdM10umEdYsiMzJ88I3BheYkz49+oa7jiRimm85D++F6FkHq4xn8JSKp5/+jocQMy7MDIk/mAn4OTbieJO8nPbvvgsA5/ibwnn8gWScg2OSDfyDHpEU5uyB/yl9w27qMPUTvafGiNGvXMO/Kkos4/FkzABA==</latexit>

Hasuo (NII, JP) 16

Two-Step Control Synthesis
for Periodically Switched Systems with Delays
Actual system T (⌃⌧, 0 )A continuous-space switched system with nearly periodic switching, with delays within 0 > 0⇠ "1

approximately bisimilar(this work)

Delay-free abstraction T (⌃⌧ )A continuous-space switchedsystem with periodic switching
signals, with no switching delays⇠ "2

A switching signal
for ⌃⌧, 0 with precision "1 + "2<latexit sha1_base64="semIRilsKDcDEdhHYdwykPu1c2o=">AAACdHicbVHLThsxFHWG0kJaaKDLtpLVgMQqmomqAgsEohLqqqVSA0iZKPJ4bsCKHyPbA6TWrPiabsvX8COsexNmAaFXsnQe9/pxnBVSOB/Hd41o4cXiy1dLy83Xb1ZW37bW1k+cKS2HHjfS2LOMOZBCQ88LL+GssMBUJuE0G3+d+qeXYJ0w+pefFDBQ7FyLkeDMozRsfdxIL5mFwgmJNCQV3aNxJ+7ufk62v2wMW20ks6LPQVKDNqnreLjW2E9zw0sF2nPJnOsnceEHgVkvuISqmZYOCsbH7Bz6CDVT4AZh9o6KbqKS05GxuLSnM/XxRGDKuYnKsFMxf+Hmvan4P69f+tHOIAhdlB40fzhoVErqDZ2GQnNhgXs5QcC4FXhXyi+YZdxjdM10umEdYsiMzJ88I3BheYkz49+oa7jiRimm85D++F6FkHq4xn8JSKp5/+jocQMy7MDIk/mAn4OTbieJO8nPbvvgsA5/ibwnn8gWScg2OSDfyDHpEU5uyB/yl9w27qMPUTvafGiNGvXMO/Kkos4/FkzABA==</latexit>

A switching signal
for ⌃⌧ with precision "2approximately bisimilar

Symbolic abstraction T⌧symb
A discrete-space transition system built as an abstraction of ⌃⌧One Lyapunov,
Two-Step
Controlays
Even bisim
bette
two approx.
-GUAS enables
In the boost DCwhere we combin
etDCal.ex:(2010). Se"1 = 0.0294176
derivethe first
ε2 : trade-off
systemT (⌃⌧, 0 )with(thegrid sizeandtransiti
freeabstraction
Another example
periodic switchedin the arxiv ver.
space discretizat(nonlinear water
thus
construct atank) the secon
tablishThe fact that ou
assumptions use
ing: for establish⇠"Lyapunovand ⇠"2 , we1function
GUAS
Lyapunov
Hasuo (NII, JP) 17

discretesynthesis / A switching signal
for T⌧symb

Fig. 1. A two-step control synthesis workflow for switchedsystems with delays. We separate two concerns: time

PPROXIMATELY BISIMILAR SYMBOLIC MODELS FOR INCREMENTALLY STABLE SWITCHED SYSTEMS 13

st DC-DC converter using the procedure described in Section 4.1. According to Theorem 4.1, a
red precision " can be achieved by choosing a state space discretization parameter ⌘ satisfying"/145. In this example, the ratio between the precision of the symbolic approximation and thee space discretization parameter is quite large. This is explained by the fact that the subsystems
quite weakly stable since the value of  is small.

Two-Step Control Synthesis

for Periodically Switched Systems with Delays

One Lyapunov,
Two-Step
ControActual system T (⌃⌧, 0 )laysEven bisim
bette
two approx.
A switching signal
A continuous-space switched sysfor ⌃⌧, 0 with preci-GUAS enables
tem with nearly periodic switchIn the boost DCsion "1 + "2
where we combin
ing, with delays within 0 > 0
etDCal.ex:(2010). Se"1 = 0.0294176⇠"1 approximately bisimilar
derivethefirst(this work)
ε2 : trade-off
systemT (⌃⌧, 0 )Delay-free abstraction T (⌃⌧ )with(thegrid sizeandtransiti
A switching signal
A continuous-space switchedfor ⌃⌧ with precifree
abstraction
system with periodic switching
Another example
sion [GirardPT’10]"2
periodic
switched
1p
signals,withnoswitchingdelaysFigure 3. Symbolic model of the boost DC-DC converter for ⌘ = 40 2 (left); Conin the arxiv ver.
space discretizat
troller for the symbolic model (right) (dark gray: mode 1, light gray: mode 2, medium(nonlinear water"2
gray:⇠bothmodes
are acceptable,
white: uncontrollable states).
approximately
bisimilar
thus
construct atank) the secon
tablishdiscreteconsider two di↵erent values of the precision". We first choose a precision " = 2.6
symb parameter
Symbolic abstraction T
ch can be achieved by choosing ⌘ = 401p2⌧. This precision
is quite poorand makes thecomputed The fact that ou
synthesisAswitchingsignal/A discrete-spacetransition
bolic modelof no practical use.
However, itsyshelps to understand theexperiment decribed assumptions use
forsecondT⌧symbtem
built
as symbolic
an abstractionof boost⌃⌧ DC-DC converter is shown on the left, red andher. On
Figure3, themodel of thearrows represent the transitions associated with mode 1 and 2, respectively. We only represented ing: for establish
transitions that keep the state of the symbolic model in the set I 0 = [1.3, 1.7] ⇥ [5.7, 5.8]. Using ⇠"Lyapunovand ⇠"2 , we1functionervisory
we synthesized
thesynthesis
most permissive
controller thatkeeps
the state ofFig.control
1. A [RW87],
two-step
control
workflowforswitched
GUAS
Lyapunov
symbolic model inside I 0 . It is shown on the right figure, the color of the boxes centered aroundHasuo (NII, JP) 17
systems with delays. We separate two concerns: time<latexit sha1_base64="semIRilsKDcDEdhHYdwykPu1c2o=">AAACdHicbVHLThsxFHWG0kJaaKDLtpLVgMQqmomqAgsEohLqqqVSA0iZKPJ4bsCKHyPbA6TWrPiabsvX8COsexNmAaFXsnQe9/pxnBVSOB/Hd41o4cXiy1dLy83Xb1ZW37bW1k+cKS2HHjfS2LOMOZBCQ88LL+GssMBUJuE0G3+d+qeXYJ0w+pefFDBQ7FyLkeDMozRsfdxIL5mFwgmJNCQV3aNxJ+7ufk62v2wMW20ks6LPQVKDNqnreLjW2E9zw0sF2nPJnOsnceEHgVkvuISqmZYOCsbH7Bz6CDVT4AZh9o6KbqKS05GxuLSnM/XxRGDKuYnKsFMxf+Hmvan4P69f+tHOIAhdlB40fzhoVErqDZ2GQnNhgXs5QcC4FXhXyi+YZdxjdM10umEdYsiMzJ88I3BheYkz49+oa7jiRimm85D++F6FkHq4xn8JSKp5/+jocQMy7MDIk/mAn4OTbieJO8nPbvvgsA5/ibwnn8gWScg2OSDfyDHpEU5uyB/yl9w27qMPUTvafGiNGvXMO/Kkos4/FkzABA==</latexit>Related Work
Approximate bisimulation for state-space discretization. Synthesis, switched systems, …
Overview: Girard, A. and Pappas, G.J. (2011). Approximate bisimulation: A bridge between computer scienceand control theory. Eur. J. Control , 17(5-6), 568-578.

Delays as adversarial disturbance ➜ alternating approximate bisimulation
Pola, G., Pepe, P., and Benedetto, M.D.D. Alternating approximately bisimilar symbolic models for nonlinear
control systems with unknown time-varying delays. CDC 2010

Synthesis by solving games“Delay-tolerating” specification
Liu, J. and Ozay, N. Finite abstractions with robustness margins for temporal logic-based control synthesis.
HSCC 2016

Discrete delays τ, 2τ, 3τ, … by zero-order hold ➜ discrete games
Zamani, M., Jr, M.M., Khaled, M., and Abate, A. (2017). Symbolic abstractions of networked control systems.
IEEE Transactions on Control of Network Systems(τ,ε)-closeness, Skorokhod distance
Abbas, H. and Fainekos, G.E. (2015). Towards composition of conformant systems. CoRR , abs/1511.05273.

Hasuo (NII, JP) 18

Conclusions
The approximate bisimulation workflow
Our use: delays in switched systems
Simper setting ➜ applicability
Technical contributions. Key: states and distanceTwo-step synthesis, via state-space discretization

Hasuo (NII, JP) 19

Conclusions
The approximate bisimulation workflow
Our use: delays in switched systems
Simper setting ➜ applicability
Technical contributions. Key: states and distanceTwo-step synthesis, via state-space discretization
We’re hiring!
Max 3.5 yrs, PD & senior researchers
logic + automata + categories + machinelearning + software engineering➜ CPS, automated driving

Thank yo u for yo ur atten
tion!
Ichiro Hasuo (NII, Tokyo)

http://group-mmm.org/~ichiro/ JP) 19
Hasuo (NII,