Hybrid Automata

Information about Hybrid Automata

Published on November 8, 2007

Author: Crystal

Source: authorstream.com

Content

Introduction to Hybrid Automata:  Introduction to Hybrid Automata Arijit Mondal Kapil Modi Arnab Sinha Introduction:  Introduction A hybrid automaton is a formal model for a mixed discrete continuous system. Systems with ‘discrete jumps’ & ‘continuous flow’ can be modeled into Hybrid Automata. Bouncing Ball Example: Here, the following properties hold: Bouncing Ball: Properties:  Bouncing Ball: Properties States: In air (Assumption: Rebound time is negligible) Continuous Variable: height (h), velocity (v) Guard Condition : height=0, velocity=negative. Effect (Reset Map): velocity changes due to restitution coefficient (e) We are ready for the Model !!! Bouncing Ball Model::  Bouncing Ball Model: State Continuous variables Guard Condition Reset condition Domain (Fly) An Illustration: Water Tank Problem :  An Illustration: Water Tank Problem Water Tank: Properties:  Water Tank: Properties The supplier can supply water at a rate of w to only one reservoir at a time. [Discrete Behavior] The current levels are x1 and x2 respectively. [Continuous Variables] The minimum threshold to be maintained are r1 and r2 respectively. [Guard Conditions] It is assumed that while transition between reservoirs none of the level changes. [Reset Property] Hence we can model it with Hybrid Automata!!! Water Tank Problem:  Water Tank Problem Guard Condition Reset Property state Continuous variables Domain(q1) Domain(q2) The Automaton:  The Automaton Where, Q = set of discrete states. X = set of continuous variables, Where, E is the set of edges. G is the guard condition, and, R is the Reset Map An Illustration: Water Tank Problem :  An Illustration: Water Tank Problem Water Tank Problem: Formal Model:  Water Tank Problem: Formal Model Water Tank Problem: Formal Model (Contd.):  Water Tank Problem: Formal Model (Contd.) Water Tank Problem:  Water Tank Problem Hybrid time set:  Hybrid time set It is a sequence of finite or infinite intervals such that Bouncing Ball: Hybrid time-set:  Bouncing Ball: Hybrid time-set The bouncing ball: The first half is upward movement and the next half is downwards. The first run is interval and the next run is in and so on. Hybrid Trajectory (t, q, x):  Hybrid Trajectory (t, q, x) A hybrid trajectory is a triple (t, q, x) consisting of a hybrid time set, t and two sequences of functions q and x such that Hybrid Execution:  Hybrid Execution An execution of a hybrid automation H is hybrid trajectory, (t, q, x), which satisfies the following conditions. Initial condition: Discrete evolution: Hybrid Execution (contd.):  Hybrid Execution (contd.) Continuous evolution: such that is the solution to the diff. equation over starting at Water Tank Problem: Hybrid Execution:  Water Tank Problem: Hybrid Execution Water Tank Problem: Hybrid Execution (Contd.):  Water Tank Problem: Hybrid Execution (Contd.) Initial Condition Discrete Evolution Water Tank Problem: Hybrid Execution (Contd.):  Water Tank Problem: Hybrid Execution (Contd.) Continuous Evolution Classification of Executions:  Classification of Executions Finite, if t is a finite sequence and the last interval in t is closed. Infinite, if t is a infinite sequence, or if, Zeno, if it is infinite but the sum of intervals is finite. Real life designs are mostly non-zeno i.e. time-diverging e.g. bouncing ball system. Maximal, if it is not a strict prefix of any other execution of H. 0-Transition:  0-Transition We know, Hence we define an event which triggers transition iff there exists an edge e= (q, q’) such that for some , Hence we can say for all states q, of a hybrid automaton i.e. we can always construct an edge such that 0 Composition of Automata:  Composition of Automata For two hybrid automata, and then we can define the semantics of parallel composition as But for composition, the transitions have to be consistent. The transitions, and are consistent if any of the following three conditions are true, and . and . Composition: Water Tank Model:  Composition: Water Tank Model We develop two independent models of the 2 reservoirs. 0 0 holds when water is supplied to tank 1. Composition: Water Tank Model:  Composition: Water Tank Model The complete model. Example: Buck Converter:  Example: Buck Converter Buck converter driving variable load Switch S1 remain on for 6 secs and off for 4 secs Switch S2 alternate between R1 and R2 in every 4 secs Discrete states and State variables:  Discrete states and State variables Four discrete states S1 on and S2—R1 (A) S1 on and S2—R2 (B) S1 off and S2—R2 (C) S1 off and S2—R1 (D) For circuit dynamics: Current through inductor (i) Voltage across capacitor (v) Clock variables: S1: denotes the duration of on/off state of switch S1 S2: denotes the duration of connection of switch S2 with R1 or R2 Dynamic activities:  Dynamic activities For states (A) and (B) For states (C) and (D) For clock variable S1 and S2 for all locations Hybrid model of Buck converter:  Hybrid model of Buck converter Example (Buck converter) [Santosh]:  Example (Buck converter) [Santosh] Descriptions:  Descriptions Zero pulse – Generates –ve square pulse when input crosses zero volt from any +ve voltage Monoshot – Generates +ve square pulse with Ton and it is triggered by a –ve edge at the input. Startup pulse – Generates –ve pulse to trigger the monoshot. Zero crossing detector – It toggles output when the input crosses zero volt. Initial output logic zero. Drivers – To drive power MOS switches. Hysteresis comparator:  Hysteresis comparator Outputs logic high if input is below threshold Outputs logic low if input is above threshold Vin Vout Determination of discrete states:  Determination of discrete states This systems can be modeled as hybrid system and dynamics behavior of each state depends on the following State of PMOS State of NMOS Control signal to PMOS Control signal to NMOS Dynamic behavior of each state will depend on the following: Vcx : PMOS drain voltage Vout : Output voltage Hybrid automata:  Hybrid automata Linear hybrid systems (LHS):  Linear hybrid systems (LHS) For all locations activity (vector field) can be defined as follows: For all locations invariant (domain) is defined by a linear formula over continuous states (X). For all transitions, guarded set of nondeterministic assgn. Example:  Example (x+y>4)→{x:=[3x+y,2y], y:=[7,5x]} v(αx)=21 v(βx)=24 x=3 y=12 x=23 y=9 v(αy)=7 v(βy)=15 v:(x=3,y=12) Special cases:  Special cases Discrete variable Discrete system – All variable are discrete variable Proposition – x is discrete variable and Clock Special cases (contd.):  Special cases (contd.) Timed automaton – Linear hybrid system all of whose variables are propositions or clocks and linear expression are Boolean combination of inequalities. (x#c or x-y#c) Skewed clock: Multirate timed system – LHS whose variables are propositions and skewed clocks n-rate timed system – Multirate timed system whose skewed clocks proceed at n different rates Special cases (contd.):  Special cases (contd.) Integrator Parameter - x discrete variable Simple LHS – Domains (invariants) and Guards are of the form x≤k or x≥k Reachability results:  Reachability results The reachability problem is decidable for simple multirate timed system. The reachability problem is undecidable for 2-rate timed system. The reachability problem is undecidable for simple integrator systems Verification of Hybrid Automata:  Verification of Hybrid Automata A hybrid automata specification can be encoded as a set of desirable hybrid trajectories, H. The given model is said to meet the given specification if the set of execution of the model is a subset of H. Safety Property:- where F is the set of safe states in which we wish to remain always. Liveness Property:- where T is the set of states in which we visit eventually. Example:  Example Say we model a traffic system with a hybrid automata, then the set of safe states F, are those, in which no two cars collide. Set of live states T, are those, in which the cars eventually reach their destination. Transition System from a hybrid automaton:  Transition System from a hybrid automaton H = (Q, X, Init, f, Dom, E, G, R) be a hybrid automaton with a distinguished set of final states, F, S: set of states (finite or infinite) A transition relation A set of initial states A set of final states Hybrid Automata transformed into a transition system. Transition System from a hybrid automaton (contd.):  Transition System from a hybrid automaton (contd.) The transition relation can be divided into a discrete transition relation and a continuous transition relation. For each edge, For the continuous transition relation, Where, x(.) is the solution of the differential equation. Hence, Backward Reachability:  Backward Reachability Algorithm: Initialization: repeat if return ” reachable “ endif until return “ not reachable“ Backward Reachability: Example:  Backward Reachability: Example q0 q1 q2 q3 q4 q5 q6 Backward Reachability: Example:  Backward Reachability: Example q0 q1 q2 q3 q4 q5 q6 Backward Reachability: Example:  Backward Reachability: Example q0 q1 q2 q3 q4 q5 q6 Bisimulation: Example:  Bisimulation: Example We can check, is a bisimulation of the given system, but is not. q0 q1 q2 q3 q4 q5 q6 Bisimulation: Example:  Bisimulation: Example q0 q1 q2 q3 q4 q5 q6 Bisimulation: Example:  Bisimulation: Example q0 q1 q2 q3 q4 q5 q6 Not a Bisimulation Bisimulation: Definition:  Bisimulation: Definition A bisimulation of a transition system is a partition of the state space S of T such that, is a union of elements of the partition, is a union of elements of the partition, If one state (say s) in some set of the partition (say ) can transition to another set in the partition (say ), then all other states, in must be able to transition to some state in . More formally, Bisimulation: Algorithm:  Bisimulation: Algorithm Let, be a bisimulation of the transition system, T and let be the quotient-transition system. is reachable by T, iff is reachable by .In fact, bisimulation preserves any property that can be expressed in CTL.[1] Algorithm: Initialization: while such that do end while return Bisimulation Algorithm: Example:  Bisimulation Algorithm: Example q0 q1 q2 q3 q4 q5 q6 Bisimulation Algorithm: Example:  Bisimulation Algorithm: Example q0 q1 q2 q3 q4 q5 q6 Problems at Hand:-:  Problems at Hand:- 1. Due to possible variations in the system parameters which are determined only after the low level synthesis is complete, our hybrid system model may change. We wish to automate the effects of change. It will also give us the range of system parameters for which the circuit behavior does not violate the system specifications. 2. In the design hierarchy, we may have a block-level design, which can be resolved into circuit-level design. To check whether, the two designs are compliant, we will check the equivalence of two hybrid automata. Intuitive Idea:  Intuitive Idea Any two equivalent hybrid systems, should follow the same differential equation, at any given cycle, assuming the designs are correct. Hence at any given cycle, a particular state in H1 should have a mirror state in H2. So, we aim to compose the two hybrid systems. Intuitive Idea: Contd.:  Intuitive Idea: Contd. Consider the following 2 models H1 H2 Intuitive Idea: Contd.:  Intuitive Idea: Contd. Composed Model H1 || H2 Informal Algorithm:  Informal Algorithm Algorithm: Init(c) = compose (Init1,Init2); Q(c) = Init(c) ; while all the nodes of H1 and H2 are not in Q(c) for each node(s(i), s’(i)) in Q(c) for each transition of s(i) to p(j) (say e(ij)) for each transition of s’(i) to p’(j) (say e’(ij)) if(!check_consistency(e(ij), e’(ij)) return FAILURE else compose (p(j), p’(j)) ; Q(c)=union( Q(c), (p(j), p’(j)) ) ; endfor endfor endfor endwhile Existing Hybrid Model Checking Tools:  Existing Hybrid Model Checking Tools Checkmate for verifying hybrid systems.[MATLAB Based] Chutinan, Krogh, Stursberg et. al., CMU Requiem for verifying hybrid systems. University of Pennsylvania d/dt for verifying and synthesis hybrid systems. Thao Dang and Oded Maler HyTech for verifying linear hybrid systems. Thomas A Henzinger, Pei-Hsin Ho, and Howard Wong-Toi Ptolemy II for simulating concurrent, embedded and hybrid systems. Center for Hybrid and Embedded Software Systems (CHESS), University of California, Berkeley. Edward A. Lee Reference:  Reference [1]“Lecture Notes on Hybrid Systems” John Lygeros, University of Patras [2]T.A.Henzinger. Hybrid automata with finite bisimulations. ICALP 95: Automata, Languages, and Programming, Lecture Notes in Computer Science 944, Pages 225-238. Springer-Verlag, 1995. [3]T.A.Henzinger. Theory of Hybrid automata [4]Rajeev Alur, T.A. Henzinger et. al. The Algorithmic Analysis of Hybrid Systems, Theoretical Computer Science, 1995

Related presentations


Other presentations created by Crystal

Organic Farming
27. 12. 2007
0 views

Organic Farming

LA break out FINAL
17. 06. 2007
0 views

LA break out FINAL

011404New and Old Mexico
04. 10. 2007
0 views

011404New and Old Mexico

Course Guidelines
12. 09. 2007
0 views

Course Guidelines

NS102 21 S07 Desert Storm
12. 09. 2007
0 views

NS102 21 S07 Desert Storm

MehdiMoniri Bachelorseminar
12. 10. 2007
0 views

MehdiMoniri Bachelorseminar

ice hockey
06. 09. 2007
0 views

ice hockey

Experiencing Helsinki 06
06. 09. 2007
0 views

Experiencing Helsinki 06

yant
06. 09. 2007
0 views

yant

Mud Sharks Flyer
06. 09. 2007
0 views

Mud Sharks Flyer

Peasants Revolt powerpoint
07. 12. 2007
0 views

Peasants Revolt powerpoint

Grammar Evolution2
05. 11. 2007
0 views

Grammar Evolution2

IT S A HELL OF TORNADO for web
05. 10. 2007
0 views

IT S A HELL OF TORNADO for web

McKinsey Productivity
23. 11. 2007
0 views

McKinsey Productivity

Aging Spr06 Lect13
23. 11. 2007
0 views

Aging Spr06 Lect13

1900tot1950af
12. 11. 2007
0 views

1900tot1950af

presentation 1
04. 01. 2008
0 views

presentation 1

cspin 200011
05. 11. 2007
0 views

cspin 200011

Turkey 0105
22. 11. 2007
0 views

Turkey 0105

Iowapain
07. 11. 2007
0 views

Iowapain

ch01s3
19. 11. 2007
0 views

ch01s3

Ripe Arin Apnic
03. 01. 2008
0 views

Ripe Arin Apnic

chapter 5
14. 11. 2007
0 views

chapter 5

THAE0402
28. 09. 2007
0 views

THAE0402

Richard Harris
04. 12. 2007
0 views

Richard Harris

CERM Lecture 1A
04. 01. 2008
0 views

CERM Lecture 1A

bridgesFIU
26. 03. 2008
0 views

bridgesFIU

Aradhna aggarwal
27. 03. 2008
0 views

Aradhna aggarwal

EARTH SCIENCE SOL
07. 04. 2008
0 views

EARTH SCIENCE SOL

ASAHPERD PPP
27. 11. 2007
0 views

ASAHPERD PPP

Japan2007
30. 03. 2008
0 views

Japan2007

smith bob
09. 04. 2008
0 views

smith bob

Kiko Presentation II
10. 04. 2008
0 views

Kiko Presentation II

CMA GTS
27. 09. 2007
0 views

CMA GTS

NCH IR2005 AP
17. 04. 2008
0 views

NCH IR2005 AP

FM DVD Notes
22. 04. 2008
0 views

FM DVD Notes

Sleep Aging Well
01. 12. 2007
0 views

Sleep Aging Well

Weniger VATA Presentation 2007
06. 09. 2007
0 views

Weniger VATA Presentation 2007

lB 6augh away stress
17. 06. 2007
0 views

lB 6augh away stress

lazzaro nicole
17. 06. 2007
0 views

lazzaro nicole

laughter
17. 06. 2007
0 views

laughter

Last Mile
17. 06. 2007
0 views

Last Mile

language play
17. 06. 2007
0 views

language play

Rewrite
06. 09. 2007
0 views

Rewrite

2003 DNS Frisco
29. 10. 2007
0 views

2003 DNS Frisco

literary genres
17. 06. 2007
0 views

literary genres

Liking and Loving
17. 06. 2007
0 views

Liking and Loving

Lecture Summer school
17. 06. 2007
0 views

Lecture Summer school

lecture 18
17. 06. 2007
0 views

lecture 18

lecture 01
17. 06. 2007
0 views

lecture 01

lect14
17. 06. 2007
0 views

lect14

lect14 semantics
17. 06. 2007
0 views

lect14 semantics

Vincentvan Gogh
20. 11. 2007
0 views

Vincentvan Gogh

ClaytonNeighbors
28. 12. 2007
0 views

ClaytonNeighbors

Praesentation2003
31. 12. 2007
0 views

Praesentation2003

ct rus auto
16. 11. 2007
0 views

ct rus auto

Nenes GAPower03
02. 01. 2008
0 views

Nenes GAPower03

UD9 Quiz
20. 11. 2007
0 views

UD9 Quiz

Harrier Seminar Jan 2004
16. 11. 2007
0 views

Harrier Seminar Jan 2004

L14 comb
17. 06. 2007
0 views

L14 comb

Galo Molina
15. 11. 2007
0 views

Galo Molina

NATO STCU
01. 10. 2007
0 views

NATO STCU

cushmancvbb
05. 12. 2007
0 views

cushmancvbb

SP297
27. 11. 2007
0 views

SP297

Italu pristatymas
01. 11. 2007
0 views

Italu pristatymas

cfunited 06 ThomasBurleson
01. 12. 2007
0 views

cfunited 06 ThomasBurleson

group1presentation to post
01. 01. 2008
0 views

group1presentation to post

nenny soemiwinata
29. 09. 2007
0 views

nenny soemiwinata

CCAT06 Holland
15. 11. 2007
0 views

CCAT06 Holland

paper pansa
24. 11. 2007
0 views

paper pansa