On the decidability of the reachability problem for GSPDIs

Department of Informatis

On the Deidability of

the Reahability

Problem for GSPDIs

Researh Report No.

359

Gerardo Shneider

Isbn 82-7368-317-6

Issn 0806-3036

June 2007

Problem for GSPDIs

Gerardo Shneider

Department of Informatis, University of Oslo

PO Box 1080 Blindern, N-0316 Oslo, Norway

E-mail: {gerardo at i.uio.no}

Abstrat

Polygonal hybrid systems (SPDIs) are a sublass of hybrid sys-

tems whosedynamis isdenedbyonstantdierentialinlusions, for

whihthe reahabilityproblemisdeidable. Thedeidabilityresultis

based, among otherthings, onthefatthat atrajetoryannot enter

and leave a given region through the same edge. An SPDI satisfy-

ing the above restrition is said to have the goodness property. In a

previous work we have given amisleading proofskethof deidability

of reahability for SPDIs when relaxing goodness. In this work we

give a ounter-example to suh proof and we give an algorithm for

semi-deiding reahability ofsuh lassof systems.

1 Introdution

An interesting andstilldeidable (w.r.treahability)lass of hybridsystems

is the so-alledPolygonal Hybrid System (SPDI for short, [ASY01, ASY07,

Sh02 ℄) whih is a sublass of hybrid systems onthe plane whose dynamis

is dened by onstant dierential inlusions. SPDIs are a generalization of

PCDs(deterministisystemswithPiee-wiseConstantDerivatives)forwhih

it has been shown that the reahability problem is deidable for the pla-

nar ase [MP93℄ but undeidablefor three and higher dimensions [AMP95℄.

Slight extensions of suh deidable lasses have been proved to be undeid-

able or equivalent to a problem for whih deidability or undeidability is

not known [AS02, MP05℄.

The onstrutive proof for deiding reahability on SPDI given in [ASY01℄

(see also [ASY07℄ and [Sh02, Chap. 5℄) relies, among other things, on the

the SPDI(loationof theorrespondingautomaton)doesnotallowatraje-

torytotraverseanyedgeofthepolygondeningtheregioninbothdiretions.

Tehnially this means that the diretor vetor of eah edge annot be ob-

tained asapositivelinearombinationofthe vetors dening thedynamis.

An SPDI withoutthe goodness property is alled GeneralSPDI or GSPDI

forshort. Wehavewronglylaimedin[Sh02,Chap. 9℄thatthe reahability

problemforGSPDIisdeidable. Theproofskethwasondutedby proving

that any GSPDI an be redued to a set of SPDIs, preserving reahabil-

ity. The proofsketh, aspresented, is notompletelywrong butinomplete,

letting the deidability onlusion to be still inonlusive. Unfortunately

we have disovered suh mistake in September 2002, just few months after

the nal print of the thesis. We onsidered it was not worth publishing a

refutation of the result at that moment sine there was no researh being

onduted in that diretion then. We revived our interest on the subjet

again only reently due to the publiation of the paper [MP05℄, in whih

the frontier between deidable and undeidable hybrid systems is revisited,

to rene previous result given in [AS02℄. The deidability of reahability of

GSPDIs would have ontributed to narrowthe undeidability frontier; with

the result presented here we letit stillopen, unfortunately.

Inthispaperweprovideaounter-exampletothelaimofthedeidabilityof

thereahabilityproblemforGSPDIsgivenin[Sh02 ,Chap. 9℄,whihremain

thus an open problem. We prove, indeed, that GSPDI reahability annot

be redued to SPDI reahability. We rephrase the results given in [Sh02℄

to give a semi-deidable algorithm for solving the reahability problem for

GSPDIs.

The paper isorganized as follows. In next setionwe explain informallythe

problems arising when relaxing goodness while in Setion 3 we give some

preliminaries,providinguseful notationanddenitionsand reallingthedef-

initionofSPDI.InSetion4wepresentGSPDIs. Setion5isonernedwith

the analysis of trajetories, providing some results needed to establish the

semi-deisionalgorithmforreahability presented inSetion6. Weonlude

in the lastsetion.

2 On Goodness

In this setion we disuss informally why goodness is good for deiding the

reahability problem of SPDI and what are the problems when relaxing it.

More formaldenitions willbe given inSetion 3.

See Fig. 1 for an example of a good and a 'bad' region (here 'bad' stands

gure we an see a good region, where the two vetors

a

and

b

determine

the impossibilityof atrajetorytoenter and leavethe region

P

^{through the}

same edge of the polygon delimiting the region. On the other hand, the

gureontherightshows abadregion: Both

e 2

^and

e 5

^{anberossedinboth}

diretions by atrajetoryentering and leaving

P

^.

e 1

e 2

e 3

e 6

e 1

e 2

e 5

e 6

e 4

e 3

e 4

e 5

P P

y

x α

β a b

(a) (b)

y

x a

b

β α

Figure 1: a)A goodregion. b)A bad region.

2.1 Why Goodness is Good?

The algorithmpresentedin[Sh02 ℄fordeidingreahabilityonSPDIheavily

depends on the pre-proessing of trajetory segments to guarantee that it

is possible to list all the possible sets of signatures, i.e., those sequenes

of edges of the SPDI traversed by all the possible trajetories between two

points. This isof ourse not possible in generalas there are innitely many

suhtrajetories. However, aqualitativeanalysisallowstoprovethatindeed

there are a nite number of types of signatures, that are kind of abstrat

signatures that preserve the reahability property.

Briey, the aboveis ahieved by performingthe followingsteps.

1. Simpliationoftrajetorysegments: straighteningthemandremoving

self-rossings. Givenanarbitrarytrajetorysegmentfromonepointto

another, weshowhowtoget apieewise onstantderivativetrajetory

segment withoutself-rossing.

2. Abstration of trajetory segmentsintosignatures, onsidering the se-

queneoftraversededges. ThisresultisbasedonthePoinarémap[HS74,

NS60℄, that relates

n

^-dim ontinuous-time systems with

(n − 1)

^-dim

disrete-time systems.

3. Fatorization of signatures ina onvenientway, having onlysequenes

of edges and simple yles. This fatorization allows to have a nie

representation of signatures.

4. Abstration of fatorized signatures into types of signatures, that are

signatureswithouttakingintoaountthenumberoftimeseahsimple

yle isiterated.

Many of the lemmas for proving that the above provides anite number of

typessignaturesritiallydependonthegoodnessassumption,whihpropa-

gatethisdependenytotheonstrutiveproofgivenfordeidingreahability

of SPDIs.

2.2 Why Relaxing Goodness is not so Good?

The mainquestion nowis,howmuh doweneed todepend onthe goodness

assumption to prove deidability of reahability of SPDIs? In other words,

let us onsider the new lass of polygonal hybrid systems, GSPDI, obtained

by relaxinggoodnessinSPDI.Isreahabilitystilldeidable? Fromtheabove

disussion weare letwith the followingtwoalternatives:

1. Adapt the proofs of deidability for SPDIs to GSPDIs. This would

implytorestate the proofstomakethem independent of the goodness

assumption.

2. ProvideaompletelynewdeidabilityproofforGSPDI.Thiswillprob-

ablyneedtouse dierenttehniquesand resultsthantheones usedfor

SPDIs.

The rst alternative above seems the most straightforward and easy to do.

However, aswewillshowlateritisnotpossibletoredueGSPDIreahability

toSPDIreahability. Thisisdonebyprovingthatitisnotingeneralpossible

tosimplifyertaintrajetoriesenteringandleavingagivenregionthroughthe

same edge, totrajetoriesbehaving as in SPDIs. One of the main problems

whenrelaxinggoodnessisthataregionannotbebi-partitionedanymoreinto

twosemi-planeswerealltheedgesinonesemi-planean betraversedonlyin

one diretion,w.r.t. theregion,andalltheedgesinthe othersemi-planean

be traversed only in the other diretion. That is, the goodness assumption

permit a ertain 'ontiguity' of entry edges and exit edges belonging to two

the reahability algorithm depend on this ontiguity. If we relax goodness,

weshouldbeabletore-proveallsuhresultswithoutassumingtheontiguity

of entry and exit edges.

This letus with the seond alternative. Unfortunately, to date we have not

sueeded inproviding a proof of deidability (nor of undeidability) to the

reahabilityproblem onGSPDIs.

On the other hand and as stated in the introdution, we willshow that we

an relax the goodness assumption as to give a terminating semi-deision

algorithmfor reahability analysis on GSPDIs.

3 Preliminaries

This setion is more tehnial, realling the main denitions and onepts

needed tounderstandthe restofthe paper. Foramoredetailedpresentation

see [ASY07, Sh02℄.

3.1 SPDI

Let

a = (a 1 , a 2 ), x = (x 1 , x 2 ) ∈ R ²

^and

α, β ∈ R

^{. The inner produt of two}

vetors

a = (a 1 , a 2 )

^and

x = (x 1 , x 2 )

^{is dened as}

a · x = a 1 x 1 + a 2 x 2

^{. We}

denote by

x ˆ

the vetor

(x 2 , −x 1 )

^{obtained from}

x

by rotating lokwise by the angle

π/2

^{. Notie that}

x · x ˆ = 0

^.

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

.

Denition 1. A polygonal dierential inlusion system (SPDI) is dened

by giving a nite partition

P

^{of the plane into onvex polygonal sets (alled}

regions), and assoiating with eah

P ∈ P

^{a ouple of vetors}

a _P

and

b _P

. Let

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

^{, we have that for eah}

x ∈ P

^,

x ˙ ∈ φ(P )

^.

Let

E(P )

^{bethe set of edgesof}

P

^{. Wesay that}

e ∈ E(P )

^{isanentry 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 of all entries of}

P

^{and by Out}

(P ) ⊆ E(P )

^{the set of}

all exitsof

P

^.

Assumption 1. All the edges in

E(P )

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

E(P ) =

^In

(P ) ∪

^Out

(P )

^{. We say then that all the regions in an SPDI are}

good or that they have the goodness property.

Example 1. In Fig.1-(a), region

P

^(with

φ(P ) = ∠ ^{b a}

^{) is good,sine all are}

entry orexitedges. Fig. 1-(b) shows aregionthat isnot good: edges

e 2

^and

e 5

^{are not inIn}

(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.}

The following is a very simple example of an SPDI: a swimmer trying to

esape froma whirlpoolina river.

Example. The dynamis

x ˙

of the swimmer around the whirlpool is ap- proximated by the piee-wise dierential inlusion dened as follows. The

zoneoftherivernearbythewhirlpoolisdividedinto8regions

R 1 , . . . , R 8

^{. To}

eahregion

R i

^{weassoiate apair of vetors}

( a _i , b _i )

^meaningthat

x ˙

belongs to theirpositivehull:

a ₁ = b ₁ = (1, 5)

^,

a ₂ = b ₂ = (−1, ¹ ₂ )

^,

a ₃ = (−1, ¹¹ ₆₀ )

^and

b ₃ = (−1, − ¹ ₄ )

^,

a ₄ = b ₄ = (−1, −1)

^,

a ₅ = b ₅ = (0, −1)

^,

a ₆ = b ₆ = (1, −1)

^,

a ₇ = b ₇ = (1, 0)

^,

a ₈ = b ₈ = (1, 1)

^{. The} orresponding SPDI is illustrated in Fig. 2.

R 3

R 7

R ₁ R ₅

e 3

R ₄

R ₆

e 4

e 5

e 2 R ₂

e 6 e 7

e 8

e 1

R 8

Figure2: The SPDI of the swimmer.

Given anSPDI, we xa one-dimensionaloordinatesystem oneah edge to

representpointslayingonedges. Fornotationalonveniene, wewilluse

e

^to

denote both the edge and its one-dimensional representation. Aordingly,

we write

x ∈ e

^or

x ∈ e

^{,to meanpoint}

x

inedge

e

^{with oordinate}

x

^inthe

one-dimensional oordinate system of

e

^{. The same onvention is applied to}

sets of pointsof

e

represented asintervals(e.g.,

x ∈ I

^or

x ∈ I

^,where

I ⊆ e

⁾

and to trajetories (e.g.,

ξ

^startingin

x

^or

ξ

^startingin

x

).

Now, let

P ∈ P

^,

e ∈

^In

(P )

^and

e ^′ ∈

^Out

(P )

^{. For}

I ⊆ e

^,

Succ _ee ′ (I)

^is

the set of all points in

e ^′

^{reahable from some point in}

I

^{by a trajetory}

segment

ξ : [0, t] → R ²

ⁱⁿ

P

^(i.e.,

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

^{). Given}

I = [l, u]

^,

Succ _ee ′ (I) = F (I ∩ S) ∩ J

^{, where}

S

^and

J

^{are intervals,}

F ([l, u]) = hf l (l), f u (u)i

^and

f l

^and

f u

^{are anefuntions(afuntion}

f : R → R

^isane

i

f (x) = ax + b

^with

a > 0

^).

For

I ⊆ e ^′

^,

Pre _ee ′ (I)

^{isthe set of points in}

e

^{that an reah apointin}

I

^{by a}

trajetorysegment in

P

^{. Wehave that:}

Pre _ee ′ = Succ ⁻¹ _ee ′

^and

Pre _σ = Succ ⁻¹ _σ

^.

3.1.2 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

^.

Assumption 2. None of the two funtions

f l , f u

^{is the identity.}

Let

l ^∗

^and

u ^∗

^{bethe x-points1 of}

f l

^and

f u

^,respetively,and

S ∩ J = hL, Ui

^.

It an beshown that asimple yle is of one of the following types:

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

^.

1

Thex-point

x ^∗

^{is omputedbysolvingalinearequation}

f (x ^∗ ) = x ^∗

^{, whih anbe}

niteorinnite.

but the leftmost one stays inside, that is,

L ≤ l ^∗ ≤ U < u ^∗

^.

The lassiation above provides useful information about the qualitative

behavior of trajetories. Any trajetory that enters a yle of type DIE will

eventuallyquititafteranitenumberof turns. Iftheyle isoftypeSTAY,

all trajetories that happen to enter it will keep turning inside it forever.

In allother ases, some trajetories will turn for a while and then exit, and

others will ontinue turning forever. This information is ruial for solving

the reahability problemfor SPDIs.

To nish this setion we reall the representation theorem for SPDIs that

allows tofatorize thesignatures (step3 inSetion2.1)ina onvenient way.

Given a sequene

w

^,

ε

^{denotes the empty sequene whereas}

f irst(w)

^and

last(w)

^{are the rst and lastelements of the sequene} respetively. An edge signature

σ

^{an be expressed as a sequene of edges and yles of the form}

r 1 s ^k 1 ¹ r 2 s ^k 2 ² . . . r n s ^k _n ⁿ r n +1

^{, where}

1. For all

1 ≤ i ≤ n + 1

^,

r i

^{is asequene of pairwise dierent edges;}

2. Forall

1 ≤ i ≤ n

^,

s i

^{isasimple yle (i.e., withoutrepetition ofedges)}

repeated

k i

^times;

This is summarized by the followingrepresentation theorem for SPDIs that

not only guarantees the existene of the aboverepresentation for SPDIs but

also provides aonstrutive way of doing so[Sh02 , Theorem 17℄.

Theorem 1. Given an SPDI, let

σ = e 1 . . . e p

^{be an edge signature, then it}

analwaysbewrittenas

σ A = r 1 s ^k 1 ¹ . . . r n s ^k _n ⁿ r n +1

^,whereforany

1 ≤ i ≤ n+1

^,

r i

^{is a sequene of pairwise dierentedges andfor all}

1 ≤ i ≤ n

^,

s i

^{isa sim-}

ple yle (i.e., without repetition of edges).

This representation of signatures is the base to obtain types of signatures

(step 4 in Setion 2.1) with the following good properties [Sh02, Lemma

20℄.

Lemma 2. Given an SPDI, let

σ = e 0 . . . e p

^{be a feasible signature, then its}

type,

type(σ) = r 1 , s 1 , . . . , r n , s n , r n +1

^{satises the following} properties.

P ₁

For every

1 ≤ i 6= j ≤ n + 1

^,

r i

^and

r j

^{are disjoint;}

P ₂

For every

1 ≤ i 6= j ≤ n

^,

s i

^and

s j

^{are dierent.}

The above is the base for the argument on the niteness of dierent types

of signatures to take into aount in the reahability algorithm and thus to

termination of SPDI reahability.

Thegoodnessrestrition(Assumption1)wasoriginallyintroduedtosimplify

treatment oftrajetoriesto guarantee, amongother things,that eahregion

an be partitioned into entry and exit edges inan ordered way, fat used in

the proof of deidability of the reahability problem. We will study in this

setion what happens when goodness is relaxed. First notie that without

goodness there are edges that are neither of entry nor of exit as shown in

Fig. 1. This naturallyleads to the followingdenition.

Denition 2. An edge

e ∈ P

^{is an inout edge of}

P

^if

e

^{is neither an entry}

nor an exit edge of

P

^.

Asalreadyexplainedinprevioussetions,the abovedenitionisthebasefor

obtaininga new lass of polygonal hybrid systems whih generalizes SPDI.

Denition 3. An SPDI without the goodness restrition is alled a general

SPDI (GSPDI).

Thus, inGSPDIs there are three kinds of edges: inouts, entries and exits.

Self-rossing of trajetorysegments of SPDIs an be eliminatedwhih allow

us to onsider only non-rossing trajetory (segments). The proof given in

[Sh02 , Chap. 4, Se. 4.2.2℄ an be extended to deal with the ase when

the self-rossing trajetories involve inout edges, so the result still holds for

GSPDIs. Thus in what follows we will onsider only trajetory segments

without self-rossings.

Notie that on GSPDIs a trajetory an interset an edge at an innite

number of pointsbeause it an slide at it. Thus, a trae is not anymore a

sequene of points but rather asequene of intervals.

Denition4. The traeof a trajetory

ξ

^isthesequene

trace(ξ) = I 0 I 1 . . .

of the intersetion intervals of

ξ

^{withthe set of edges, thatis,}

I i ⊆ (ξ ∩ E )

^.

A point interval

I = [ x , x ]

^{will be sometimes written as}

x

whenever no onfusion mightarise.

Denition 5. An edge signature (or simply a signature) of a GSPDI is

a sequene of edges. The edge signature of a trajetory

ξ

^,

Sig(ξ)

^{, is the}

orderedsequeneoftraversededgesbythetrajetorysegment,thatis,

Sig (ξ) = e 0 e 1 . . .

^{, with}

trace(ξ) = I 0 I 1 . . .

^and

I i ⊆ e i

^{. The region signature of}

ξ

^is

the sequene

RSig(ξ) = P 0 P 1 . . .

^{of traversed regions, that is,}

e i ∈

^In

(P i )

^.

Notie that in many ases the intervals of a trae are in fat points. We

say that a trajetory with edge signature

Sig (ξ) = e 0 e 1 . . . e i . . .

^{and trae}

trace(ξ) = I 0 I 1 . . . I i . . .

interval-rossesedge

e i

^if

I i

^{is not apoint.}

(a’) (a)

x 0

x _f x _f

x 0

e e

Figure3: (a): A properinout edge; (b): A slidingedge.

Givenatrajetorysegment,wewillmakethe dierenebetween proper inout

edges and sliding edges.

Denition 6. Let

ξ

^{be a trajetory segment from point}

x ₀ ∈ e 0

^to

x _f ∈ e f

^,

with edge signature

Sig (ξ) = e 0 . . . e i . . . e n

^{, and}

e i ∈ E(P )

^{be an edge of}

P

^.

We say that

e i

^{is a sliding edge of}

P

^for

ξ

^if

ξ

interval-rosses

e i

^{, otherwise}

e

^{is saidto be a properinout edge of}

P

^for

ξ

^.

Wesaythatatrajetorysegment

ξ

^{slidesonanedge}

e

^if

e

^{isaslidingedgeof}

P

^for

ξ

^and

ξ

^{is said to be a sliding trajetory if there is at least one sliding}

edge

e ∈ Sig (ξ)

^.

Example 2. In Fig. 3-(a),

e

^{is aproperinout edge. Edge}

e

^{onFig. 3-(b)is}

a sliding edge.

5 Simpliation of GSPDI's Trajetory Segments

Inthissetionweshowthatinmanyasesitispossibletosimplifytrajetory

segments eliminatinginoutedges, but not always. Werst start by showing

that the good properties of the representation theorem for SPDIs are not

validany longer for GSPDIs, explaining why inouts edges are not desirable

in areahability analysis.

Proposition1. Property

P ₂

oftherepresentationtheoremforSPDIs(Lemma 2) does not hold in general for GSPDIs.

Proof: Let

ξ

^{be a trajetory with signature}

Sig(ξ) = σ = e 0 . . . e i . . . e n . . .

of a given GSPDI. The proposition states that it is not possible in general

to write

σ

^{in the form}

σ A = r 1 s ^k 1 ¹ . . . r n s ^k _n ⁿ r n +1

^{with the properties stated}

ounter-example shouldallowtoobtain asignature onsistingof alokwise

spiral followed by aounter-lokwise spiral(orvie-versa) and thenbak to

the rst spiral. In suh a ase it is possible to nd two simple yles whih

are repeated inthe type of signature. Let us onsider the GSPDI of Fig. 4.

To let it simple we do not write down the dynamis of the regions and we

assume that they are as to allow the segments of trajetories shown in the

pituretobewell-dened. InsuhaGSPDIitispossibletoobtainthefollow-

ing type of signature:

r 1 s 1 r 2 s 2 r 3 s 3 . . .

^{, where}

s 1 = (abcd)

^,

s 2 = (dcba)

^{, and}

s 3 = (abcd)

^{. Sine}

s 1 = s 3

^{,thenproperty}

P ₂

ofLemma2isnotsatised.

a b

c

d

Figure4: Counter-example for Proposition1.

The followinglemmapresentssometypialaseswhereitispossibletoelim-

inate properinout edges.

Lemma 3. Let

ξ

^{be a trajetory segment}

x ₀ ∈ e 0

^to

x _f ∈ e f

^{with edge}

signature

Sig(ξ) = e 0 . . . e i . . . e n

^{. If}

e i

^{is a proper inout edge then in some}

ases there exists a trajetory segment

ξ ^′

^from

x ₀

to

x _f

that traverses

e i

ⁱⁿ

at most one sense (that is,

e i

^{is either an entry or an exit, but no both).}

Proof Sketh: In Fig. 5-(a) we illustrate a typial ase where edge

e i

^{is a}

properinoutedge. Afterastraightforwardalgebraivetormanipulation,on

in Fig. 5-(a')is obtained.

x f

(a)

x 0

x f

e e

(a')

x 0

Figure5: Inout ase.

Note that the above does not establish ompleteness of a redution from

GSPDIs intoSPDIs reahability sinethere areases wherethe above isnot

possible. Wehave then the followingresult.

Proposition 2. Given a GSPDI, assume there exists a trajetory segment

from points

x ₀ ∈ e 0

^to

x _f ∈ e f

^{, traversing inout edges in both diretions.}

Then it is, in general, not possible to nd a trajetory segment whose edge

signature ontains no proper inout edges (traversed in both diretions), be-

tween them.

Proof: TheGSPDIofFig. 6presentsatypialexampleofaninoutedge(

e 2

⁾

whihannot bediretly eliminated astopreservethat

x f

^{isreahablefrom}

x 0

^{. Tokeep the} explanation simple we donot present here a formalGSPDI as ounter-example. The example, however, sheds some light onthe kind of

GSPDIregionsservingasounter-examples. Itsuestotakeanytrajetory

with a dynamis suh that the angle is slightly less than 180 degrees. The

trajetorymusttraverse aninout edgefollowingthe

b

vetorand entersinto theregionbyfollowingthe

a

vetor. Thetrajetorymustnotrossitself.

Weshow now howto eliminatesliding edges.

Lemma 4. Let

ξ

^{be a trajetory segment}

x ₀ ∈ e 0

^to

x _f ∈ e f

^{with edge}

signature

Sig(ξ) = e 0 . . . e i . . . e n

^{. If}

e i

^{is aslidingedge for}

ξ

^{thenthere exists}

a trajetory segment

ξ ^′

^from

x ₀

to

x _f

that does not slide on edge

e i

^.

x 0

e 5

P _b

a

e 1

x f

e 2

e 3

e 6

e 4

Figure6: A GSPDI with a non-eliminatinginout edge.

Proof Sketh: Slidingedgesanariseinfourdierentases(withouttaking

intoaount thesymmetriases); theyare shown inFig.14-(a)to(d). The

orresponding primed gures (Fig. 14-(a') to (d')) show the transformation

done in order to avoid sliding on edge

e

^{. The reason why the above trans-}

formation ispossible isbeause inallthe ases the new obtainedsegment of

trajetory an be expressed as a positivelinear ombination of two suitable

existing segments of trajetory. Suh two segments are the sliding segment,

and another segment of trajetory with starting point at the beginning or

the end of the sliding segment.

As a onsequene we have the following result.

Proposition 3 (Existeneofanon-slidingtrajetory). If there existsa slid-

ing trajetorysegment from points

x ₀ ∈ e 0

^to

x _f ∈ e f

^{thentherealways exists}

a non-slidingtrajetory segment between them.

Proof: By indution on the number

n

^{of sliding edges of the signature of}

the trajetorysegment using Lemma 4 inthe indution step.

Weusually eliminaterst properinout edges (whenpossible)and next slid-

ing. In fat, the number of sliding edges is not guaranteed to derease if

sliding edges are eliminated before proper inout edges as shown in the fol-

lowingexample.

Example3. InFig. 7-(a)atrajetorysegmentthatslidesatedge

e ^′

^isshown.

After eliminatingthe sliding atedge

e ^′

^{,a newsliding edge isintrodued(}

e

^).

This is shown in Fig. 7-(b). However, if proper inout edges are eliminated

same gure.

x f x f x f

(a)

x 0

e e ^′

(b)

x 0

e e ^′

()

x 0

e e ^′

Figure7: Eliminationorder of inout edges.

Remark. Slidingis noteasy totreatingeneralsine anedgealways belong

to two dierent regions with dierent dynamis. Thus a trajetory may be

'allowed' to slide by one of the dynamis but not by the other. We do not

analyze this in more detail, for our purposes we assume that at an inout

edge a trajetory an slide if at least one of the dynamis allows so. This

assumption does not aet the reahability analysis.

About the ordering between edges. We nish this setion with an

informal disussion about the importane of the 'ontiguous' order between

entry and exit edges onSPDIs.

In SPDIsedges of aregionan bebi-partitionedintoentryand exitedges in

a ontiguous way (see Fig. 8) having as a onsequene an orderingbetween

edges. This is not longer the ase in GSPDIs.

P

b a

In

Out

Figure 8: Ordering of edges onan SPDI (allthe edges

e

^satisfy

a e ˆ > 0

^).

order to preserve the `positiveanity' (and hene the monotoniity) of the

suessor funtions. Given a region

R

^{with dierentialinlusion}

∠ ^{b a}

^,let

e

^be

anentryedgeand

e 1

^and

e 2

^{twoexitedgesof}

R

^{. For}

e

^{wehosethe diretion}

(given by a diretor vetor

e

) that satises the inequality

ˆ a e > 0

^{(see Fig.}

11). The same for

e 1

^and

e 2

^{. As a onsequene we obtain an ordering like}

the one shown in Fig. 8.

Note that on a GSPDI (see Fig. 9(a)), the property that for any edge

e

^,

ˆ

a e > 0

^{isnot longervalidsine anedgean beofentryand ofexitand then}

the ordering an hange. In spite of that, one an inout edge is 'onverted'

into an entry (or exit) then we an have the notation of onsidering the

ordering of entry edges going ounter-lokwise and lokwise for exit edges

(see Fig. 9(b)).

(a) (b)

P

a

In

In In

In

Out Out

Out Out

b

P

a

I n

I n I nout

I nout

I nout

I nout Out

b I nout

Figure9: (a)A GSPDI; (b) Ordering after xing input and output edges.

Eventhoughthedenitionofedgeandregionsignaturesaswellasedgeyle

ontinue to hold, it is not the ase for region yle. We an have a region

signature

P 1 · · · P i · · · P k P 1

^{that is not a region yle. The reason is that in}

GSPDIs a trajetory an enter a regionthrough two dierent edges without

forming a yle.

Thuswehavethataregionsignature

P 1 · · · P i · · · P k P 1

^{isaregion yle if the}

edge signature

e 1 · · · e k e 1

^,with

e i ∈

^Out

(P i )

^{for all}

1 ≤ i ≤ k

^{, forms anedge}

yle.

In Fig. 10 the following is a region yle:

P 1 P 2 P 3 P 4 P 2 P 5 P 1

^{. Notie that}

P 2 P 3 P 4 P 2

^{isregion yle forSPDIs but not for the given GSPDI.}

P 2

P 3

P 4

P 1

P 5

e 1

e 2

e 3

e 4

e 5

e 6

Figure10: A regionyle.

6 Reahability Analysis for GSPDIs

In this setion we `topologially' rephrase and prove the results of [Sh02,

Chap. 4,5℄ that use the ontiguity between entry and exit edges in their

proofs. Wealsore-provesoundnessofExit-LEFTandExit-STAYalgorithms

andattheendwegiveasemi-deisionalgorithmforGPSDIreahability. We

have informallyexplainedin Setion2.2why we need to doso.

6.1 Proof of Lemmas without using the Contiguity As-

sumption

The onlyresults that use the ontiguity order between entry and exit edges

are Lemmas20,Lemma 26and Corollary27of [Sh02 ℄. Lemma20hasbeen

repeated hereinSetion3asLemma2,whihaswe have seendoesnot hold

ingeneralfor GSPDIs(Proposition1). However, afterxing allthe edgesas

either of entry or exit, we an prove the result holds sine it behaves as an

SPDI, modulothe ontiguity of entry and exit edges.

Weprovethenthese threeresultswithoutusingthe orderbetween entryand

exit edges. We restate Lemma 2 ([Sh02, Lemma 20℄) for property

P ₂

, for the ase whenGPSDI istransformedastoxinout edgesasentries orexits.

Lemma 5. Given a GSPDI where edges has been xed as entry or exit, let

σ = e 0 . . . e p

^{be a feasible signature, then its type,}

type(σ) = r 1 , s 1 , . . . , r n ,

(a) (b)

P

e e

P

e

ˆ a

e

a a

ˆ a

Figure11: (a)

ˆ a e > 0

^{; (b)}

a e ˆ < 0

^.

s n , r n+1

^{satisesthe followingproperty,}

P ₂

: For every

1 ≤ i 6= j ≤ n

^,

s i

^and

s j

^{are dierent.}

Proof: In order to prove property

P ₂

we prove that, given a simple yle

s i = e ^′ , . . . , e

^{,thesequene ofedges}

ee ^′

^{annotourafterleaving}

s i

^(heneit

annotourinanyothersimpleyle

s j

^,with

1 ≤ i < j ≤ n

^{). Afteryling}

k i

^{times yle}

s i

^{is abandoned by edge}

e

(guaranteed by onstrution). Let

P

^{be a region s.t.}

e ∈

^In

(P )

^{and onsider the unfolding of the last iteration}

and its ontinuation(see Fig.12-(a)):

. . . , e, e ^′ , . . . , e, e ^′′ , . . .

where

e ^′′ = f irst(r i+1 )

^,

e ∈

^In

(P )

^and

e ^′ , e ^′′ ∈

^Out

(P )

⁽

e ^′ 6= e ^′′

^{). Let}

x 2

^be

thelastpointvisitedonedge

e

^{beforeleavingyle}

s i

^and

x ^′′ 2

^{betherstpoint}

on edge

e ^′′

^{after leaving}

s i

^{(see Fig. 12-(b)). Segment}

x ₂ x ^′′

2

^{of the trajetory}

segment divides region

P

^{intotwosubregions}

P 1

^and

P 2

^andedge

e

^intotwo

segments

e ^l x 2

^and

x 2 e ^u

^{. By the} non-rossing hypothesis (and monotoniity on edges) after leaving

s i

^{the only aessible part of edge}

e

^{is the segment}

x 2 e ^u ∈ e

^{. ByJordan'surve theorem theonly way toreahedge}

e ^′

^fromany

pointin

x 2 e ^u ∈ e

^isbyrossing

x ₂ x ^′′ ₂

orbyrossingoneofthe edgesofregion

P 2

^{. The rst ase is not possible sine itwould ontradit the hypothesis of}

non-rossing trajetory and in the seond ase the sequene

ee ^′

^{would not}

belongto the trajetory segment.

Remark. Note that for our purposes it is irrelevant whether property

P ₁

holds or not, sine it does not aet the niteness argument. This isdue to

0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000 0000000000000

1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111 1111111111111

000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000 000000000000

111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111 111111111111

x 1

x 2

e

P x ^′ ₁

e ^′ e ^′′

x ^′′ ₂

(a)

e ^l e

x 2

x 3

e ^u

(b)

P 2

x ^′′ ₂ e ^′′

e ^′

P 1

Figure12: (a): Simpleyle

s i

^anditsontinuationthroughedge

e

^{;(b) Edge}

e ^′

^{annot be reahed frompoint}

x 3

^withoutinterseting

x ₂ x ^′′

2

the fat that a type of signature is nite if the number of simple yles are

not repeated, whihis stated in

P ₂

.

In what follows we use the following notation. Whenever we partition the

spae into two regions

P L

^and

P R

^{by the line dened by a segment of line}

xy

^,

P L

^{is the semi-spae of all the points that are a left rotation of}

xy ~

^and

P R

^{isthe semi-spae} orresponding tothe pointsthat are a right rotationof

the samevetor. With

f(x) ↓

^wemeanthat

f

^{isdened at}

x

^and

f (x) ↑

^will

mean that

f

^{isundened at}

x

^.

Next we will(topologially)rephrase [Sh02 , Lemma 26℄and [Sh02 , Corol-

lary 27℄and we provethem both.

Lemma 6. Let

P

^{be a region,}

e ∈

^In

(P )

^,

e 1 , e 2 ∈

^Out

(P )

^,

hl i , u i i

^{be any}

subinterval of

he ^l _i , e ^u _i i

^and

f i (x) = F _e,e ^c _i (x)

^.

1. Let

P

^be partitioned into two regions

P L

^and

P R

^{by the line dened by}

xl 1

^{, then the following holds: if}

e 2 ∈ P L

^,

f 2 (x) ↓

^and

l 1 < f 1 (x)

^then

u 2 < f 2 (x)

^;

2. Let the plane be partitioned into two subspaes

P L

^and

P R

^{by the line}

denedby

xl 2

^{, thenthefollowingholds: if}

e 1 ∈ P R

^,

f 1 (x) ↓

^and

f 2 (x) <

u 2

^then

f 1 (x) < l 1

^.

Proof:

(a) (b)

b a b a

P

e x

f 2 (x)

e 1

e 2

l 2

u 2

u 1

A

l 1

f 1 (x)

P L

P R

P

e x

f 2 (x) ↑

e 1

u 1

l 1

f 1 (x)

P L

P R

e 2

u 2

l 2

Figure13: Lemma6'-1. (a) When

f 2 ^l (x) ↓

^{; (b) The ase}

f 2 ^l (x) ↑

^.

1. Remember that the line dened by

e 2

^{is ordered and that}

u 2

^,

A

^and

f 2 (x)

^{belongs to it. We have then that}

e 2 ∈ P L

^{(and hene}

u 2 ∈ P L

⁾

and that

f 2 (x) ∈ P R

^{(by onstrutionof the} partition). We have then that

u 2 < A

^and

A < f 2 (x)

^{, that implies}

u 2 < f 2 (x)

^{. See Fig. 13(a).}

2. This ase is symmetri tothe previous one.

Corollary 7. Let

P

^{bea region,}

e ∈

^In

(P )

^,

e 1 , e 2 ∈

^Out

(P )

^,

f i (x) = F _e,e ^c _i (x)

be anane funtionand

F i (hx, yi) = F i (hx, yi ∩ S i ) ∩J i

^{bea trunated ane}

multi-valued funtion (with

F i = [f _i ^l , f _i ^u ]

^and

J i = hL i , U i i

^).

1. Let

P

^be partitioned into two regions

P L

^and

P R

^{by the line dened}

by

xL 1

^{, then the following holds: If}

e 2 ∈ P L

^and

L 1 < f 1 ^l (x)

^then

F 2 (hx, yi) = ∅

^;

2. Let

P

^be partitioned into two regions

P L

^and

P R

^{by the line dened}

by

xL 2

^{, then the following holds: if}

e 1 ∈ P R

^and

f 2 ^u (y) < U 2

^then

F 1 (hx, yi) = ∅

^.

Proof:

1. If

f 2 ^l (x)

^{is undened, then it is obviousthat}

F 2 (hx, yi) = ∅

^{. If}

f 1 ^l (x)

^is

dened, thenthe resultfollowsdiretlyfromLemma6-1and denition

of

F i (hx, yi)

^.

2. Symmetri tothe above ase using Lemma 6-2.

6.2 Soundness of Exit-STAY and Exit-LEFT

Weprove nowsoundnessof theExit-STAYand Exit-LEFTalgorithmwhose

proofs rely onthe results proved in the previous setion.

Let

A = Succ ^b _s (L)

^{and onsider the linedened by}

AL

^{. This line partition}

the spaeinto

P L

^and

P R

^{as before.}

Exit-STAY

funtion

Exit ST AY (I, s, ex)

←− ∅

Soundness Byhypothesis,

L < l ^∗ < u ^∗ < U

^{. Hene, forall}

i

^,

I ˜ i = h ˜ l i , u ˜ i i ⊆ hL, U i

^{, hene}

I i = ˜ I i

^{and by Corollary7 we havethat}

Succ ⁱ _s,ex (I) = ∅

^.

Termination Trivial.

Exit-LEFT:

funtion

Exit LEF T (I, s, ex)

←− Succ _s,ex ( Succ _s,f (hL, max{u, u ^∗ }i))

Soundness By hypothesis,

l ^∗ < L < u ^∗ ≤ U

^{. Thus, there exists a natural}

number

n

^s.t.

l ˜ n ≤ L

^{and for all}

i

^,

u i = ˜ u i ≤ U

^{. Let's onsider the}

followingtwoases:

1. If

ex ∈ P R

^then

Ex = ∅

^{(bydenitionofExit-LEFT)and}

Succ _s,ex (I i ) =

∅

^forany

i

^{(byCorollary7-2),so}

Succ _s,ex ( Succ _s,f (hL, max{u, u ^∗ }i)) =

∅

^;

2. If

ex ∈ P L

^{, we onsider two ases:}

(a) If

u < u ^∗

^thenforall

i

^,

u i = ˜ u i ≤ u ^∗

^andthen

∪ m>0 Succ ^m _s,f (I) =

Succ _s,f (L, u ^∗ )

^{, thus}

Ex = Succ _s,ex (Succ s,f (L, u ^∗ ))

^;

(b) If

u ^∗ < u

^{then for all}

i

^,

u i = ˜ u i ≤ u

^and

∪ m>0 Succ ^m _s,f (I) = Succ _s,f (L, u)

^. Consequently,

Ex = Succ _s,ex (Succ s,f (L, u))

^;

Frombothaseswehavethat

Ex = Succ _s,ex (Succ s,f (hL, max{u, u ^∗ }i))

^.

Termination Trivial.

6.3 A semi-deision algorithm for reahability analysis

of GSPDIs

Fromthe aboveresultswehavethatthemainalgorithmforreahabilitymay

beapplied toGSPDIs after performingertain pre-proessing steps.

Before presentingasound (butinomplete)algorithmforreahabilityanaly-

sisof GSPDIsweneed thefollowingnotation. Given aGSPDI

H

^,wedenote

by

H red = {H 1 , . . . , H n }

^{the set of alltheSPDIs obtained afterxing allthe}

inout edges of

H

^{as inputs oroutputs, onsideringall the possible permuta-}

tions.

ThereahabilityalgorithmforaGSPDI

H

^,Reah

(H, x ₀ , x _f )

^{,onsistsofthe}

followingsteps:

1. Detet allthe inout edges;

2. Generate the set of SPDIs

H red = {H 1 , . . . , H n }

^;

3. Apply the reahability algorithmfor SPDIs to eah

H i

⁽

1 ≤ i ≤ n

^).

4. Ifthereexistsatleastone

H i ∈ H red

^suhthatReah

(H i , x ₀ , x _f ) = Yes

then Reah

(H, x ₀ , x _f ) = Yes

^{, otherwise we do not know.}

Wehave then the followingresult about termination of GSPDI reahability.

Lemma 8. Reah

(H, x ₀ , x _f )

^{always terminate.}

Proof: Theresult followsfromtheterminationofsteps 1and 2oftheabove

algorithm, as well as from that of Reah

(H i , x ₀ , x _f )

^{(for all}

H i ∈ H red

^,

1 ≤ i ≤ n

^).

Wenishthissetionwiththemainresultofourpaper,whihfollowsfromall

thepreviousresults,statingthatweansemi-deidereahabilityforGSPDIs.

Theorem 9. Given aGSPDI

H

^{, ifReah}

(H i , x ₀ , x _f ) = Yes

^forsome

H i ∈ H red

^{, then Reah}

(H, x ₀ , x _f ) = Yes

^{. On the other hand, if for all}

H i ∈ H red

^,

Reah

(H i , x ₀ , x _f ) = No

^{, then Reah}

(H, x ₀ , x _f )

^is inonlusive.

soundness of the algorithm for SPDIs [Sh02 , Se. 5.2℄, inluding the new

proofgiveninSetion6.2onsideringtheuseofnon-ontiguousentryandexit

edges. ThefatthatreahabilityisinonlusivewheneverReah

(H i , x ₀ , x _f ) = No

^{for all}

H i ∈ H red

^{follows from} Proposition2.

7 Final Disussion

In this work we have provided a ounter-example to aprevious proof of the

deidability of the reahability problem for GSPDIs given in [Sh02 , Chap.

9℄,whihremainthusanopen problem. Wehaverephrased theresultsgiven

in above mentioned work in order to give a semi-deidable algorithm for

solving the reahability problemfor suhlass of systems.

Referenes

[AMP95℄ E. Asarin, O. Maler, and A. Pnueli. Reahability analysis of

dynamial systems having pieewise-onstant derivatives. TCS,

138:3565,1995.

[AS02℄ E. Asarin and G. Shneider. Widening the boundary between de-

idable and undeidable hybrid systems. In CONCUR'2002, vol-

ume2421 ofLNCS, pages193208,Brno,CzehRepubli,August

2002.Springer-Verlag.

[ASY01℄ E. Asarin, G. Shneider, and S. Yovine. On the deidability

of the reahability problem for planar dierential inlusions. In

HSCC'2001, number 2034 in LNCS, pages 89104, Rome, Italy,

2001.Springer-Verlag.

[ASY07℄ Eugene Asarin, Gerardo Shneider, and Sergio Yovine. Algo-

rithmi Analysis of Polygonal Hybrid Systems. Part I: Reah-

ability. Theoretial Computer Siene, 379(1-2):231265, 2007.

doi:10.1016/j.ts.2007.03.055.

[HS74℄ MorrisW. Hirshand Stephen Smale. DierentialEquations, Dy-

namialSystems and Linear Algebra. Aademi Press In., 1974.

[MP93℄ O. Maler and A. Pnueli. Reahability analysis of planar multi-

linear systems. In CAV, number 697 in LNCS, pages 194209.

Springer-Verlag,1993.

frontier of hybrid automata. In FSTTCS, volume 3821 of LNCS,

pages 261272.Springer-Verlag,2005.

[NS60℄ V.V.NemytskiiandV.V. Stepanov. Qualitative theoryof dieren-

tialequations. Prineton University Press, 1960.

[Sh02℄ GerardoShneider. AlgorithmiAnalysisof PolygonalHybrid Sys-

tems. PhDthesis,VERIMAGUJF,Grenoble, Frane,July2002.

(a’)

e

(d') (d)

x 0 x 0

e

x _f x _f

(') ()

x 0

e e

x 0

(b') (b)

e

x _f x _f

e x 0

(a)

x 0

x _f x _f

e

e