Scribd
Upload
65 views

EL2450 Hybrid and Embedded Control: Lecture 12: Verification of Hybrid Systems

This document summarizes key concepts from Lecture 12 on verification of hybrid systems, including: - Bisimulations and language equivalence can be used to determine if transition systems have similar behavior. - Reachability analysis can determine the set of states that can be reached from the initial states of a hybrid automaton, and check if any "bad" states are reachable to verify safety properties. - The predecessor and successor operators are used to iteratively compute the reach set for hybrid automata by tracking states reachable through continuous evolution and discrete transitions.

Uploaded by

Nishant Batra
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
65 views

EL2450 Hybrid and Embedded Control: Lecture 12: Verification of Hybrid Systems

This document summarizes key concepts from Lecture 12 on verification of hybrid systems, including: - Bisimulations and language equivalence can be used to determine if transition systems have similar behavior. - Reachability analysis can determine the set of states that can be reached from the initial states of a hybrid automaton, and check if any "bad" states are reachable to verify safety properties. - The predecessor and successor operators are used to iteratively compute the reach set for hybrid automata by tracking states reachable through continuous evolution and discrete transitions.

Uploaded by

Nishant Batra
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 26

EL2450 Hybrid and Embedded Control

Lecture 12: Verification of hybrid systems

• Bisimulations of hybrid systems


• Languages of hybrid systems
• Reachability for hybrid automata

Lecture 12 1 January 9, 2014


Today’s Goal

You should be able to


• state when transitions systems are bisimilar
• state when transitions systems are language equivalent
• find a bisimulation quotient for a transition system
• do reachability analysis for hybrid automata

Lecture 12 2 January 9, 2014


Transition System with Initial and Final States

A transition system with the set of initial states S0 and the


set of final states SF is a tuple T = (S, Σ, →, S0 , SF ) where
• S is a set of states
• Σ is a set of generators
• →⊂ S × Σ × S is a transition relation
• S0 ⊆ S is a set of initial states
• SF ⊆ S is a set of final states

Lecture 12 3 January 9, 2014


Example

s0 b b
a s1
a a
a a
a
s1 s2 s2
b c b c b c
s3 s4 s6 s5 s4 s5

Figure 1: The transition systems T (left) and T (right).

• How formalize that T (left) and T (right) above have


similar behaviour?

Lecture 12 4 January 9, 2014


Language

A sequence w = σ1 σ2 . . . σn is a word produced by T if there


σ1 σ2 σn
exist transitions s1 −→ s2 −→ . . . sn −→ sn+1 , where s1 ∈ S0 ,
and sn+1 ∈ SF .
A language of T is

L(T ) = {w | w is a word produced by T }

Example
Find language of T in the previous example.

Lecture 12 5 January 9, 2014


Language Equivalence

T and T are language equivalent if L(T ) = L(T ).

Example
1. T and T in the previous example are language equivalent.
2. Add a transition labeled with a between q4 and q5 in T
and between p4 and p4 in T . They are not language
equivalent. Find a word w ∈ L(T ) \ L(T ).

Lecture 12 6 January 9, 2014


Relation

Given two sets A and B, a (binary) relation R from A to B


is a subset of A × B. We write a R b if (a, b) ∈ R.

Example
= is a relation from N to N.

Lecture 12 7 January 9, 2014


Simulation Relation
Given transition systems T = (S, Σ, →, S0 , SF ) and
T = (S , Σ, → , S0 , SF ). A relation ∼⊂ S × S is a
simulation relation if
1. ∀s ∈ S0 (∃s ∈ S0 . s ∼ s )
2. s ∼ s ∧ s ∈ SF ⇒ s ∈ SF
σ σ
3. s ∼ s ∧ s → r ⇒ ∃r ∈ S such that s → r and r ∼ r
We say that T simulates T
Example
Derive a simulation relation for T and T in the previous
example

Lecture 12 8 January 9, 2014


Bisimulation Relation

If ∼ is a simulation relation from T to T and


∼ = {(s , s) : (s, s ) ∈∼} is a simulation relations from T to
T , then ∼ is a bisimulation relation.

• The existence of a bisimulation relation between two


transition systems indicates that they are equivalent in
some sense
• We say that T and T are bisimular

Lecture 12 9 January 9, 2014


Examples: Bisimulation Relation

1. T and T in the previous example are bisimular

2. Add a transition labeled with a between q4 and q5 in T


and between p4 and p4 in T .
Then T and T are not bisimular, because T simulates T but
T does not simulate T

Lecture 12 10 January 9, 2014


Language Equivalence vs. Bisimulation
Bisimulation ⇒ language equivalence
Language equivalence ⇒ bisimulation
Example

s0 s0

a a a
s1 s1
s1

c b c
b

s2 s3 s2 s3

Lecture 12 11 January 9, 2014


Equivalence Relation

A relation ∼⊂ S × S is an equivalence relation if for all


s, s , s ∈ S
1. s ∼ s (reflexive)
2. s ∼ s ⇒ s ∼ s (symmetric)
3. s ∼ s and s ∼ s ⇒ s ∼ s (transitive)

Example
= is an equivalence relation

Lecture 12 12 January 9, 2014


Equivalence Class

Let ∼⊂ S × S be an equivalence relation. The equivalence


class of r ∈ S is defined as [r] = {s ∈ S | s ∼ r}.

Note
The equivalence classes constitutes a partition of S, i.e., a

collection of states S/∼ = {Si }i∈I such that

Si ∩ Sj = ∅, i = j

and

Si = S
i∈I

Lecture 12 13 January 9, 2014


Quotient Transition System

Given a transition system T = (S, Σ, →, S0 , SF ) and a


partition {Si }i∈I , the quotient transition system
T̂ = (Ŝ, Σ, →,
ˆ Ŝ0 , ŜF ) is defined as

1. Ŝ = {Si }i∈I
σ σ
ˆ ŝ if ∃s, s ∈ S,s ∈ ŝ, s ∈ ŝ , s → s
2. ŝ →

3. ŝ ∈ Ŝ0 if ∃s ∈ ŝ, s ∈ S0
4. ŝ ∈ ŜF if ∃s ∈ ŝ, s ∈ SF

Can we find a finite partition such that T and T̂ are bisimular?

Lecture 12 14 January 9, 2014


Quotient Transition System

The equivalence relation is a bisimulation when


• SF is a union of equivalence classes.
• For each P ⊆ S that is a union of equivalence classes,
Pre(P ) is a union of equivalence classes.
• Thus, if T and T̂ are bisimular, all the information related
to T can be derived from the evolution in T̂ !

Lecture 12 15 January 9, 2014


Bisimulation Quotient Algorithm

1. initialize S/∼ = {s | s ∈ S ⊆ SF }, {s | s ∈ SF }
2. while ∃P, P ∈ S/∼ , σ ∈ Σ, s.t. ∅ = P ∩ P reσ (P ) = P
P1 := P ∩ P reσ (P )
P2 := P \ P reσ (P )
S/∼ := (S/∼ \ {P }) ∪ {P1 , P2 }
endwhile

If the algorithm terminates, it computes the coarsest quotient.


If T is infinite, the algorithm is not guaranteed to terminate.

Lecture 12 16 January 9, 2014


Verification

• Prove that a system fulfill certain property


• Based on a mathematical model and a computational tool

Lecture 12 17 January 9, 2014


Hybrid Automaton as a Transition System
A hybrid automaton is a transition system TH = (S, Σ, →, S0 = Init)
with interacting event-driven and time-driven evolution:
• S = Q × X and (q, x) ∈ S denotes the state
• Σ = {g} ∪ Time where the generators {g} causes the jumps and
Time the continuous evolution
• (q, x) → (q , x ) defines the event-driven and time-driven transitions
Example: S = Q × X, with Q = {q1 , q2 } and X = R,
Σ = {g1 , g2 } ∪ Time, g1 corresponds to the event x > 1 and g2 to
x < −1, S0 = Init = {(q1 , x) | x ≥ 0}
x>1

q1 q2
ẋ = 1 ẋ = −1

x < −1

Lecture 12 18 January 9, 2014


Reach Set

Reach(S0 ) is the set of states that can be reached from S0 by


a sequence of transitions, i.e.,

Reach(S0 ) = Postk (S0 )
k=0,1,...

Lecture 12 19 January 9, 2014


Safety

For a transition system T = (S, Σ, →, S0 ), let B ⊂ S denote


a “bad” set, i.e., a set of states that we don’t want the
system to enter. T is safe if

Reach(S0 ) ∩ B = ∅

Remark
• B encodes the property to verify
• Verification is about verifying that the system fulfills its
specification, i.e., Reach(S0 ) ∩ B = ∅

Lecture 12 20 January 9, 2014


Pre and Post for Hybrid Automata
The predecessor operator Pre(P ), P ⊂ S for a hybrid automaton is
t e
Pre(P ) = {(qp , xp ) : ∃(q, x) ∈ P, (qp , xp ) → (q, x) or (qp , xp ) → (q, x)}

The successor operator Post(P ) for a hybrid automaton is


t e
Post(P ) = {(qp , xp ) : ∃(q, x) ∈ P, (q, x) → (qp , xp ) or (q, x) → (qp , xp )}

The Preσ (P ) and P ostσ (P ) are


σ
Preσ (P ) = {(qp , xp ) : ∃(q, x) ∈ P, (qp , xp ) → (q, x)}

σ
Postσ (P ) = {(qp , xp ) : ∃(q, x) ∈ P, (q, x) → (qp , xp )}

Lecture 12 21 January 9, 2014


Reach Set for Hybrid Automata

ReachH (S0 ) ⊂ Q × X is the set of states that can be reached


by a solution of H from S0 , i.e.,

(q̄, x̄) ∈ ReachH (S0 )

if and only if there exists a solution χ = (τ, q, x) of H such


that
• (q(t), x(t)) = (q̄, x̄) for some t ∈ [τi , τi ) ∈ τ , and
• (q(0), x(0)) ∈ S0

Lecture 12 22 January 9, 2014


Reach Set Computations for Hybrid Automata

• If the hybrid automaton has a finite bisimilar quotient


transition system, then the Reachability Algorithm (ref.
Lec. 9) terminates in a finite number of steps.
• This is done by applying the algorithm to the finite
quotient system.
• Which classes of hybrid systems admit a finite bisimilar
quotient transition system?

Lecture 12 23 January 9, 2014


Property of Quotient Transition Systems

• For finite state systems an algorithm that always finds the


coarsest bisimilar quotient system exists and always
terminates
• For time-triggered continuous-time systems (and hybrid
systems) we cannot always find a finite partition
• Even if a transition system has infinite state space, its
corresponding quotient transition system can be finite

Lecture 12 24 January 9, 2014


Beyond Reachability Verification

• More complex properties can be expressed and verified


• Verification of bisimulation between a system and its
specification
• Requirements on language can be expressed e.g. in
temporal logics

Lecture 12 25 January 9, 2014


Next Lecture

• Reachability for timed automata, multi-rate automata,


rectangular automata
• Over-approximations

Lecture 12 26 January 9, 2014

You might also like