Dynamical Systems

A. Trivedi – 1 of 24

CS620, IIT BOMBAY

An Introduction to Hybrid Systems Modeling

Ashutosh Trivedi

Department of Computer Science and Engineering, IIT Bombay

CS620: New Trends in IT: Modeling and Verification of Cyber-Physical Systems (2 August 2013)

Dynamical Systems

Dynamical System: A system whosestateevolves withtimegoverned by a fixed set ofrulesordynamics.

– state: valuation to variables (discrete or continuous) of the system – time: discrete or continuous

– dynamics: discrete, continuous, or hybrid

Discrete System Continuous System Hybrid Systems.

A. Trivedi – 2 of 24

Dynamical Systems

Dynamical System: A system whosestateevolves withtimegoverned by a fixed set ofrulesordynamics.

– state: valuation to variables (discrete or continuous) of the system – time: discrete or continuous

– dynamics: discrete, continuous, or hybrid

Discrete System Continuous System Hybrid Systems.

Discrete Dynamical Systems

Continuous Dynamical Systems

Hybrid Dynamical Systems

A. Trivedi – 4 of 24

Abstract Model for Dynamical Systems

Definition (State Transition Systems)

A state transition system is a tupleT = (S, S0,Σ,∆)where:

– S is a (potentially infinite) set ofstates;

– S0⊆S is the set ofinitial states;

– Σis a (potentially infinite) set ofactions; and – ∆⊆S×Σ×S is thetransition relation;

count, 0

start count, 1 count,2 count,3

pause, 0 pause, 1 pause,2 pause,3

tick pause

start tick

tick pause

start tick

tick pause

start tick

tick

pause start tick

Abstract Model for Dynamical Systems

Definition (State Transition Systems)

A state transition system is a tupleT = (S, S0,Σ,∆)where:

– S is a (potentially infinite) set ofstates;

– S0⊆S is the set ofinitial states;

– Σis a (potentially infinite) set ofactions; and – ∆⊆S×Σ×S is thetransition relation;

count,0

start count, 1 count, 2 count,3

pause, 0 pause, 1 pause, 2 pause,3

tick pause

start tick

tick pause

start tick

tick pause

start tick

tick

pause start tick

A. Trivedi – 5 of 24

State Transition Systems

Definition (State Transition Systems)

A state transition system is a tupleT = (S, S₀,Σ,∆)where:

– S is a (potentially infinite) set ofstates;

– S0⊆S is the set ofinitial states;

– Σis a (potentially infinite) set ofactions; and – ∆⊆S×Σ×S is thetransition relation;

– Finite and countable state transition systems – Afinite runis a sequence

hs0, a1, s1, s2, s2, . . . , sni

such thats0∈S0and for all0≤i < nwe have that(si, ai+1, si+1)∈∆.

– ReachabilityandSafe-Schedulabilityproblems

We need efficient computer-readable representations of infinite systems!

State Transition Systems

Definition (State Transition Systems)

A state transition system is a tupleT = (S, S₀,Σ,∆)where:

– S is a (potentially infinite) set ofstates;

– S0⊆S is the set ofinitial states;

– Σis a (potentially infinite) set ofactions; and – ∆⊆S×Σ×S is thetransition relation;

– Finite and countable state transition systems – Afinite runis a sequence

hs0, a1, s1, s2, s2, . . . , sni

such thats0∈S0and for all0≤i < nwe have that(si, ai+1, si+1)∈∆.

– ReachabilityandSafe-Schedulabilityproblems

We need efficient computer-readable representations of infinite systems!

A. Trivedi – 6 of 24

Extended Finite State Machines

– LetX be the set of variables(real-valued) of the system – let|X|=N.

– Avaluationν ofX is a function ν:X →R.

– We consider a valuation as a point inR^N equipped withEuclidean Norm.

– Apredicateis defined simply as a subset ofR^N represented (non-linear) algebraic equations involvingX.

– Non-linear predicates, e.g. x+ 9.8 sin(z) = 0 – Polyhedral predicates:

a1x1+a2x2+· · ·+anxn∼k

whereai∈R,xi∈X, and∼={<,≤,=,≥, >}.

– Octagonal predicates

xi−xj∼korxi∼k wherexi, xj∈X, and∼={<,≤,=,≥, >}.

– Rectangular predicates

xi∼k wherexi∈X, and∼={<,≤,=,≥, >}.

– Singular Predicatesxi=c.

Extended Finite State Machines

count

start >, pause,x⁰=x pause

x<3, tick,x⁰=x+ 1

x=3, tick,x⁰=0

>, start,x⁰=x >, tick,x⁰=x

Extended Finite State Machines (EFSMs):

– Finite state-transition systems coupled with afinite set of variables – The valuation remains unchanged while system stays in a mode (state) – The valuation changes during a transition when itjumpsto the valuation

governed by a predicate overX∪X⁰ specified in the transition relation.

– Transitions areguarded by predicates overX – Mode invariants

– Initial stateandvaluation

A. Trivedi – 8 of 24

Extended Finite State Machines

count

start >, pause,x⁰=x pause

x<3, tick,x⁰=x+ 1

x=3, tick,x⁰=0

>, start,x⁰=x >, tick,x⁰=x

Definition (EFSM: Syntax)

Anextended finite state machineis a tupleM= (M, M0,Σ, X,∆, I, V0)such that:

– M is a finite set of controlmodesincluding a distinguished initial set of control modesM₀⊆M,

– Σis a finite set ofactions,

– X is a finite set of real-valuedvariable,

– ∆⊆M ×pred(X)×Σ×pred(X∪X⁰)×M is thetransition relation, – I:M →pred(X)is the mode-invariant function, and

– V₀∈pred(X)is the set of initial valuations.

EFSM: Semantics

count

start >, pause,x⁰=x pause

x<3, tick,x⁰=x+ 1

x=3, tick,x⁰=0

>, start,x⁰=x >, tick,x⁰=x

count,0

start count, 1 count, 2 count,3

pause, 0 pause, 1 pause, 2 pause,3

tick pause

start tick

tick pause

start tick

tick pause

start tick

tick

pause start tick

A. Trivedi – 10 of 24

EFSM: Semantics

Thesemantics of an EFSMM= (M, M0,Σ, X,∆, I, V0)is given as astate transition graphT^M= (S^M, S₀^M,Σ^M,∆^M)where

– S^M⊆(M ×R^|X|)is the set ofconfigurations ofMsuch that for all (m, ν)∈S^M we have thatν ∈JI(m)K;

– S₀^M⊆S^Mis the set ofinitial configurationssuch that(m, ν)∈S^M if m∈M₀andν∈V₀;

– Σ^M= Σis the set oflabels;

– ∆^M⊆S^M×Σ^M×S^M is the set oftransitionssuch that ((m, ν), a,(m⁰, ν⁰))∈∆^M if there exists a transition δ= (m, g, a, j, m⁰)∈∆such that

– current valuation satisfies the guardν∈JgK;

– current and next valuations satisfy the jump constraint(ν, ν⁰)∈JjK; and – next valuation satisfies the invariant of the target modeν⁰∈JI(m⁰)K.

Discrete Dynamical Systems

Continuous Dynamical Systems

Hybrid Dynamical Systems

A. Trivedi – 12 of 24

Continuous Dynamical Systems

– Afiniteset ofcontinuous variables,

– a set ofordinary differential equations(ODE) characterizing theflowof these variables as a function of time

– F: ˙X→pred(X)wherex˙ is thefirst derivativeofx.

– Higher-order derivativescan be written using first derivatives by introducing auxiliary variables, e.g. writeθ¨+ (g/`) sin(θ) = 0can be written as

θ˙=yandy˙=−(g/`) sin(θ).

– aninitial valuationto the variables.

Definition (Continuous Dynamical System)

Acontinuous dynamical systemis a tupleM= (X, F, ν0)such that – X is a finiteset of real-valuedvariable,

– F : ˙X →pred(X)is the flow function, and – ν0∈R^|X|is the initial valuation.

Continuous Dynamical Systems

– Afiniteset ofcontinuous variables,

– a set ofordinary differential equations(ODE) characterizing theflowof these variables as a function of time

– F: ˙X→pred(X)wherex˙ is thefirst derivativeofx.

– Higher-order derivativescan be written using first derivatives by introducing auxiliary variables, e.g. writeθ¨+ (g/`) sin(θ) = 0can be written as

θ˙=yandy˙=−(g/`) sin(θ).

– aninitial valuationto the variables.

Definition (Continuous Dynamical System)

Acontinuous dynamical systemis a tupleM= (X, F, ν0)such that – X is a finiteset of real-valuedvariable,

– F : ˙X →pred(X)is the flow function, and – ν0∈R^|X|is the initial valuation.

A. Trivedi – 13 of 24

Continuous Dynamical Systems

Definition (Continuous Dynamical System)

Acontinuous dynamical systemis a tupleM= (X, F, ν₀)such that – X is a finiteset of real-valuedvariable,

– F : ˙X →pred(X)is the flow function, and – ν0∈R^|X|is the initial valuation.

– Arunor a trajectoryofM= (X, F, ν₀)is given as a solution to the differential equationsX˙ =F(X)with initial valuationν₀.

– Let a differentiable functionf :R_≥0→R^|X|be a solution toX˙ =F(X) that provides the valuations of the variables as a function of time:

f(0) = ν0

f˙(t) = F(f(t))for everyt∈R_≥0, wheref˙:R≥0→R|X|is the time derivative of the functionf. – a run of a continuous dynamical systemmay not exist or may not be

unique!

Existence and Uniqueness

Definition (Lipschitz-continuous Function)

We say that a functionF :Rⁿ→Rⁿ is Lipschitz-continuous if there exists a constantK>0, called the Lipschitz constant, such that for allx, y∈Rⁿ we have thatkF(x)−F(y)k< Kkx−yk.

Theorem (Picard-Lindel¨ of Theorem)

If a functionF:R^|X|→R^|X|is Lipschitz-continuous then the differential equationX˙=F(X)with initial valuationν0∈R^|X| has a unique solution f :R_≥0→R^|X|for allν0∈R^|X|.

Theorem (Stability wrt initial valuation)

LetF be a Lipschitz-continuous function with constantK>0and let f:R_≥0→R^|X| andf⁰:R_≥0→R^|X|be solutions to the differential equation X=F˙ (X)with initial valuationν₀∈R^|X|andν₀⁰∈R^|X|, respectively. Then, for allt∈R_≥0 we have thatkf(t)−f⁰(t)k ≤ kν−ν0ke^Kt.

A. Trivedi – 14 of 24

Existence and Uniqueness

Definition (Lipschitz-continuous Function)

We say that a functionF :Rⁿ→Rⁿ is Lipschitz-continuous if there exists a constantK>0, called the Lipschitz constant, such that for allx, y∈Rⁿ we have thatkF(x)−F(y)k< Kkx−yk.

Theorem (Picard-Lindel¨ of Theorem)

If a functionF:R^|X|→R^|X|is Lipschitz-continuous then the differential equationX˙=F(X)with initial valuationν0∈R^|X|has a unique solution f :R_≥0→R^|X|for allν0∈R^|X|.

Theorem (Stability wrt initial valuation)

LetF be a Lipschitz-continuous function with constantK>0and let f:R_≥0→R^|X| andf⁰:R_≥0→R^|X|be solutions to the differential equation X=F˙ (X)with initial valuationν₀∈R^|X|andν₀⁰∈R^|X|, respectively. Then, for allt∈R_≥0 we have thatkf(t)−f⁰(t)k ≤ kν−ν0ke^Kt.

Existence and Uniqueness

Definition (Lipschitz-continuous Function)

We say that a functionF :Rⁿ→Rⁿ is Lipschitz-continuous if there exists a constantK>0, called the Lipschitz constant, such that for allx, y∈Rⁿ we have thatkF(x)−F(y)k< Kkx−yk.

Theorem (Picard-Lindel¨ of Theorem)

If a functionF:R^|X|→R^|X|is Lipschitz-continuous then the differential equationX˙=F(X)with initial valuationν0∈R^|X|has a unique solution f :R_≥0→R^|X|for allν0∈R^|X|.

Theorem (Stability wrt initial valuation)

LetF be a Lipschitz-continuous function with constantK>0and let f:R_≥0→R^|X|andf⁰:R_≥0→R^|X|be solutions to the differential equation X=F˙ (X)with initial valuationν₀∈R^|X|andν₀⁰∈R^|X|, respectively. Then, for allt∈R_≥0 we have thatkf(t)−f⁰(t)k ≤ kν−ν₀ke^Kt.

A. Trivedi – 15 of 24

Example: Simple Pendulum

θ

mg m`²θ¨

`

– Variablesyandθ

– flow equations: m`<sup>2</sup>θ¨=−mg`sin(θ), or θ˙ = y,

˙

y = −(g/`) sin(θ), – initial valuations(θ, y) = (θ₀,0).

Simple Pendulum

– To analytically solve these equations, assume that initial angular displacementθ is small.

– hencesin(θ)≈θ.

– Now the equations simplify to

θ˙=y andy˙=−(g/`)θ.

– The solution for these differential equations is θ(t) = Acos(Kt) +Bsin(Kt) y(t) = −AKsin(Kt) +BKcos(Kt),

whereK=p g/`.

– Substitutingθ(0) =θ₀ andy(0) = 0 from the initial valuation, we get thatA=θ₀andB= 0.

– The unique run of the pendulum system can be given as the function f :R≥0→ {θ, y} as

t7→(θ₀cos(Kt),−θ₀Ksin(Kt)).

A. Trivedi – 17 of 24

Pendulum Motion

0 2 4 6 8 10

−10 0 10

t(in seconds)7→

θ(indegrees)andy(indegrees/second)7→

θ0cos((p g/`)t)

−θ0

pg/`sin((p g/`)t)

(b)

Discrete Dynamical Systems

Continuous Dynamical Systems

Hybrid Dynamical Systems

A. Trivedi – 19 of 24

Another example: Bouncing Ball

Bouncing Ball

– Consider abouncing ball systemdropped from height`and velocity0.

– Is it a continuous system?

– variables of interest: height of the ballx₁and velocity of the ball x₂ – flow function:

˙

x1=x2 andx˙2=−g – What happens at impact?

– x⁰₁=x1andx⁰₂=−cx2where cisRestituition coefficient.

˙ x1=x2,

˙ x2=−g m start

x1≥0 x1=0∧x2≤0,

impact x⁰1=x1∧x⁰2=−cx2

Another example: Bouncing Ball

Bouncing Ball

– Consider abouncing ball systemdropped from height`and velocity0.

– Is it a continuous system?

– variables of interest: height of the ballx₁and velocity of the ball x₂ – flow function:

˙

x1=x2 andx˙2=−g – What happens at impact?

– x⁰₁=x1andx⁰₂=−cx2where cisRestituition coefficient.

˙ x1=x2,

˙ x2=−g m start

x1≥0 x1=0∧x2≤0,

impact x⁰1=x1∧x⁰2=−cx2

A. Trivedi – 19 of 24

Another example: Bouncing Ball

Bouncing Ball

– Consider abouncing ball systemdropped from height`and velocity0.

– Is it a continuous system?

– variables of interest: height of the ballx₁and velocity of the ball x₂ – flow function:

˙

x1=x2 andx˙2=−g – What happens at impact?

– x⁰₁=x1andx⁰₂=−cx2where cisRestituition coefficient.

˙ x1=x2,

˙ x2=−g m start

x1≥0 x1=0∧x2≤0,

impact x⁰1=x1∧x⁰2=−cx2

Another example: Bouncing Ball

Bouncing Ball

– Consider abouncing ball systemdropped from height`and velocity0.

– Is it a continuous system?

– variables of interest: height of the ballx₁and velocity of the ball x₂ – flow function:

˙

x1=x2 andx˙2=−g – What happens at impact?

– x⁰₁=x1 andx⁰₂=−cx2where cisRestituition coefficient.

˙ x1=x2,

˙ x2=−g m start

x1≥0 x1=0∧x2≤0,

impact x⁰1=x1∧x⁰2=−cx2

A. Trivedi – 19 of 24

Another example: Bouncing Ball

Bouncing Ball

– Consider abouncing ball systemdropped from height`and velocity0.

– Is it a continuous system?

– variables of interest: height of the ballx₁and velocity of the ball x₂ – flow function:

˙

x1=x2 andx˙2=−g – What happens at impact?

– x⁰₁=x1 andx⁰₂=−cx2where cisRestituition coefficient.

˙ x1=x2,

˙ x2=−g m start

x1≥0 x1=0∧x2≤0,

impact x⁰1=x1∧x⁰2=−cx2

Discrete, Continuous, and Hybrid Systems

0 1 2 3 4 5

1 2 3 4

t

X

Discrete System

0 2 4 6 8 10

−1

−0.5 0 0.5 1

t

X

Continuous System

0 2 4 6 8 10

−1 0 1 2 3

t

X

Hybrid System

A. Trivedi – 21 of 24

Hybrid Automata: Syntax

Some examples:

– Two leaking-water tanks systems – Water-level monitor with delayed switch – A leaking gas-burner

– Green scheduling with lower dwell-time requirements – Light-bulb with three modes- dim, bright, and off.

– Job-shop scheduling problem

Login Protocol

start

start valid

delay error conn

user name,x:=0 restart, x >60

restart, x≥10

x:=0

pw fail,

x <60 pw match, x <60

A. Trivedi – 23 of 24

Hybrid Automata: Syntax

Definition (HA: Syntax)

A hybrid automaton is a tupleH= (M, M0,Σ, X,∆, I, F, V0)where:

– M is a finite set of controlmodesincluding a distinguished initial set of control modesM0⊆M,

– Σis a finite set ofactions,

– X is a finite set of real-valuedvariable,

– ∆⊆M ×pred(X)×Σ×pred(X∪X⁰)×M is thetransition relation, – I:M →pred(X)is the mode-invariant function,

– F :M →( ˙X →pred(X))is the mode-dependent flow function, and – V₀∈pred(X)is the set of initial valuations.

– Aconfiguration(m, ν)and atimed action(t, a) – Atransition((m, ν),(t, a),(m⁰, ν⁰)

– solve flow ODE of modemwithνas the starting stateν⊕F(m)t. – invariant, guard, and jump conditions.

– Arunorexecutionis a sequence of transitions

(m0, ν0),(t1, a1),(m1, ν1),(t2, a2). . .

Hybrid Automata: Syntax

Definition (HA: Syntax)

A hybrid automaton is a tupleH= (M, M0,Σ, X,∆, I, F, V0)where:

– M is a finite set of controlmodesincluding a distinguished initial set of control modesM0⊆M,

– Σis a finite set ofactions,

– X is a finite set of real-valuedvariable,

– ∆⊆M ×pred(X)×Σ×pred(X∪X⁰)×M is thetransition relation, – I:M →pred(X)is the mode-invariant function,

– F :M →( ˙X →pred(X))is the mode-dependent flow function, and – V₀∈pred(X)is the set of initial valuations.

– Aconfiguration(m, ν)and atimed action(t, a) – Atransition((m, ν),(t, a),(m⁰, ν⁰)

– solve flow ODE of modemwithνas the starting stateν⊕F(m)t.

– invariant, guard, and jump conditions.

– Arunorexecutionis a sequence of transitions

(m0, ν0),(t1, a1),(m1, ν1),(t2, a2). . .

A. Trivedi – 24 of 24

Hybrid Automata: Semantics

Definition (HA: Semantics)

The semantics of a HAH= (M, M₀,Σ, X,∆, I, F, V₀)is given as a state transition graphT^H= (S^H, S₀^H,Σ^H,∆^H)where

– S^H⊆(M×R^|X|)is the set of configurations ofHsuch that for all (m, ν)∈S^H we have thatν ∈JI(m)K;

– S₀^H⊆S^H s.t. (m, ν)∈S₀^H ifm∈M₀andν ∈V₀; – Σ^H=R≥0×Σis the set of labels;

– ∆^H⊆S^H×Σ^H×S^H is the set of transitions such that ((m, ν),(t, a),(m⁰, ν⁰))∈∆^H if there exists a transition δ= (m, g, a, j, m⁰)∈∆such that

– (ν⊕F(m)t)∈JgK;

– (ν⊕F(m)τ)∈JI(m)Kfor allτ∈[0, t];

– ν⁰∈(ν⊕F(m)t)[j]; and – ν⁰∈JI(m⁰)K.