Static analysis of SPDIs for state-space reduction

Department of Informatis

Stati Analysis of

SPDIs for State-Spae

Redution

Researh Report No.

336

Gordon Pae

Gerardo Shneider

Isbn 82-7368-291-9

Issn 0806-3036

April 2006

Redution

Gordon Pae

∗

Gerardo Shneider

†

April 2006

Abstrat

Polygonal hybrid systems (SPDI) are a sublass of planar hybrid

automata whih an be represented by pieewiseonstant dierential

inlusions. Thereahabilityproblemaswellastheomputationofer-

tainobjets ofthephaseportrait, namelytheviability,ontrollability

and invariane kernels, for suh systems is deidable. In this paper

we show how to ompute another objet of an SPDI phase portrait,

namely semi-separatrix urves and show how the phase portrait an

be used for reduing the state-spae for optimizing the reahability

analysis.

1 Introdution

Hybrid systems ombining disreteand ontinuous dynamisarise asmath-

ematialmodels ofvariousartiialand naturalsystems,and asapproxima-

tions to omplex ontinuous systems. They have been used in various do-

mains, inludingavionis, robotis andbioinformatis. Reahabilityanalysis

has beentheprinipalresearhquestionintheveriationofhybridsystems,

even ifitisawell-known resultthatformost non-trivialsublassesofhybrid

systems reahability and most veriation questions are undeidable. Vari-

ous deidable sublasses have, subsequently, been identied, inludingtimed

[AD94 ℄ and retangular automata [HKPV95℄, hybrid automata with linear

∗

Dept. of Computer Siene and AI, University of Malta, Msida, Malta. E-mail:

gordon.paeum.edu.mt

†

Dept. ofInformatisUniv. ofOslo, P.O. Box1080Blindern, N-0316Oslo,Norway.

E-mail: gerardoi.uio.no

and polygonaldierentialinlusionsystems (SPDIs)[ASY01℄.

Compared to reahability veriation, qualitative analysis of hybrid sys-

tems is a relatively negleted area [ALQ

+

01b, DV95, KdB01, MS00, SP02,

SJSL00℄. Typial qualitative questions inlude: Are there `sink' regions

where a trajetory an never leave one it enters the region?; Whih are

the basins of attration of suh regions?; Are there regions in whih every

pointinthe regionis reahable fromevery other pointinthe region without

leaving it?. To answer suh questions one usually gives a olletion of ob-

jets haraterizingthese sets, hene providinguseful informationabout the

qualitative behavior of the hybrid system. The set of all suh objets for a

given system is alled the phase portrait of the system.

Deningandonstrutingphaseportraitsofhybridsystemshasbeendiretly

addressed for PCDs in [MS00℄, and for SPDIs in[ASY02℄. In this paper we

present a a new element of the phase portrait for SPDIs, and disuss how

the phase portrait an be used to redue the size of an SPDI, as an aid to

veriation.

Roughly speaking, anSPDI (Fig. 1)isa nitepartition

P

^{of the plane (into}

onvexpolygonalareas),and,foreah

P ∈ P

^{anassoiatedpair ofvetors}

a P

and

b _P

^{. TheSPDI behaviourisdened by thedierentialinlusion}

x ˙ ∈ ∠ ^{b a} P ^P

for

x ∈ P

^{, where}

∠ ^{b a}

^{denotes the angle on the plane between the vetors}

a

and

b

^.

In [ASY01℄ it has been proved that edge-to-edge and polygon-to-polygon

reahabilityinSPDIs isdeidable by exploitingthe topologialproperties of

the plane. The proedure is not based on the omputation of the reah-set

but rather on the exploration of a nite number of types of qualitative be-

haviors obtained from the edge-signatures of trajetories (the sequenes of

their intersetions with the edges of the polygons). Suh types of signatures

may ontain loops whih an be very expensive (or impossible) to explore

naively. However, it has been shown that loops have strutural properties

that are exploited by the algorithmto eiently ompute the eet of suh

loops. In summary,the novelty oftheapproahisthe ombinationofseveral

tehniques, namely,(i)therepresentation ofthe two-dimensionalontinuous

dynamisasaone-dimensionaldisretedynamialsystem,(ii)the harater-

ization ofthe set of qualitativebehaviorsofthe latter asanite set of types

ofsignatures, and(iii)theaeleration oftheiterationsinthease ofyli

signatures.

Givenayle onaSPDI,wean speakaboutanumberof kernels pertaining

tothatyle. Theviability kernelisthelargestsetofpointsintheylewhih

mayloopforeverwithintheyle. Theontrollability kernelisthelargestset

R1 R2 R3

R6 R5 R4

e1 e4

e0

I

e2 e6

I’

e5 e3

Figure 1: An SPDI and itstrajetory segment.

bereahedfromanyother). Aninvariantset isaset ofpointssuhthateah

pointmustkeep rotatingwithintheset forever. Theinvariane kernel isthe

largest of suh sets. The information gathered for omputing reahability

turns out to be useful for omputing viability,ontrollability and invariane

kernels of suh systems. Algorithms for omputing these kernels have been

presented in[ASY02,Sh04 ℄andimplementedinthetoolsetSPeeDI

+

[PS06℄.

The ontributionof this paperisthreefold. We start by givinganalgorithm

to ompute semi-separatrix urves (or simply, semi-separatries) of SPDIs.

Separatriesareonvexpolygonsdissetingtheplaneintotwomutuallynon-

reahable subsets. The notion of separatrix an be relaxed, obtainingsemi-

separatrixurves,suhthatsomepointsinonesetmaybereahablefromthe

other set, but not vie-versa. We then show how the kernels an be used to

answer reahability questions diretly. We also show how semi-separatries

anbeused tooptimizethereahabilityalgorithmforSPDIsby reduingthe

numberofstatesoftheSPDIgraph. Theoptimizationisbasedontopologial

properties of the plane (and inpartiular, that of SPDIs).

The paper is strutured as follows. In the next setion we introdue the

neessary theoretial bakground, inluding the denition of SPDI, kernels

and semi-separatriesaswellashowtoomputesuhphaseportraitobjets.

In Setion 3 we show how the semi-separatries an be used for reduing

the state-spaeof the reahabilitygraphwhereas inSetion4wepresent the

optimization done by using the kernels.

A(positive)ane funtion

f : R → R

^issuhthat

f(x) = ax + b

^with

a > 0

^.

An ane multivalued funtion

F : R → 2 ^R

^{, denoted}

F = hf l , f u i

^{, is dened}

by

F (x) = hf l (x), f u (x)i

^where

f l

^and

f u

^areaneand

h·, ·i

^{denotesaninter-}

val. For notational onveniene, we do not make expliit whether intervals

are open, losed,left-open orright-open, unless requiredfor omprehension.

Foran interval

I = hl, ui

^{we have that}

F (hl, ui) = hf l (l), f u (u)i

^{. The inverse}

of

F

^{is dened by}

F ⁻¹ (x) = {y | x ∈ F (y)}

^{. The universal inverse of}

F

^is

dened by

F ˜ ⁻¹ (I) = I ^′

^{if and only if}

I ^′

^{is the greatest non-empty interval}

suh that for all

x ∈ I ^′

^,

F (x) ⊆ I

^.

It is not diult to show that

F ⁻¹ = hf _u ⁻¹ , f _l ⁻¹ i

^{and similarly that}

F ˜ ⁻¹ = hf _l ⁻¹ , f _u ⁻¹ i

^{, provided that}

hf _l ⁻¹ , f _u ⁻¹ i 6= ∅

^{. Notie thatif}

I

^{is asingletonthen}

F ˜ ⁻¹

^{is dened only if}

f l = f u

^{. These lasses of funtions are losed under}

omposition.

A trunated ane multivalued funtion (TAMF)

F : R → 2 ^R

^{is dened}

by an ane multivalued funtion

F

^{and intervals}

S ⊆ R ⁺

^and

J ⊆ R ⁺

^as

follows:

F (x) = F (x) ∩ J

^if

x ∈ S

^{, otherwise}

F (x) = ∅

^{. For onveniene}

we write

F (x) = F ({x} ∩ S) ∩ J

^{. For an interval}

I

^,

F (I) = F (I ∩ S) ∩ J

and

F ⁻¹ (I) = F ⁻¹ (I ∩ J ) ∩ S

^{. The universal inverse of}

F

^{is dened by}

F ˜ ⁻¹ (I) = I ^′

^{if and onlyif}

I ^′

^{is the greatest non-empty intervalsuhthat for}

all

x ∈ I ^′

^,

F (x) ⊆ I

^and

F (x) = F (x)

^.

We say that

F

^{is normalized if}

S = DomF = {x | F (x) ∩ J 6= ∅}

^(thus,

S ⊆ F ⁻¹ (J)

^)and

J = ImF = F(S)

^.

The following theorem states that TAMFs are losed under omposition

[ASY01℄.

Theorem 1. The omposition of two TAMFs

F 1 (I) = F 1 (I ∩ S 1 ) ∩ J 1

^and

F 2 (I) = F 2 (I ∩ S 2 ) ∩ J 2

^{, is the TAMF}

(F 2 ◦ F 1 )(I) = F (I) = F (I ∩ S) ∩ J

^,

where

F = F 2 ◦ F 1

^,

S = S 1 ∩ F 1 ⁻¹ (J 1 ∩ S 2 )

^and

J = J 2 ∩ F 2 (J 1 ∩ S 2 )

^.

2.1 SPDI

An angle

∠ ^{b a}

^{onthe plane, dened by two non-zero vetors}

a, b

^{isthe set of}

allpositivelinearombinations

x = α a + β b

^,with

α, β ≥ 0

^,and

α + β > 0

^.

We an always assume that

b

^{is situated in the} ounter-lokwise diretion from

a

^.

A polygonal hybrid system 1

(SPDI) is dened by giving a nite partition

P

of the plane into onvex polygonal sets, and assoiating with eah

P ∈ P

^a

1

In theliterature thenamespolygonal dierential inlusion andsimple planar dier-

ouple of vetors

a P

^and

b P

^{. Let}

φ(P ) = ∠ ^{b a} P ^P

^{. The SPDI is determined by}

˙

x ∈ φ(P )

^for

x ∈ P

^.

Let

E(P )

^{be the set of edges of}

P

^{. We say that}

e

^{is an entry of}

P

^{if for}

all

x ∈ e

^{and for all}

c ∈ φ(P )

^,

x + cǫ ∈ P

^{for some}

ǫ > 0

^{. We say that}

e

is an exit of

P

^{if the same ondition holds for some}

ǫ < 0

^{. We denote by}

in

(P ) ⊆ E(P )

^{the set ofallentries of}

P

^{andby out}

(P ) ⊆ E(P )

^{the set of all}

exits of

P

^.

Assumption 1. All the edges in

E(P )

^{are either entries or exits, that is,}

E(P ) =

ⁱⁿ

(P ) ∪

^out

(P )

^.

A trajetory segment of an SPDI is a ontinuous funtion

ξ : [0, T ] → R ²

whihis smootheverywhere exept inadisrete set ofpoints,and suh that

for all

t ∈ [0, T ]

^{, if}

ξ(t) ∈ P

^and

ξ(t) ˙

^{is dened then}

ξ(t) ˙ ∈ φ(P )

^{. The}

signature, denoted

Sig(ξ)

^{, is the ordered sequene of edges traversed by the}

trajetory segment, that is,

e 1 , e 2 , . . .

^{, where}

ξ(t i ) ∈ e i

^and

t i < t i +1

^{. If}

T = ∞

^{,a trajetory segment isalled a trajetory.}

Example 1. Consider the SPDI illustrated inFig. 1. For sake of simpliity

wewillonlyshowthe dynamisassoiatedtoregions

R 1

^to

R 6

^{inthe piture.}

For eah region

R i

^,

1 ≤ i ≤ 6

^{, there is a pair of vetors}

(a i , b i )

^{, where:}

a 1 = (45, 100), b 1 = (1, 4)

^,

a 2 = b 2 = (1, 10)

^,

a 3 = b 3 = (−2, 3)

^,

a 4 = b 4 = (−2, −3)

^,

a 5 = b 5 = (1, −15)

^,

a 6 = (1, −2), b 6 = (1, −1)

^.

A trajetory segment starting on interval

I ⊂ e 0

^{and nishing in interval}

I ^′ ⊆ e 4

^isdepited.

Denition1. We saythatasignature

σ

^{isfeasible ifandonlyifthere exists}

a trajetory segment

ξ

^{with signature}

σ

^{, i.e.,}

Sig(ξ) = σ

^.

From this denition, it immediately follows that extending an unfeasible

signature, an nevermake it feasible:

Proposition1. Ifa signature

σ

^{isnotfeasible,thenneitherisany extension}

of the signature for any signatures

σ ^′

^and

σ ^′′

^{, the signature}

σ ^′ σσ ^′′

^{is not}

feasible.

Given anSPDI

S

^{, let}

E

^{bethe set of edgesof}

S

^{, then wean dene agraph}

G S

^{where nodes orrespond to edges of}

S

^{and suh that there exists an ar}

from one node toanother if there exists a trajetory segment from the rst

edge to the seond one withouttraversing any other edge. More formally:

Denition 2. Given an SPDI

S

^{, the underlying graphof}

S

^{(or simply the}

graph of

S

^{), is a graph}

G S = (N G , A G )

^{, with}

N G = E

^and

A G = {(e, e ^′ ) |

∃ξ, t . ξ(0) ∈ e ∧ ξ(t) ∈ e ^′ ∧ Sig (ξ) = ee ^′ }

^{. We say that a sequene}

e 0 e 1 . . . e k

of nodes in

G S

^{is a path whenever}

(e i , e i +1 ) ∈ A G

^for

0 ≤ i ≤ k − 1

^.

and paths in itsorresponding graph.

Lemma 2. If

ξ

^{is a trajetory segment of}

S

^{with edge signature}

Sig (ξ) = σ = e 0 . . . e p

^{, it follows that}

σ

^{is a path in}

G S

^.

Remark. Notiethattheonverseoftheabovelemmaisnottrueingeneral.

It is possible tond a ounter-example wherethere exists apath from node

e

^to

e ^′

^{, but it does not exist a trajetory segment form edge}

e

^{to edge}

e ^′

^on

the SPDI.

Lemma 3. If

σ = e 0 . . . e p

^{isafeasible signature,then}

σ

^{isa pathin}

G S

^.

2.2 Suessors and predeessors

Given an SPDI, we x a one-dimensional oordinate system on eah edge

torepresent pointslayingonedges [ASY01℄. Fornotationalonveniene, we

indistintlyuseletter

e

^{todenotethe edgeorits}one-dimensionalrepresenta- tion. Aordingly, we write

x ∈ e

^or

x ∈ e

^{, tomean point}

x

^{in edge}

e

^with

oordinate

x

^inthe one-dimensional oordinatesystem of

e

^{. The same on-}

ventionisappliedtosetsof pointsof

e

represented asintervals(e.g.,

x ∈ I

^or

x ∈ I

^,where

I ⊆ e

^{) and to} trajetories (e.g.,

ξ

^{starting in}

x

^or

ξ

^starting

in

x

^).

Now, let

P ∈ P

^,

e ∈

ⁱⁿ

(P )

^and

e ^′ ∈

^out

(P )

^{. For}

I ⊆ e

^,

Succ _e,e ′ (I)

^{is the}

set of allpointsin

e ^′

^{reahablefromsome pointin}

I

^{by atrajetorysegment}

ξ : [0, t] → R ²

ⁱⁿ

P

^(i.e.,

ξ(0) ∈ I ∧ ξ(t) ∈ e ^′ ∧ Sig (ξ) = ee ^′

^{). It has been}

shown [ASY01℄ that

Succ _e,e ′

^{is a TAMF.}

Example 2. Let

e 1 , . . . , e 6

^{be as in Fig. 1 and}

I = [l, u]

^{. We assume a}

one-dimensional oordinate system. We have:

F e 1 e 2 (I) = l

4 , 9 20 u

, S = [0, 10] , J =

0, 9 2

F e 2 e 3 (I) = [l + 1, u + 1] , S = [0, 9] , J = [1, 10]

F e 3 e 4 (I) = 3

2 l, 3 2 u

, S =

0, 20 3

, J = [0, 10]

F e 4 e 5 (I) = 2

3 l, 2 3 u

, S = [0, 10] , J =

0, 20 3

F e 5 e 6 (I) =

l − 2

3 , u − 2 3

, S = 2

3 , 10

, J =

0, 28 3

F e 6 e 1 (I) = [l, 2u] , S = [0, 10] , J = [0, 10]

with

Succ _e i e i +1 (I) = F e i e i +1 (I ∩ S i ) ∩ J i+1

^{, for}

1 ≤ i ≤ 5

^{, and}

Succ _{e 6 e 1} (I) = F e 6 e 1 (I ∩ S 6 ) ∩ J 1

^.

Given asequene

w = e 1 , e 2 , . . . , e n

^{, Theorem 1impliesthat the suessor of}

I

^along

w

^{dened as}

Succ _w (I ) = Succ _e n − 1 ,e ⁿ ◦ . . . ◦ Succ _{e 1 ,e 2} (I)

^{is aTAMF.}

Example 3. Let

σ = e 1 · · · e 6 e 1

^{. It results that}

Succ _σ (I) = F (I ∩ S) ∩ J

^,

where:

F (I) = l

4 + 1 3 , 9

10 u + 2 3

(1)

S = [ ³⁷ ₂₅ e ⁻¹⁶ , 10]

^and

J = [ ¹ ₃ , ²⁹ ₃ ]

^{are omputed usingTheorem 1.}

For

I ⊆ e ^′

^,

Pre _e,e ′ (I)

^{is the set of points in}

e

^{that an reah a point in}

I

^{by a trajetory segment in}

P

^{. The}

∀

-predeessor

Pre f (I )

^{is dened in a}

similar way to

Pre(I)

^{using the universal inverse instead of justthe inverse:}

For

I ⊆ e ^′

^,

Pre f _ee ′ (I)

^{is the set of points in}

e

^{suh that any suessor of}

suh points are in

I

^{by a trajetory segment in}

P

^{. Both denitions an be}

extended straightforwardly to signatures

σ = e 1 · · · e n

^:

Pre _σ (I)

^and

Pre f _σ (I)

^.

Therefore, the suessor operator has two inverse operators.

Example 4. Let

σ = e 1 . . . e 6 e 1

^{be as in Fig. 1 and}

I = [l, u]

^{. Now,}

Pre _e i e i+1 (I) = F _e ⁻¹ _{i e i+1} (I ∩ J i +1 ) ∩ S i

^,for

1 ≤ i ≤ 5

^,and

Pre _{e 6 e 1} (I) = F _e ⁻¹ _{6 e 1} (I ∩ J 1 ) ∩ S 6

^,where:

F _e ⁻¹ _{1 e 2} (I) = 20

9 l, 4u

F _e ⁻¹ _{2 e 3} (I) = [l − 1, u − 1]

F _e ⁻¹ _{3 e 4} (I) = 2

3 l, 2 3 u

F _e ⁻¹ _{4 e 5} (I) = 3

2 l, 3 2 u

F _e ⁻¹ _{5 e 6} (I) =

l + 2

3 , u + 2 3

F _e ⁻¹ _{6 e 1} (I) = l

2 , u

Besides,

Pre _σ (I) = F ⁻¹ (I ∩ J) ∩ S

^{, where}

F ⁻¹ (I) = [ ¹⁰ ₉ l − ²⁰ ₂₇ , 4u − ⁴ ₃ ]

^.

Similarly,weompute

Pre f _σ (I) = ˜ F ⁻¹ (I ∩J )∩S

^,where

F ˜ ⁻¹ (I) =

4l − ⁴ ₃ , ¹⁰ ₉ u − ²⁰ ₂₇

.

2.3 Qualitative analysis of simple edge-yles

Let

σ = e 1 · · · e k e 1

^{be a simple edge-yle, i.e.,}

e i 6= e j

^{for all}

1 ≤ i 6=

j ≤ k

^{. Let}

Succ _σ (I) = F (I ∩ S) ∩ J

^with

F = hf l , f u i

^{(we suppose that}

this representation is normalized). We denote by

D σ

^the one-dimensional disrete-time dynamialsystem dened by

Succ _σ

^{, that is}

x n +1 ∈ Succ _σ (x n )

^.

Assumption 2. None of the two funtions

f l , f u

^{is the identity.}

Let

l ^∗

^and

u ^∗

^{bethe xpoints2 of}

f l

^and

f u

^, respetively,and

S ∩ J = hL, Ui

^.

A simple yle is of one of the following types [ASY01℄:

STAY. Theyleisnotabandonedneitherbytheleftmostnortherightmost

trajetory,that is,

L ≤ l ^∗ ≤ u ^∗ ≤ U

^.

DIE. Therightmosttrajetoryexitstheylethroughtheleft(onsequently

the leftmost one also exits) or the leftmost trajetory exits the yle

through the right (onsequently the rightmost one alsoexits), that is,

u ^∗ < L ∨ l ^∗ > U

^.

EXIT-BOTH. Theleftmost trajetoryexitsthe yle through the leftand

the rightmost one through the right,that is,

l ^∗ < L ∧ u ^∗ > U

^.

EXIT-LEFT. Theleftmosttrajetoryexitstheyle (throughtheleft)but

the rightmost one stays inside, that is,

l ^∗ < L ≤ u ^∗ ≤ U

^.

EXIT-RIGHT. Therightmosttrajetoryexitstheyle(throughtheright)

but the leftmostone stays inside, that is,

L ≤ l ^∗ ≤ U < u ^∗

^.

Example 5. Let

σ = e 1 · · · e 6 e 1

^{. We have}

S ∩ J = hL, Ui = [ ¹ ₃ , ²⁹ ₃ ]

^{. The}

xpoints of Eq. (1) are suh that

1

3 < l ^∗ = ¹¹ ₂₅ < u ^∗ = ²⁰ ₃ < ²⁹ ₃

^{. Thus,}

σ

^{is a}

STAY.

The lassiation above gives us some useful information about the quali-

tative behavior of trajetories. Any trajetory that enters a yle of type

DIE will eventually quit it after a nite number of turns. If the yle is of

type STAY, alltrajetories that happen to enter it willkeep turning inside

it forever. In allotherases, some trajetories willturn fora whileand then

exit, andothers willontinue turningforever. Thisinformationisruialfor

proving deidabilityof the reahability problem.

Example 6. Considerthe SPDIof Fig.1. Fig. 2showspart ofthe reahset

of the interval

[8, 10] ⊂ e 0

^{,answering positively tothe} reahabilityquestion:

Is

[1, 2] ⊂ e 4

^{reahable from}

[8, 10] ⊂ e 0

^{? Fig. 2 has been} automatially generated by theSPeeDitoolboxwe havedeveloped forreahabilityanalysis

of SPDIs basedon the results of [ASY01 ℄.

2

Thexpoint

x ^∗

^{isomputedbysolvingtheequation}

f (x ^∗ ) = x ^∗

^,where

f (·)

^ispositive

ane.

I’

I

Figure 2: Reahability analysis.

The above result doesnot allowusto diretlyanswerother questions about

thebehavioroftheSPDIsuhasdetermineforagivenpoint(orsetofpoints)

whether: (a) there exists (at least) one trajetory that remainsinthe yle,

and (b)itispossibletoontrolthe systemtoreahany otherpoint. Inorder

to do this, we need to further study the properties of the system around

simple edge-yles.

2.4 Kernels

We an nowpresent how toompute the invariane, ontrollabilityand via-

bility kernelsof anSPDI. Proofsare omittedbut for further details,refer to

[ASY02℄ and [Sh04 ℄. In the following, for

K

^{a subset of}

R ²

^and

σ

^{a yli}

signature, we dene

K σ

^{as follows:}

K σ = [ k i=1

(

^int

(P i ) ∪ e i )

⁽²⁾

where

P i

^{is suh that}

e i−1 ∈

ⁱⁿ

(P i )

^,

e i ∈

^out

(P i )

^{and int}

(P i )

^is

P i

^'sinterior.

2.4.1 ViabilityKernel

Wenow reall the denition of viability kernel[Aub01℄.

Denition 3. A trajetory

ξ

^{is viable in}

K

^if

ξ(t) ∈ K

^{for all}

t ≥ 0

^.

K

is a viability domain if for every

x ∈ K

^{, there exists at least one trajetory}

Figure3: (a) ViabilityKernels; (b) ControllabilityKernels

ξ

^{, with}

ξ(0) = x

^{, whih is viable in}

K

^{. The viability kernel of}

K

^{, denoted}

Viab(K )

^{, is the largest viability domainontained in}

K

^.

For

I ⊆ e 1

^wedene

Pre _σ (I)

^{tobethe setof all}

x ∈ R ²

^{forwhihthereexists}

a trajetorysegment

ξ

^startingin

x

^{,that reahes somepointin}

I

^{, suh that}

Sig(ξ)

^{is a sux of}

e 2 . . . e k e 1

^{. It is easy to see that}

Pre _σ (I)

^{is a polygonal}

subset of the plane whih an be alulated using the following proedure.

We start by dening:

Pre _e (I) = {x | ∃ξ : [0, t] → R ² , t > 0 . ξ(0) = x ∧ ξ(t) ∈ I ∧ Sig (ξ) = e}

and apply this operation

k

^times:

Pre _σ (I) = S k

i=1 Pre _e i (I i )

^with

I 1 = I

^,

I k = Pre _e k ,e 1 (I 1 )

^and

I i = Pre _e i ,e i+1 (I i +1 )

^{, for}

2 ≤ i ≤ k − 1

^.

The followingresult providesa non-iterativealgorithmiproedurefor om-

puting the viability kernel of

K σ

^{onan SPDI:}

Theorem 4. If

σ

^{is not DIE,}

Viab(K σ ) = Pre _σ (S)

^{, otherwise}

Viab(K σ ) =

∅

^.

Example 7. Fig. 3-(a) shows all the viability kernels of the SPDI given in

Example 1. There are 4 yles with viability kernels in the piture two of

the kernels are overlapping.

We say

K

^is ontrollable if for any two points

x

^and

y

ⁱⁿ

K

^{there exists a}

trajetorysegment

ξ

^startingin

x

^{thatreahes an}arbitrarilysmallneighbor- hoodof

y

^{withoutleaving}

K

^{. More formally:}

Denition 4. A set

K

^is ontrollable if

∀x, y ∈ K, ∀δ > 0, ∃ξ : [0, t] → R ² , t > 0 . (ξ(0) = x ∧ |ξ(t) − y| < δ ∧ ∀t ^′ ∈ [0, t] . ξ(t ^′ ) ∈ K )

^{. The}

ontrollabilitykernel of

K

^{, denoted}

Cntr(K)

^{, isthelargest} ontrollablesubset of

K

^.

For agiven yli signature

σ

^{, we dene}

C D (σ)

^{as follows:}

C D (σ) =

 

 

 

 

 



hL, U i

^if

σ

^{is EXIT-BOTH}

hL, u ^∗ i

^if

σ

^{is EXIT-LEFT}

hl ^∗ , Ui

^if

σ

^{is EXIT-RIGHT}

hl ^∗ , u ^∗ i

^if

σ

^{is STAY}

∅

^if

σ

^{is DIE}

(3)

For

I ⊆ e 1

^letusdene

Succ _σ (I)

^{asthesetofallpoints}

y ∈ R ²

^forwhihthere

exists a trajetory segment

ξ

^{starting in some point}

x ∈ I

^{, that reahes}

y

^,

suhthat

Sig (ξ)

^{isaprex of}

e 1 . . . e k

^{. Thesuessor}

Succ _σ (I)

^isapolygonal

subset of the plane whihan beomputed similarlyto

Pre _σ (I)

^{. Dene}

C (σ) = (Succ σ ∩ Pre _σ )(C D (σ))

Weompute the ontrollability kernel of

K σ

^asfollows:

Theorem 5.

Cntr (K σ ) = C (σ)

^.

Example 8. Fig. 3-(b) shows all the ontrollability kernels of the SPDI

given in Example 1. There are 4 yles with ontrollability kernels in the

piture two of the kernels are overlapping.

The followingresult whihrelatesontrollabilityand viabilitykernels,states

that theviabilitykernelofagivenyle istheloalbasinofattration ofthe

orresponding ontrollability kernel.

Proposition 2. Any viable trajetory in

K σ

^{onverges to}

Cntr (K σ )

^.

Let

Cntr ^l (K σ )

^{be the losed urve obtained by taking the leftmost traje-}

tory and

Cntr ^u (K σ )

^{be the losed urve obtained by taking the rightmost}

trajetorywhihanremaininsidethe ontrollabilitykernel. Inotherwords,

Cntr ^l (K σ )

^and

Cntr ^u (K σ )

^{are the two polygons dening the} ontrollability kernel.

A non-empty ontrollability kernel

Cntr (K σ )

^{of a given yli signature}

σ

partitionsthe plane intothree disjointsubsets: (1)the ontrollabilitykernel

itself,(2)thesetofpointslimitedby

Cntr ^l (K σ )

^{(andnotinluding}

Cntr ^l (K σ )

⁾

and(3)thesetofpointslimitedby

Cntr ^u (K σ )

^{(andnotinluding}

Cntr ^u (K σ )

^).

Denition 5. We dene the inner of

Cntr (K σ )

^{(denoted by}

Cntr _in (K σ )

^{) to}

be the subset dened by (2) above if the yle is ounter-lokwise or to be

the subset dened by (3) if it is lokwise. The outer of

Cntr(K σ )

^(denoted

by

Cntr _out (K σ )

^{) is dened to be the subset whih is not the inner nor the}

ontrollability itself.

Remark: Notie that an edge in the SPDI may be split into parts by the

ontrollabilitykernel part inside, part onthe kernel and part outside. In

suh ases, we an generate a dierent SPDI, with the same dynamis but

with theedge splitintoparts, suh thateahpart isompletelyinside, onor

outsidethekernel. Althoughthesignatureswillobviouslyhange,itistrivial

toprovethatthe behaviourofthe SPDIremainsidentialtotheoriginal. To

simplify presentation, inthe rest of the paper, we willassume that alledges

are either ompletely inside, on or ompletelyoutside the kernels. We note

that in pratie splittingis not neessary sine we an just onsider parts of

edges.

Proposition 3. Given two edges

e

^and

e ^′

^{, one lying ompletely inside a}

ontrollability kernel, and the other outside or on the same ontrollability

kernel, suhthat

ee ^′

^{isfeasible,thenthere existsapoint onthe}ontrollability kernel, whih is reahablefrom

e

^{and from whih}

e ^′

^{is reahable.}

Proof. Let

e ⊆ Cntr _in (K σ )

^{. Let us assume that}

e ^′ ⊆ Cntr (K σ )

^{; sine}

ee ^′

is feasible, by the Jordan urve theorem [Hen79℄, the trajetory must ross

Cntr ^l (K σ )

^or

Cntr ^u (K σ )

^{at least one. Assume the rst holds, then there}

exists

x ∈ Cntr ^l (K σ )

^{suh that}

exe ^′

^{is feasible. If}

e ^′ ⊆ Cntr _out (K σ )

^{the proof}

is onduted in a similar way as the previous ase by using the denition

of ontrollability kernel: every point inside the kernel is reahable from any

other point inthe kernel.

2.4.3 Invariane Kernel

In general,an invariant set is a set of points suh that for any point in the

set, every trajetorystartinginsuhpointremainsintheset foreverand the

invariane kernel is the largest of suh sets. In partiular, for SPDI, given

a yli signature, aninvariant set is a set of points whih keep rotating in

the yle forever and the invariane kernel is the largest of suh sets. More

Denition6. A set

K

^{issaidtobe invariantifforany}

x ∈ K

^{thereexistsat}

least one trajetory starting in it and every trajetory starting in

x

^{is viable}

in

K

^{. Given a set}

K

^{, its largest invariant subset is alled the invariane}

kernel of

K

^{and isdenoted by}

Inv (K σ )

^.

We need some preliminary denitions before showing how to ompute the

kernel. The extended

∀

-predeessor of an output edge

e

^{of a region}

R

^{is the}

set of pointsin

R

^{suh that every trajetory segment startingin suh point}

reahes

e

^{withouttraversinganyotheredge. More formally,let}

R

^bearegion

and

e

^{be anedge in out}

(R)

^{, then the}

e

^-extended

∀

-predeessor of

I

^,

Pre f _e (I)

is dened as:

Pre f _e (I) = {x | ∀ξ . (ξ(0) = x ⇒ ∃t ≥ 0 . (ξ(t) ∈ I ∧ Sig (ξ[0, t]) = e))}.

It is easy to see that

Pre f _σ (I)

^{is a polygonal subset of the plane whih an}

be alulated using the following proedure. First ompute

Pre f _e i (I)

^{for all}

1 ≤ i ≤ k

^{and then apply this operation}

k

^times:

Pre f _σ (I) = S k

i =1 Pre f _e i (I i )

with

I 1 = I

^,

I k = Pre f _{e k e 1} (I 1 )

^and

I i = Pre f _e i e i +1 (I i+1 ),

^for

2 ≤ i ≤ k − 1

^{. We}

ompute the invariane kernel of

K σ

^asfollows:

Theorem6.If

σ

^isSTAYthen

Inv(K σ ) = Pre f _σ ( Pre f _σ (J))

^,otherwise

Inv(K σ ) =

∅

^.

Example 9. Fig. 4-(a) shows the unique invariane kernels of the SPDI

given in Example 1.

An interesting property of invariane kernels is that the limitsare inluded

in the invarianekernel, i.e.

[l ^∗ , u ^∗ ] ⊆ Inv(K σ )

^{. In other words:}

Proposition 4. The set delimited by the polygons dened by the interval

[l ^∗ , u ^∗ ]

^{is an invariane set of STAY yles.}

In [ASY02℄ it has been proved that for

σ

^{a STAY yle, then (1)}

C(σ)

^is

invariant and (2) there exists a neighborhood

K

^of

C(σ)

^{suh that any vi-}

able trajetory starting in

K

^{onverges to}

C (σ)

^{. From this, the denition}

of invariane kernel and theorem 6 it follows the following result relating

ontrollabilityand invarianekernels.

Proposition 5. If

σ = e 1 . . . e n e 1

^{is STAY then}

Cntr(K σ ) ⊆ Inv(K σ )

^.

Figure 4: (a) Invariane Kernel;(b) All the Kernels

Example 10. Fig. 4-(b) shows the viability, ontrollability and invariane

kernels of the SPDIgivenin Example1. Forany pointin theviability kernel

of a yle there exists a trajetory whih will onverge to its ontrollability

kernel (proposition2). Itispossibletoseein thepiture that

Cntr (·) ⊂ Inv (.)

(proposition 5). All the above pitures has been obtained with the toolbox

SPeeDI

+

[PS06℄.

Inasimilarwayasfortheontrollabilitykernel,wedene

Inv ^l (K σ )

^,

Inv ^u (K σ )

^,

the inner

Inv _in (K σ )

^{and outer}

Inv _out (K σ )

^{of aninvarianekernel.}

2.5 Semi-Separatrix Curves

In this setionwedene the notionofseparatrix urves,whihare urves on

R ²

^{disseting the plane into two mutually} non-reahable subsets. We relax the notion of separatrix obtaining semi-separatrix urves suh that some

pointsin one set may bereahable fromthe other set, but not vie-versa.

Wedene rst the abovenotions for the plane independently of SPDIs.

Denition 7. Let

K ⊆ R ²

^{. A separatrix in}

K

^{is a losed urve}

γ

^parti-

tioning

K

^{into three sets}

K A

^,

K B

^and

γ

^{itself, suh that}

K A ∩ K B ∩ γ = ∅

^,

K = K A ∪ K B ∪ γ

^{and the following onditions hold:}

1. For any point

x 0 ∈ K A

^{and trajetory}

ξ

^{, with}

ξ(0) = x 0

^{, there is no}

t

suh that

ξ(t) ∈ K B

^{; and}

2. For any point

x 0 ∈ K B

^{and trajetory}

ξ

^{, with}

ξ(0) = x 0

^{, there is no}

t

suh that

ξ(t) ∈ K A

^.

If only one of the above onditions holds then we say that the urve is a

semi-separatrix. If only ondition 1 holds, then we say that

K A

^{is the inner}

of

γ

^(written

γ in

^{) and}

K B

^{is the outer of}

γ

^(written

γ out

^{). If only ondition}

2 holds,

K B

^{is the inner and}

K B

^{is the outer of}

γ

^.

Remark: Notie that,asinthe ase of theontrollabilitykernel, anedge of

the SPDI maybesplit intotwoby asemi-separatrixpartinside,and part

outside. As before, we an split the edge into parts, suh that eah part is

ompletely inside,or ompletelyoutside the semi-separatrix.

The set of all the separatries of

R ²

^{is denoted by}

Sep( R ² )

^{, or simply}

Sep

^.

The above notions are extended toSPDIs straightforwardly.

Now,let

σ = e 1 . . . e n e 1

^{beasimpleyle,}

∠ ^{b a} i ⁱ

⁽

1 ≤ i ≤ n

^{)bethe dynamisof}

theregionsforwhih

e i

^{isanentryedgeand}

I = [l, u]

^{andintervalonedge}

e 1

^.

Rememberthat

Succ _{e 1 e 2} (I) = F (I ∩ S)∩ J

^,where

F = [a 1 l +b 1 , a 2 u +b 2 ]

^{. Let}

l

^{bethe vetor} orrespondingtothe point on

e 1

^{with loaloordinates}

l

^and

l ^′

^{bethe vetor} orrespondingtothe pointon

e 2

^{with loaloordinates}

F (l)

(similarly,wedene

u

^and

u ^′

^for

F (u)

^{). Wedenerst}

Succ ^b _{e 1} ¹ (I ) = {x | l ^′ = αx + l, 0 < α < 1}

^and

Succ ^a _{e 1} ¹ (I) = {x | u ^′ = αx + u, 0 < α < 1}

^{. Weextend}

these denitions in a straight way to any (yli) signature

σ = e 1 . . . e n e 1

^,

denoting themby

Succ ^b _σ (I)

^and

Succ ^a _σ (I)

^,respetively;weanomputethem similarlyasfor

Pre

^{. Wheneverappliedtothex-point}

I ^∗ = [l ^∗ , u ^∗ ]

^,wedenote

Succ ^b _σ (I ^∗ )

^and

Succ ^a _σ (I ^∗ )

^by

ξ _σ ^l

^and

ξ _σ ^u

respetively. Intuitively,

ξ ^l _σ

⁽

ξ _σ ^u

^)denotes

thepiee-wiseanelosedurvedenedbytheleftmost(rightmost)x-point

l ^∗

⁽

u ^∗

^).

Weshow now howto identify semi-separatries for simple yles.

Theorem7. GivenanSPDI, let

σ

^{beasimpleyle,thenthefollowinghold:}

1. If

σ

^{is EXIT-RIGHT then}

ξ _σ ^l

^{is a} semi-separatrix urve (ltering tra- jetories from left to right);

2. If

σ

^{isEXIT-LEFTthen}

ξ _σ ^u

^{is a semi-separatrixurve (ltering traje-}

tories from right to left);

3. If

σ

^{is STAY, then the two polygons dening the invariane kernel}

(

Inv ^l (K σ )

^and

Inv ^u (K σ )

^),are semi-separatries.

leftby

ξ _σ ^l

^{,whihisapiee-wiseanelosedurve,}partitioning

R ²

^into

three disjoint sets:

K B

^{, the right part of}

ξ _σ ^l

^;

K A

^{, the left part of}

ξ _σ ^l

^{; and}

ξ _σ ^l

^{itself. By Jordan's theorem, any trajetory may pass from}

K B

^to

K A

^{if and only if it ross}

ξ ^l _σ

^{. However, by denition of EXIT-}

RIGHT,thisisonlypossiblefrom

K A

^to

K B

^{butnot vie-versa. Hene}

ξ _σ ^l

^{is a} semi-separatrixurve.

2. Symmetri tothe previous ase.

3. Follows diretly from the denition of invarianekernel, sine any tra-

jetorywithinitialpointin

Inv(K σ ) ∪ Inv _in (K σ )

^annotleave

Inv(K σ )

^.

If the trajetory yles lokwise it annot traverse

Inv ^l (K σ )

^{and if it}

yles ounter-lokwise it annot traverse

Inv ^u (K σ )

^{. In both ases no}

point on

Inv _out (K σ )

^{an be reahed.} Symmetrially,trajetories start- ing in

Inv(K σ ) ∪ Inv _out (K σ )

^{annot reah any point on}

Inv _in (K σ )

^.

Remark: In the ase of STAY yles,

ξ _σ ^l

^and

ξ _σ ^u

^{are also} semi-separatries.

Notie that in the above result, omputing a semi-separatrix depends only

onone simpleyle,and the orrespondingalgorithmisthenredued tond

simple yles in the SPDI and heking whether it is STAY, EXIT-RIGHT

or EXIT-LEFT.

Example 11. Fig. 5 shows all the semi-separatries of the SPDI given in

Example 1. The small arrows traversing the semi-separatries show the in-

ner and outer of eah semi-separatrix: a trajetory may traverse the semi-

separatrix followingthe diretion of the arrow, but not vie-versa.

The following two results relatefeasible signatures and semi-separatries.

Proposition 6. If, for some semi-separatrix

γ

^,

e ∈ γ in

^and

e ^′ ∈ γ out

^{, then}

the signature

ee ^′

^{is not feasible.}

Proof. Diretly fromthe denition of semi-separatrix.

Proposition 7. If, for some semi-separatrix

γ

^{, and signature}

σ

^{(of at least}

length 2), then, if head

(σ) ∈ γ in

^{and last}

(σ) ∈ γ out

^,

σ

^{is notfeasible.}

Proof. The proofproeedsby indutiononsequene

σ

^{. Thebase ase,when}

σ

^{isoflength2,reduesto}proposition6. Now,assumingthattheproposition istrue forsignatures oflength

n

^{,weare requiredtoprove thatitisalsotrue}

for signatures of length

n + 1

^{. Consider the signature}

σ ^′ = ee ^′ σe ^′′

^{, with}

Case 1:

e ^′ ∈ γ in

^{. Thesignature}

e ^′ σe ^′′

^{satisestheonditionsandisoflength}

n

^{. Therefore, theindutiveproperty applies,andwean onludethat}

e ^′ σe ^′′

^{is not feasible. However, sine any extension of an unfeasible}

signature is itself unfeasible,itfollows that

σ ^′

^{is not feasible.}

Case 2:

e ^′ ∈ γ out

^{. The signature}

ee ^′

^{is unfeasible by} proposition 6. There- fore,being anextensionof

ee ^′

^,

σ ^′

^{isalsounfeasible}(proposition1).

3 State-Spae Redution Using Semi-Separatries

Semi-separatriespartitionthe statespaeintotwo parts 3

oneonerosses

suh a border, all states outside the region an be ignored. We present a

tehnique, whih, given an SPDI and a reahability question, enables us to

disard portionsof the state spae basedon this information. The approah

is based onidentifyinginert states(edges in the SPDI) whih annotplaya

role in the reahability analysis.

Denition 8. Given an SPDI

S

^{, a set of semi-separatries}

Γ ⊆ Sep

^{, a}

soure edge

e0

^{and a} destination edge

e1

^{, an edge}

e

^{is said to be inert if it}

lies outside a semi-separatrix inside whih lies

e0

^{, or it lies inside a semi-}

separatrix outside whih lies

e1

^:

3

Wedon'tonsiderthesemi-separatrixitself.

inert

Γ

e 0→e 1 = {e : E | ∃γ ∈ Γ · e0 ∈ γ in ∧ e ∈ γ out }

∪ {e : E | ∃γ ∈ Γ · e1 ∈ γ out ∧ e ∈ γ in }

Weanprovethat theseinertedgesan neverappear inafeasible signature:

Lemma 8. Given an SPDI

S

^{, a set of} semi-separatries

Γ

^{, a soure edge}

e0

^{and a} destination edge

e1

^{, and a feasible signature}

e0σe1

ⁱⁿ

S

^{. No inert}

edge from inert

Γ

e0→e1

^{may appear in}

e0σe1

^.

Proof. From the denition of inert states, it follows that eitherboth

e0

^and

e1

^{are inert, or neither is. If both are inert, then for some}

γ

^,

e0 ∈ γ in

^and

e1 ∈ γ out

^{. But if this were so, then}

e0σe1

^{isunfeasible by} proposition7. We

an thus onsider onlyinert edges in

σ

^.

Let

e

^{be an inert edge appearing in}

σ

^{. Therefore,}

e0σe1 = e0σ 1 eσ 2 e1

^{. By}

denition of inert edges,

e

^{an either be inert beause (i) it lies outside a}

semi-separatrix inside whih lies

e0

^{, or (ii) it lies inside a} semi-separatrix outside whih lies

e1

^.

Case 1: Let

γ ∈ Γ

^beasemi-separatrixsuhthat

e0 ∈ γ in

^and

e ∈ γ out

^{. But}

by proposition 7,

e0σ 1 e

^{is not feasible. Hene, neither is}

e0σ 1 eσ 2 e1

^.

Case 2: Let

γ ∈ Γ

^{be a}semi-separatrixsuh that

e ∈ γ in

^and

e1 ∈ γ out

^{. By}

proposition 7,

eσ 2 e1

^{is not feasible, and hene, neitheris}

e0σ 1 eσ 2 e1

^.

It thus follows that

e0σe1

^{is not feasible.}

Given anSPDI, we an redue the state spae by disarding inert edges.

Denition 9. Givenan SPDI

S

^{, a set of} semi-separatries

Γ

^{, a soure edge}

e0

^{and a} destination edge

e1

^{, we dene the redued SPDI}

S _e0→e1 ^Γ

^{to be the}

same as

S

^{but without the inert edges.}

Clearly, the resultingSPDI is smaller than the originalone.

Proposition 8. For any SPDI

S

^{, aset of} semi-separatries

Γ

^{, andedges}

e0

and

e1

^,

S

^{does not have less edges than}

S _e ^Γ _0→e 1

^.

Example 12. The shaded (light blue) areas of Fig. 6 (a) and (b) are the

subsets of the SPDI (edges of the reahability graph) eliminated by the re-

dutionpresented in thissetion,whenansweringthe question: Isinterval

I ^′

reahable from

I

^?

I I’

(a)

I’

I

(b)

Figure6: Redution using Semi-separatries

Finally,weprovethathekingreahabilityonthereduedSPDIisequivalent

to hekingreahability onthe original SPDI:

Theorem 9. Given an SPDI

S

^{, a set of} semi-separatries

Γ

^{, and edges}

e0

and

e1

^{, then,}

e1

^{is reahablefrom}

e0

ⁱⁿ

S

^{if and only if}

e1

^{is reahable from}

e0

ⁱⁿ

S _e0→e1 ^Γ

^.

Proof. The proof is split into two parts: that reahability in the redued

SPDI implies reahability in the original automaton (soundness) and vie-

versa (ompleteness).

Soundness: Assume that

e1

^{is reahable from}

e0

ⁱⁿ

S _e ^Γ _0→e 1

^{. Then, there}

must exista feasiblesignature

σ

ⁱⁿ

S _e ^Γ _0→e 1

^{whihstarts on}

e0

^{and ends}

at

e1

^{. Sine every SPDI edge in}

S _e ^Γ _0→e 1

^{is alsoin}

S

^{, and the dynamis}

of thetwo systemsare idential, itfollows that

σ

^{isalsoafeasiblepath}

in

S

^{. Therefore,}

e1

^{isalso reahable from}

e0

ⁱⁿ

S

^.

Completeness: Now assume that

e1

^{is reahable from}

e0

ⁱⁿ

S

^{. By deni-}

tion of reahability, there exists a feasible signature

e0σe1

ⁱⁿ

S

^{. By}

proposition 8, no inert edge may appear in

e0σe1

^{. Therefore,}

e0σe1

is also a feasible signature in

S _e ^Γ _0→e 1

^{, whih in turn implies that}

e1

^is

reahable from

e0

ⁱⁿ

S e 0→e 1

^.

ity question,we an redue the size of the SPDI to beveried. Thisenables

ustoverify SPDIsmuhmoreeiently. It isimportanttonote thatmodel-

heking an SPDI requires identiation of simple loops, whih means that

the alulation of the semi-separatries is not more expensive than the ini-

tialpassof themodel-hekingalgorithm. Furthermore,wean perform this

analysis onlyone for an SPDI and store the information tobe used in any

reahabilityanalysis onthatSPDI. Redution,however, an onlybeapplied

one we know the soure and destination states.

4 State-Spae Redution Using Kernels

4.1 State-spae redution using kernels

We have already shown that any invariant set, is essentially a pair of semi-

separaties. In partiular, the invariane kernel is a largest invariantset for

apartiularloop,weanuse theresultspresented insetion3toabstrat an

SPDI by using invarianekernels. We nowturn our attention tostate spae

redution using ontrollabilitykernels:

Denition 10. Givenan SPDI

S

^{, a loop}

σ

^{, a soure edge}

e0

^{and a destina-}

tion edge

e1

^{, an edge}

e

^{issaid to be redundant if it lies on the opposite side}

of a ontrollability kernel as both

e0

^and

e1

^:

redundant

σ

e 0→e 1 = {e : E | ∃e0, e1 ∈ Cntr _in (σ) ∪ Cntr (σ) ∧ e ∈ Cntr _out (σ)}

∪ {e : E | ∃e0, e1 ∈ Cntr _out (σ) ∪ Cntr (σ) ∧ e ∈ Cntr _in (σ)}

Wean prove that we an dowithout these edges tohek feasibility:

Lemma 10. Given an SPDI

S

^{, a loop}

σ

^{, a soure edge}

e0

^{, a} destination edge

e1

^{, and a feasible signature}

e0σe1

^{then there exists a feasible signature}

e0σ ^′ e1

^{suh that}

σ ^′

^{ontains no redundant edge from redundant}

^σ _e0→e1

^.

Proof. Let

e0σe1

^{beafeasiblesignaturewhihontainssomeredundantedge}

from the set redundant

σ

e 0→e 1

^{. Without loss of} generality, we assume that

e0, e1 ∈ Cntr _out (σ) ∪ Cntr(σ)

^{. Let}

f0

^and

f 1

^be, respetively, the rst and last redundant edges in

σ

^{. By denition of redundant edges, it follows that}

f 0, f 1 ∈ Cntr _in (σ)

^{. The path we are following isthus:}

Sine

f0

⁽

f 1

^{)istherst(last)redundantedge,itfollowsthatthelastelement}

of

σ 1

^{(the rst element of}

σ 3

^{) is inside the} ontrollability kernel. Using proposition 3, it follows that there exists a point

p

^{on the} ontrollability kernel reahablefrom the lastelementof

σ 1

^(apoint

q

^onthe ontrollability kernel from whih the rst element of

σ 3

^{is reahable). Sine all points on}

theontrollabilitykernelaremutuallyreahable,itfollowsthat

q

^isreahable

from

p

^{along some disrete path}

σ 2 ^′

^{ompletely within the kernel. We have}

thusobtained ashorterdisretepath

e0σ 1 σ 2 ^′ σ 3 e1

^{whihisfeasibleand whih}

ontains noredundant edges.

GivenanSPDI,weanreduethestatespaebydisardingredundantedges.

Denition 11. Given an SPDI

S

^{, a loop}

σ

^{, a soure edge}

e0

^{and a desti-}

nation edge

e1

^{, we dene the redued SPDI}

S _e ^σ _0→e 1

^{to be the same as}

S

^but

without redundant edges.

Clearly, the resultingSPDI is smaller than the originalone.

Proposition9. ForanySPDI

S

^,aloop

σ

^{, asoureedge}

e0

^andadestination edge

e1

^,

S

^{does not have less edges than}

S _e0→e1 ^σ

^.

Finally,weprovethathekingreahabilityonthereduedSPDIisequivalent

to hekingreahability onthe original SPDI:

Theorem 11. Givenan SPDI

S

^{, witha setof loops}

σ

^{, a soure edge}

e0

^and

a destination edge

e1

^{, then,}

e1

^{is reahable from}

e0

ⁱⁿ

S

^{if and only if}

e1

^is

reahable from

e0

ⁱⁿ

S _e ^σ _0→e 1

^.

Proof. The theorem follows immediatelyfrom proposition 10.

Given aloopwhih hasa ontrollabilitykernel, wean thusreduethe state

spae to explore. In pratie, we apply this state spae redution for eah

ontrollability kernel in the SPDI. One a loop in the SPDI is identied, it

is straightforward to apply the redution algorithm.

4.2 Immediate answers to reahability questions

By denition of the ontrollability kernel, any two points inside it are mu-

tually reahable. This an be used to answer ertain reahability questions

simply by inspeting the ontrollability kernel: if both the soure and des-

tination edge lie (possibly partially) within the same ontrollability kernel,

then, there exists atrajetory from the soureto the destination edge.