Design and implementation of a new digital automatic gain control

Design of the Control System for Automatic Riveting Machine Based on PLC implementation on fiber transmission with automatic photo-power control system
Dr.SethPatton Profile Pic
Dr.SethPatton,United Kingdom,Teacher
Published Date:30-11-2017
Your Website URL(Optional)
Comment
1 Introduction This master thesis will consider automatic control design synthesis based on high level temporal logic motion planning. The main purpose is to study how to design control input for a continuous linear system such that the controlled system satis es a temporal logic formula. Temporal logic consists of mathematical formulas which express properties that a system is desired to satisfy. The formulas are built by atomic propositions, logic connectives and temporal modal operators. Atomic propositions are statements which can be true or false and which considers the system variables 1. An example of an atomic proposition is "The robot is in room 1", where the system is the robot motion and room 1 is a subset of the area the robot can move around in. The example is expressed as in equation (1).  =r (1) 1 1 Logic connectives are operators which, when applied to the atomic propositions, describes other areas of the system's state space as a function of the named propositions 1. An example of a logic connective is "The robot is either in room 1 or in room 2.", here the logic connective is the or which is expressed as a disjunction (_). The example is expressed as in equation (2).  =r _r (2) 2 1 2 Other logic connectives includes negation (:), conjunction () and implies ()). Temporal modal operators describe present and future events with respect to the atomic propositions 1. An example of a temporal modal operator is "The robot will eventually be in room 2.", where the temporal modal operator is eventually (). The example is expressed as (3).  =r (3) 3 2 Other temporal modal operators includes next ( ), always () and until (U). Three simple examples of implemented temporal logic are illustrated in gures 1 and 2. The examples consider a robot which is moving around 6 rooms through a corridor. In gure 1a, the robot stands still in room 1. This example satis es the atomic proposition r and the satis ed formulas includer . In gure 1 1 1b, the robot stands still in room 2. This example satis es the atomic propositionr . Furthermore it 2 satis es the formular _r , composed of the atomic propositions r andr and the logic connective 1 2 1 2 _. In gure 2, the robots starts in room 1, moves through the corridor to room 2 followed by room 6 and nally return to room 1 where it stops. Throughout the run, di erent atomic propositions hold at di erent point in time. The run itself, satis es formulas such asr , rUc,:r among others. 2 2 5 Temporal logic consists of several types such as Linear Temporal Logic (LTL), Metric Interval Temporal Logic (MITL) and Signal Temporal Logic (STL). Which connectives and operators are included in each type is de ned by the grammar and semantics of the type, which is presented in section 2. Up until now the focus area within research have been LTL. The subject of formal control design based on LTL have been widely studied in papers such as 1, 2, 3, 4, 5, 6, 7, 8 and 9, motivating a shift of focus to new areas such as MITL or STL. LTL considers discrete time 10, as illustrated in tables 1 and 2. While MITL and STL both considers real-time 11, 12. Adding a time aspect to the problem would increase the possibilities regarding the speci cations given to a system. For instance, it would allow for language such as "Remain within room 1 for all time in the time interval 5 to 10 time-units." ( r ), a developed form of "Remain within room 1, always." 5;10 1 (r ). 1 In this report, all three mentioned temporal logics will be presented; including grammar, semantics and some easy to follow examples based on motion planning. This is done in section 2, which also includes a comparison between the subjects. Based on this comparison, MITL have been chosen as the topic of study in this master thesis. The problem de nition and preliminaries of the single-agent problem and the multi-agent problem are presented in section 3 and section 6 respectively, and the approach to the problems, i.e. the solutions are described in section 4 and section 7. Examples and results from MATLAB simulations are presented in sections 5 and 8. Finally, the result is summarized and evaluated in section 9, and conclusions regarding the thesis as well as future work are presented in section 10. 1Room 1 Room 2 Room 3 Room 1 Room 2 Room 3 Corridor Corridor Room 4 Room 5 Room 6 Room 4 Room 5 Room 6 (a) The robot is in room 1. Hence, for- (b) The robot is in room 2. Hence for- mulas and holds, while formula mulas  and  holds while formula  1 2 3 2 3 1 doesn't. doesn't. Figure 1: Example of two very simple runs of a motion planning system. The system consists of a robot which moves around in 6 rooms through a corridor. The atomic proposition set consists of the set R =frji = 1; 2; 3; 4; 5; 6g which considers if the i robot is in a given room. The red circle represents the robot. Room 1 Room 2 Room 3 4 1 2 Corridor 3 Room 4 Room 5 Room 6 Figure 2: The gure illustrates a slightly more complicated run of the same system as introduced in 1. The robot moves according to the arrows and numbers, starting and ending in room 1. The run satis es formula . The other two formulas and 3 1  are satis ed at some points in time, but not throughout the entire run. 2 22 Temporal Logic In this section, the topics of LTL, MITL and STL are presented. The grammar, semantics and terminology of the three temporal logic versions are described in sections 2.1, 2.2 and 2.3, and the di erences are discussed in 2.4, ending with a motivation of the conclusion to base this master thesis on MITL. 2.1 Linear Temporal Logic The grammar of LTL is de ned according to equation (4), and includes true, atomic proposition, negation, disjunction, until and next 10.  :=jj:j_ jU j  (4) The semantics of an LTL formula is de ned as a language Words() which contains all in -  nite words over the alphabet, 2 , that satisfy  10. The language is de ned in accordance with De nition 2:1:1. The properties of the satisfaction relation () are de ned in De nition 2:1:2. De nition 2.1.1. Let be an LTL formula over . The linear-time property induced by is de ned by:  Words() =f2 2 jg (5)  where 2 LTL is the satisfaction relation. De nition 2.1.2. LTL semantics of the satisfaction relation is de ned as:   , 2 ; ( ) 0 0  , and : , 2   ,   ::: 1 2 U , 9j 0;  ::: and  :::;8is:t: 0ij (6) j j+1 i i+1   where  =    ::2 2 is an in nite word (see De nition 2:1:3) over 2 which satis es  and 0 1 2  =fji = 0;:::ng is a set of atomic propositions  . i i From the grammar in equation (4); eventually, always, false, conjunction, implies, equivalence and parity(exclusive or), can be deducted in accordance with equation (7).  = U  = :: ? = :  = :(:_: ) ) = :_ , = () ) ( ))  = (: )_ (: ) (7) In all temporal logics, there are some terminology which is used. This terminology includes words and runs among other. The de nitions of these terms are given below in De nition 2:1:3 and De nition 2:1:4 .  De nition 2.1.3. A word  is an in nite string   :::, where  2 2 8i 0. 0 1 i De nition 2.1.4. A run of in an non-deterministic Buc  hi Automaton (NBA) (see De nition 2:1:6)  i is an in nite sequence of states s.t. q 2 Q and q q ;8i 0. Where Q is the set of initial 0 0 i i+1 0 states. 3When approaching control problems with LTL, transition systems are considered. Transition systems are a representation of systems just as automata and state space equations can be. The de nition of a transition system is given in De nition 2:1:5 10. Examples of words included in the alphabet of a transition system and LTL formulas satis ed by a transition system is given in Example 2:1. De nition 2.1.5. A transition system is a tuple TS = (;  ; ;;AP;L), init where   =frji = 0;:::;ng is a set of states, i     is a set of initial states, init   =fji = 0;:::;lg is a set of actions, i      is a transition relation, the expression (r ; ) =r i used to express transition i j k from r to r under the action  , i k j  AP =fapji = 0;:::;mg is a set of atomic propositions and i AP  L :  2 is a labelling function. As mentioned above, another representation is automata. The de nition of a non-deterministic automaton is given in De nition 2:1:6 10. LTL formulas can be translated into automata, using the fact that some states are accepting, creating an automaton which is accepting of all runs which satisfy the LTL formula it is built for. De nitions of accepting words and accepting runs are given in De nition 2:1:8 and De nition 2:1:7, also accepting language in De nition 2:1:9 13. An example of a automaton constructed from a temporal logic formula and accepting words/runs are given in section 2.2 in Example 2:2. De nition 2.1.6. A non-deterministic Buc  hi Automaton is a tupleA = (S;S ;E;F;AP;L) where init  S =fsji = 0;:::;ng is a nite set of states, i  AP =fapji = 0;:::;lg is a nite set of inputs, called an alphabet, i  ESAPS is a transition relation,  S S is a set of initial states and init  FS is a set of accepting states,  L is a labelling function, labelling some set of atomic propositions to each state. De nition 2.1.7. An accepting run is a run for which there are in nitely many j 0 s.t. q 2F , j i.e. a run which consists of in nitely many accepting states. De nition 2.1.8. An accepting string is a string  which has an accepting run in A. De nition 2.1.9. An accepted language L(A) is a set of all accepting strings of A. Example 2.1. Returning to the example with the robot moving around 6 rooms, the system can be translated into the transition system presented in gure 3, assuming that the robot starts in room 1 and that the controllers which induces the transitions are a;b;:::;f according to the gure. The language of the system includes any combination ofa;b;::;f (any word) starting witha and otherwise n n n n n n only containing any of the combinations (ba) , (ac) , (cb) , (de) , (ea) and/or (fd) , as well as a possible end letter. An example of a word included in the language is: aaccbe, which would take the 1 robot from room 1 (q ), through the corridor (q ) to room 4 (q ), back through the corridor to room 1 0 4 5 (q )and nally back through the corridor to room 3 (q ). Furthermore, the system would satisfy 5 3 LTL formulas such as:  =r ) ( c), where c is the corridor. The formula translates to "The robot 4 being in room 4 implies that the next room it enters will be the corridor.". 1 Here q is used to represent states in the transition system instead of r , this is done in order to avoid confusion between i i states and rooms. 4q , r q , r 1 1 4 4 a b c a d b q , r q , c q , r 2 2 0 5 5 f c a e e d q , r q , r 3 3 6 6 Figure 3: Transition system of a robot moving through 6 roomsq ;::;q by a hallway 1 6 q . The robot starts in room 1. 0 52.2 Metric Interval Temporal Logic This section contains de nitions and examples considering both MITL as well as the timed aspects of automata and transition systems. Previous work within the elds which have been used as a basis for this section, includes 14, 7, 15 and 12. In MITL real-time is considered rather than discrete- time. Therefore, this section is initialized by some de nitions regarding timed terms. Namely, time sequence, timed word and timed language, the de nitions follow 13. De nition 2.2.1. A time sequence  =  ::: is an in nite sequence of time values which satis es 0 1   2IQ , i +    ;8i 0 and i i+1  9i 1; s:t: t;8t2I. i De nition 2.2.2. A timed wordw over the set  is a nite sequencew = ((0); )((1) ):::((n) ), 0 1 n  where  =(0)(1):::(n) is a nite word over 2 (see De nition 2:1:3) and  =  ::: is a time 0 1 n sequence (see De nition 2:2:1). De nition 2.2.3. A timed language L over  is a set of timed words, i.e. L =fwji = 0;::;ng. i The MITL grammar is de ned as equation (8) 12, translating to true, proposition, negation, disjunction and until. :  =jpj:j_ jU (8) a;b The semantics of MITL is illustrated in De nition 2:2:4. De nition 2.2.4. Let  be an MITL formula over  and (s;I) be a timed state sequence (timed word). The semantics of the satisfaction relation is then de ned as:  , 2s (s ) 0 0 : ,  2  , and 0 t 0 t U , 9t2I; s:t:  and8t 2 (0;t);  (9) I The grammar in (8) can be extended to include eventually, always, false and conjunction, as illustrated in equation (10).   = U  a;b a;b   = : : a;b a;b ? = :  = :(:_: ) (10) As for the LTL, the system which is evaluated can be represented by a transition system. How- ever, in order to take in consideration the time aspect which MITL includes, weights are added to transitions. These weights corresponds to the time a transition takes. The de nition of a weighted transition system is given in De nition 2:2:5 16. De nition 2.2.5. A weighted transition system is a tuple T = (;  ; ;;AP;L;d) init where   =frji = 0;:::;ng is a set of states, i     is a set of initial states, init   =fji = 0;:::;lg is a set of inputs, i   :   2 is a transition map, the expression (r ; ) = r i used to express transition i j k from r to r under the action  , i k j  AP is a set of observations,  L : AP is an observation map and  d :  R is a positive weight assignment map. + Corresponding to the runs, de ned in section 2.1, there are timed runs, taking in consideration whether some clock-constraints are ful lled. The de nition is given in De nition 2:2:6. 6t De nition 2.2.6. A timed run r = (r(0); )(r(1); ):::(r(n) )2 I for a transition system T 0 1 n (see De nition 2:2:5) is a nite sequence wherer(0)r(1):::r(n) is an untimed run (see De nition 2:1:4) and   ::: is a time sequence s.t. 0 1 n   = 0 0   = +d(r(i);r(i + 1));8i2f0; 1;:::;n 1g, i+1 i where d(r(i);r(i + 1)) is the transition weight for the transition between the state corresponding to r(i) to the state which corresponds to r(i + 1), i.e. the time the transition needs. Finally, the MITL formula can be translated into a timed automaton (see section 4.2 for details). The timed automaton includes clocks and clock-constraints. Before presenting the de nition of a timed Buc  hi automaton, the de nitions of clock constraints and clock valuation will be considered. The de nition of clock constraints is given in De nition 2:2:7 17. De nition 2.2.7. Let C be a nite set of clocks C =fc ;c ;:::;c g, a set of clock constraints  1 2 M C over C is then de ned as: 0  :=j?jc./kjcc ./kj j _  ; C 1 2 1 2 0 wherek2N is a non-negative integer,./2f=; =6 ;;;;g is an comparison operator andc;c 2C are clocks. The clock valuations are de ned as De nition 2:2:8 18. De nition 2.2.8. A clock valuation (or interpretation)v for a set of clocksC, assigns a real value to each clock and hence maps from C toR f0g. v + denotes the valuation which maps every clock + : c to the value v(c) +. vR = 0 denotes the valuation for C which assigns 0 to each c2 R C, and agrees with v over the rest of the clocks. Now, we proceed with the de nition of a timed Buc  hi automaton, which is given in De nition 2:2:9 13. De nition 2.2.9. A timed Buc  hi Automaton (TBA) is a tuple A = (S;S ;X;I;E;F;AP;L) where 0  S =fsji = 0; 1;:::g is a nite set of locations, i  S 2S is the set of initial locations, 0 AP  2 is the alphabet or set of actions (AP is the set of atomic propositions),  X is a nite set of clocks,  F2S is a set of accepting locations,  I :S  is a map labelling each state s with some clock constraint, X i X  ES   2 S is a set of transitions and X  L is a labelling function, labelling some set of atomic proposition to each state. A state of A is a pair (s;v) where s2 S is a location and v is a valuation that satis es I(s). The initial state ofA is a pair (s ; (0; 0;:::; 0)), wheres 2S and the null-vector (0; 0;:::; 0) is a vector of 0 0 0 jXj number of valuations v = 0. i Similarly to the accepting word and accepting runs of the BA constructed from the LTL formula, there are accepting timed words and accepting timed runs for the TBA. An example of accepting timed words and accepting timed runs are given in Example 2:2. Example 2.2. Consider the timed automata A illustrated in gure 4. The automata consists of  3 states; s , s and s , where s is the initial state and s is the accepting state. The accepting 0 1 2 0 1 words ofA , are the words which results in the system visiting the accepting states in nitely often.  1 Similarly, the accepting runs of A , are the runs which visits the accepting state in nitely many  times. An example of an accepting word of A is:  0 (0;f:ag)(t;fag) 0 where t b. The corresponding accepting run is : 0 0;f:ag t ;fag (s ; 0) (s ; 0) (s ; 0) 0 0 1 7¬a,c≤b a,c≤b, c := 0 s s 0 1 ,, c := 0 ,cb, c := 0 s 2 ,, c := 0 Figure 4: Illustration of the timed automata A , constructed of the MITL formula   = a, where a is an atomic proposition i.e.  =fag. b Examples of a non-accepting words of A is:  00 (0;f:ag)(t ;fag) 00 where t b, and w (; (f:ag) ) for any in nite time sequence . In the rst example the system transition to state s due to the 2 clock-constraint cb being broken, in the other example the atomic proposition a is never ful lled. The corresponding runs of the words are: 00 0;f:ag t ;fag (s ; 0) (s ; 0) (s ; 0) 0 0 2 and i w 0:::i1;(f:ag) i;f:ag i+1:::;(f:ag) (s ; 0) (s ; 0) (s ; 0) (s ; 0) 0 0 2 2 wherei is theith element of the sequence ,i::j is the elements between i andj andi is the rst element which is greater than b. The accepting words corresponds to the sequences of atomic propositions and time which satis es the MITL formula  = a, which the automaton is constructed of. b n 0 0 Notice: All accepting words are those with a pre x (0;f:ag)(; (f:ag) )(t;fag), for somet b, 0 where  is a nite time sequence of length n and t  ,8jn. j An example of a weighted transition system which is evaluated by an MITL formula follows in Example 2:3. 86s 2s 2s 2s 4s 2s 1s 4s 1s (a) The robot (illustrated as a black dot), (b) Example of a run which ful ls the can move within the 5 5 area. Mov- MITL formula given in Example 2:3. ing one square upwards or to the left demands 2s, while moving one square downwards or to the right only demands 1s. Figure 5: Motion planning example of a robot moving through a partitioned space. The gures illustrate costs of movements and a possible run. Example 2.3. Considering the system illustrated in gure 5a, a robot is moving within a partitioned area of the size 5 5. Movements upwards or to the left costs the robot 2s, while movements downwards or to the right only costs 1s. Now, consider the MITL formula  = red:blueU yellow(yellow) blue) 5s 10s 12s The formula states  that the robot must reach the red square within 5s,  that it mustn't go to the blue square until it has been at the yellow square,  that it must reach the yellow square within 10s and  that it always must go to the blue square within 12s if it enters the yellow square. Assuming the robot starts at the square which it is located at in the gure, the MITL formula can be satis ed. An example of a run which satisfy the formula is given in gure 5b. Here the robot reaches the red square by 4s (4 5 - ok), it doesn't enter the blue square until it has been in the yellow square, it enters the yellow square by 10s (10 10 - ok), and nally the blue square within 8s of entering the yellow square (8 12 - ok). 2.3 Signal Temporal Logic Previous work within STL include papers such as 12, 19, 20, 21 and 22. This section is based on the information presented in those papers. The grammar of STL is given by equation (11) and includes true, atomic proposition, negation, disjunction and until. The grammar can be extended to include eventually, always, conjunction and false in accordance with equation (12).  :=jj:j_ jU (11) a;b 9  = U  a;b a;b   = : : a;b a;b  = :(:_: ) ? =: (12) Where the value of  is determined by the underlying signal x;  f(x) c, where f is a scalar-valued function over x,2f;;;; =; =6 g and c is a constant real number. The boolean semantics of the satisfaction relation is given by De nition 2:3:1. De nition 2.3.1. The boolean semantics of STL is de ned as (x;t) , x satis es at timet (x; 0) , x (x;t): , (x;t)2 (x;t) , (x;t)and (x;t) (x;t)_ , (x;t)or (x;t) 0 0 (x;t)  , 8t 2I +t; (x;t ) I 0 0 (x;t)U , 9t 2I +t; s:t: (x;t ) and I h i 00 0 00 8t 2 t;t ; (x;t ) (13) The new aspect of STL, which MITL is lacking is the possibility to measure how close the signal is to not ful l . This measurement is expressed by . The value of  is determined by the signal x the atomic proposition  and the time t. The semantics of , also called the quantitative semantics, are given by De nition 2:3:2. De nition 2.3.2. The quantitative semantics of STL is de ned as (;x;t) = f(x(t)) (:;x;t) = (;x;t) ( ;x;t) = min((;x;t);( ;x;t)) (_ ;x;t) = max((;x;t);( ;x;t)) 0 ( ;x;t) = min((;x;t )) I 0 t2I   0 00 (U ;x;t) = max min ( ;x;t ); min (;x;t ) (14) I 0 00 0 t2I t 2t;t An example of a signal which is evaluated by some STL formulas follows in Example 2:4. Example 2.4. An example of a system which can be evaluated by an STL formula is given in gure 6a. The gure illustrates a signal x evolving over time. It is clear from gure 6b, that the system satis es the STL formula(jxj 3). While it does not satisfy(jxj 2) (see gure 7a) for all t. However, as illustrated in gure 7b, it does satisfy the formula for some t, hence the STL formula  (jxj 2) is satis ed. 2:15;4:2 10x x 2 2 1 1 0 0 1 2 3 4 5 t 1 2 3 4 5 t -1 -1 -2 -2 -3 -3 (a) A signalx evolving over timet, de n- (b) The absolute value of the signal never ing a system. exceeds 3, and hence satisfy(jxj 3). Figure 6: Example of a signal under evaluation of an STL formula. x x (2.15,2.0) (4.2,2.0) 2 2 1 1 0 0 1 2 3 4 5 t 1 2 3 4 5 t -1 -1 -2 -2 -3 -3 (a) The absolute value of the signal (b) The absolute value of the sig- does exceed 2, and hence doesn't satisfy nal doesn't exceed 2 at the time (jxj 2). interval 2:15; 4:2, and hence satisfy  (jxj 2). 2:15;4:2 Figure 7: Example of how the real-time could be applied in order to satisfy the softer version of a temporal logic formula. 112.4 Comparison The main di erences between the already studied LTL and the possible areas of study, STL and MITL, are illustrated in table 1. An example is given in table 2. It follows that MITL is an extension of LTL which includes time-constraints and that STL is a further extension which, besides including time-constraints, also predicates over real-values compared to LTL and MITL which predicates over boolean. When approaching the problem at hand the considered methods would therefore di er. Table 1: Properties that di er between LTL, MITL and STL, 23. Predicates over Time property LTL Boolean Discrete-time MITL Boolean Real-time STL Real-value Real-time Table 2: Example of di erences conserning the expression possibilities of LTL, MITL and STL. Example LTL pUq At some point in the future, q will be true, until then p will be true. MITL pU q At some point in the time interval 1 to 5 time- 1;5 units, q will be true, until then p will be true. STL (x(t) 2)U (y(t) 5) At some point in the time interval 1 to 5 time- 1;5 units, y will be greater than 5, until then x will be smaller than 2. The approach to the problem using LTL is described by scheme 8. The scheme is a remake of the image"Temporal Logic-Based Planning: Hierarchical Approach" in 24. In short, the LTL formula and the continuous system is abstracted into a joint discrete model by creating an automata product of a Buc  hi automaton representing the LTL formula and a discrete model abstracted directly from the system. The control input is then designed based on accepted runs of the automata product. Due to STL predicating over real-values, it is not possible to translate an STL formula to an automaton. This would not be an issue for the MITL approach. To solve the problem based on STL, the considered approach would become an optimization problem where the system is considered as the cost function and the STL formula as conditions. Due to the authors preference towards automaton, the area of MITL has been chosen. 12Figure 8: Remake of the scheme "Temporal Logic-Based Planning: Hierarchical Approach" in 24 by Jana Tumova. 133 Problem De nition 1 The problem considered in this master thesis is nding a control input for the continuous linear system (15), which ful l the MITL formula . (15) is assumed to be controllable and stabilizable. x _ =Ax +Bu (15) x2X u2U 4 Solution Approach 1 The intended approach to the problem is illustrated in scheme 9. The approach has been constructed based on previous work such as 23, 2, 1 and 3, the idea being to adapt the approach towards the LTL problem such that it suits the MITL issue. Each step of the approach is described in more detail in sections 4.1, 4.2, 4.3 and 4.4. Figure 9: Scheme describing the MITL approach to the problem. 4.1 Abstraction of the Continuous System to a Transition System X X N Assuming thatx2R (a ;b )R in (15), that is that the state space of the system can be divided N into rectangles of dimension N (see De nition 4:1:1), the following approach towards abstracting the environment into a weighted transition system is suggested, it follows the theory presented in 16. N De nition 4.1.1. An N-dimensional rectangle R (a;b)R is characterized by two vectors a;b, N wherea = (a ;a ;:::;a ),b = (b ;b ;:::;b ) anda b ,8i = 1; 2;:::;N. The rectangle is then given 1 2 N 1 2 N i i by N R (a;b) =fx2R j8i2f1; 2;::;Ng :a x bg (16) N i i i That is, the vector a includes the points in each dimension which the rectangle's rst vertex is positioned in and theb vector includes the points in each dimension which the rectangle's last vertex is positioned in. Firstly, the state space x is divided into rectangles in accordance with the atomic propositions which are considered. Namely, if AP =fapji = 0;:::;lg is the set of atomic propositions then the i partition follows equation (17). Which ensures that there is always a distinct answer regarding if an atomic proposition is true or false within a rectangle, i.e. it eliminates the possibility of an atomic proposition being true in part of a rectangle and false in the other part. Now, if the MITL formula is constructed of the atomic propositionsap , it will be possible to determine if a run in the partitioned i state space satis es the formula. The rst step in abstracting system (15) to a weighted transition X X system, is then to de ne the states q in De nition 2:2:5 as the rectangles R (a ;b ). N d j;ap j;ap X X i i i ap = R (a ;b )R (a ;b ); d 2N (17) i N N i j=1 14The next step is to include the time aspect in the abstraction. 16 suggest a solution by introducing the Facet Reachability Problems, which considers whether a closed-loop system can reach determined facets of a rectangle. Namely, is it possible to design a control input such that the system can exit one rectangle and enter another? A theorem determining when the problem is solvable, i.e. when such a controller can be designed, is presented in Theorem 1, introduced in 16. Theorem 1. Let R (a;b) be a rectangle and "F(a;b) be a non-empty subset of its facets. 9 a N multi-ane feedback controller k : R (a;b) U s.t. all the trajectories of the closed-loop system N (15), originating in R (a;b), leave it through a facet from the set " in nite time if: N n (Av +Bk(v)) 0;8F2Fn";8v2V(a;b); (18) v F and 02= Conv(fAv +Bk(v)jv2V(a;b)g) (19) where Conv denotes the convex hull andV(a;b) is the vertexes (corners) of the rectangle. Equation (18) states that the closed-loop system (15) must move away from the facets which are not approved. While equation (19) includes that the system must always evolve (the speed of the system can't be 0). Note, equation (19) contains more information than this. Theorem 1, states that it is possible to design a controller such that the system always exit a rectangle through a determined facet if equation (18) and equation (19) are satis ed. If there is only one approved facet, i.e if " =fFg, condition (19) can be simpli ed to equation (20), stating that the system must move towards the approved facet. n (Av +Bk(v)) 0;8v2V(a;b) (20) F 16 continue by proposing that the system will leave the rectangle through the given facet in F F time less than or equal to T , where T is de ned according to equation (21), where i corresponds to the outer normal e which the particular facet has and s and s are de ned according to (22). i F F   s b a F F i i T =ln (21) s s s F F F s = min (h(v) +Bk(v)) s = min (h(v) +Bk(v)) (22) F i F i v2V(F) v2V(F) F The idea behind T is to calculate the time it would take for the system to reach the facet, assuming that it starts at the point the furthest away from it, i.e. on the opposite facet, and that it F moves towards the facet at the slowest possible rate given the determined u. That is, choosing T as the maximum time required for the transition to occur. For a continuous linear system (15) this corresponds to solving the problem x _ = (Ax) + (Bu) (23) i i i x(0) =x x(t ) =x i 0 1 i 1 wherei is the norm direction of the facet, fort . Which gives the time it will take for the system 1 (15) to evolve from x to x in direction i. Hence, if x is a point along the facet, t is the time it 0 1 1 1 will take for the system to reach the facet from the point x . Now, assuming that u is linear, i.e. 0 Bu =B x +B system (23) can be rewritten to (24). 1 2 n     x _ = ((A +B )x) + (B ) = (A x) +B = a x +B (24) i 1 i 2 i i i ij j i j=1 n    Finally, by introducing C =B +  a x , the system can be further simpli ed to (25). j i i ij j=1;j=6 i   x _ = a x +C (25) i ii i i x(0) =x x(t ) =x i 0 1 i 1 15 The equation is solved by separatingx fromt as shown in (26), assuming thatC can be treated i i as a constant. The assumption is directly valid if u is designed such that the dependence x _ has of i  x for j =6 i is cancelled out, i.e. if a = a + (B ) = 0. If this is not true, i.e. if there is a j ij ij 1 ij desire to choose (B ) di erently, the assumption would still be indirectly valid. The motivation 1 ij  for this is that the dependence on x will be linear, this corresponds to solving the problem as if C j i were constant for two cases - x =x andx =x wheremin andmax are the smallest and j j;max j j;min biggest value x can have in the rectangle - and then using the maximum of the two solutions. j dx i   = a x +C ii i i dt Z Z   1 dt = dx i   a x +C i ii i   ln(a x +C ) i ii i t +k = (26)  a ii Now,k can be determined usingx(0) =x , giving the result shown in (27), and usingx(t ) =x , i 0 1 i 1 t can be determined as (28). 1   ln(a x +C ) 0 ii i k = (27)  a ii     ln(a x +C )ln(a x +C ) ii 1 i ii 0 i t = (28) 1  a ii F Finally, T is the maximum time it will take for the system to reach the facet (x ). This 1 corresponds to t , when x is one of the points which is the furthest away from x , i.e. when x is a 1 0 1 0 point on the opposite facet F , and when the system evolves at the slowest possible speed, i.e.when  F C is minimized. Hence, T , for a continuous linear system can be de ned as (29), where s and F i  s are de ned as (30), and a is the iith element of the matrix A +B . Here A is the matrix 1 ii F determining the open-loop dependence onx, andB is the matrix determining the added dependence 1 of x from the closed-loop. s 1 F F T =ln (29)  s a F ii     s =a x +C s =a x +C (30) F ii i i ii i i F x2F x2F Furthermore, 16 states that the time bound can be minimized by using the controller which maximizes n (Av +Bu ), i.e. which maximizes the speed of which the system moves towards the v F given facet. More precisely the optimization problem given by equation (31) must be solved for all vertexes in a rectangle for a given facet. In a 2 dimensional case this results in 4 problems for each approved facet in each rectangle.   max n (Av +Bu ) F v u 2U v 0 n 0(Av +Bu ); 8F 2F F v v F u 2U  0 (31) v Now, the time can be incorporated into the weighted transition system by setting the weights d F for each transition according to T , that is as the maximal time the system will need to nish the transition. Also, the inputs  can be set to the control-input u which will cause the transition. As for the remaining properties of the weighted transition system; corresponds to the allowed transitions i.e. the approved facets, AP =AP (the set of atomic propositions) and L is the function that maps which atomic propositions that holds in each state (rectangle). An example is given in Example 4:1. 16Example 4.1. Let the continuous linear system to be controlled be: x _ =x +u (32) 2 2 where x2 (1; 1) ; (5; 6)  R and u2 (7;7) ; (6; 6)  R . Furthermore, let the MITL formula to be satis ed  be over the atomic proposition set AP =fap ;ap ;ap ;apg. Where ap is 0 1 2 3 i de ned as: : ap x 4; x 3 0 1 2 : ap x 4; x 3 1 1 2 : ap x 3; x 3 2 1 2 : ap x 3; x 3 (33) 3 1 2 The state space of the linear system (32) is then illustrated in gure 10a. By applying equation (17) on the state space, with ap as de ned in (33), the partition illustrated in gure 10b follows. This i corresponds to a weighted transition systemT = (;;  ; ;;AP;L;d) with 5 statesr according init i to equation (34).  =frji = 0; 1;::; 4g i r =R ((1; 1); (3; 3)) r =R ((3; 1); (5; 3)) 0 2 1 2 r =R ((1; 3); (5; 4)) r =R ((1; 4); (3; 6)) 2 2 3 2 r =R ((3; 4); (5; 6)) (34) 4 2 It also follows that the observation set AP is equal to the atomic proposition set AP and that the observation map L is described by equation (35). L(r ) = ap 0 2 L(r ) = ap 1 3 L(r ) = ; 2 L(r ) = ap 3 0 L(r ) = ap (35) 4 1 Left to de ne is now , and d. This is done by considering one rectangle at a time and solving the facet reachability problem for each approved facet of that rectangle. Starting with state r =R ((1; 1); (3; 3)) we must solve the optimization problem of equation (36) for each vertex of the 0 2 rectangle (i.e. each corner), for each approved facet. maxn (x +u ) v F u 2U v n 0(x +u )  0 (36) v F Due to the de nition of the state space, there are two possible facets which the system is allowed   to transition through, F and F which is illustrated in gure 11a. Hence the optimization prob-  lem must be solved 8 times. First, considering F , yields a transition (r ; ) = r , if the facet 0 0 2 reachability problem is solvable. It is simple to see that both condition (18) and (19) are ful lled for some u. Namely, x +u 0 in both direction x and x for some u, and 0 is not in the convex hull 1 2 of the rectangle. Now, by solving the optimization problem for each corner of the rectangle one can conclude that u must be greater than1 in order to ensure that the system doesn't move in the 2  wrong direction, also u must be greater than1 at the facet opposite F but less than3 along 1  F . One possibility could then be to set u = u = 6 and u =x . This would then yield 2 max 1 1  = (x ; 6). Furthermore, solving equations (22) yieldss  = 9 ands  = 7, which when together 0 1 F F  F with equation (21) gives a maximal time of T = ln(9=7) 0:25. Hence, d((r ; )) = 0:25. 0 0 17Following the same theory, each transition in the direction of x or x from a rectangle of size 2 2 1 2 will result in the same maximal time ( 0:25). Furthermore, transitions in the direction ofx from 1 F a rectangle of size 2 2, will need T = ln(2) 0:7 and transitions in directionx from named 2 F rectangle will cost T = ln(3) 1:1. Finally, the transitions out of the rectangle of size 4 1 will F F yield a maximal time of T = ln(10=9) 0:1 in direction x and T = ln(4=3) 0:3 in direction 2 x . The nal non-deterministic weighted transition system is given in equations (37), (38), (39), 2 (40), (41), (42) and (43). T = (;  ; ;;AP;L;d) (37) init  = fr ;r ;r ;r ;rg =fR ((1; 1); (3; 3));R ((3; 1); (5; 3)); 0 1 2 3 4 2 2 R ((1; 3); (5; 4));R ((1; 4); (3; 6));R ((3; 4); (5; 6))g (38) 2 2 2  =f ; ; ;g =f(x ; 6); (6;x ); (6;x ); (x ;6)g (39) 0 1 2 3 1 2 2 1 (r ; ) =r (r ; ) =r 0 0 2 0 1 1 (r ; ) =r (r ; ) =r 1 0 2 1 2 0 (r ; )2fr ;rg (r ; )2fr ;rg 2 0 3 4 2 3 0 1 (r ; ) =r (r ; ) =r 3 1 4 3 3 2 (r ; ) =r (r ; ) =r (40) 4 2 3 4 3 2 AP =fap ;ap ;ap ;apg (41) 0 1 2 3 L(r ) =ap L(r ) =ap 0 2 1 3 L(r ) =; L(r ) =ap 2 3 0 L(r ) =ap 4 1 (42) d((r ; )) 0:25 d((r ; )) 0:25 0 0 1 0 d((r ; )) 0:25 d((r ; )) 0:25 0 1 3 1 d(r ; )) 0:7 d((r ; )) 0:7 1 2 4 2 d((r ; )) 1:1 d((r ; )) 1:1 3 3 4 3 d((r ; )) 0:1 d((r ; )) 0:3 (43) 2 0 2 3 The weighted transition system is illustrated in gure 11b. 18x x 2 2 6 6 ap ap 5 5 0 1 4 4 ∅ 3 3 ap ap 2 2 2 3 1 1 0 0 x x 1 1 0 1 2 3 4 5 0 1 2 3 4 5 (a) The grey area represents the state (b) The gure illustrates the partition space of the continuous linear system of the state space of system (32), done (32) in Example 4:1. according to equation (17), for Exam- ple 4:1. Figure 10: The state space and rectangular partition of Example 4:1. x 2 6 σ 2 5 r , ap r , ap 0 2 1 3 σ1 4 σ3 σ3 ∗ F σ σ 0 0 3 r , ∅ 2 ∗∗ ap , r 2 2 0 F σ 3 σ3 1 σ 0 σ 0 σ 1 0 x 1 r , ap r , ap 4 1 3 0 σ2 0 1 2 3 4 5 (a) The blue marked edges of rectangle (b) The gure illustrates the weighted R ((1; 1); (3; 3)) are the facets which the transition system (37), which the contin- 2 system is allowed to exit through in Ex- uous linear system in Example 4:1 can be ample 4:1. abstracted to. Figure 11: The facets of one of the rectangles of the partitioned system and the nal weighted transition system of Example 4:1. 194.2 Translation of the MITL Formula to a Timed Buc  hi Automaton In this section, the step of translating an MITL formula  to a timed Buc  hi automaton (TBA) is described. Approaches towards translating an MITL formula into a timed automata has been presented in 14, 25, 26, 27 and 28. The construction described in 26 and 27 regards MTL formulas rather than MITL, however since MITL is a subset of MTL, the method applies here as well. The main result of 25 is the corollary given in Corollary 1. The statement is supported and extended by the results of 27 presented in Corollary 2, as well as the results of 28 presented in De nition 4:2:1. The latter results extends the former by stating complexity of the automata. Corollary 1. MITL formulas can be transformed into timed automata using a simple procedure. Corollary 2. For every MTL formula  with m propositions, n unbounded temporal operators and inputs of bounded variability k, there exists l m kfut()  ...a non-deterministic timed automaton with 2m + 1 clocks and 2   m l m kfut() n 2 + 1 + 1 (2 4 + 1) states that accepts the language of . 2 l m kfut()  ...a deterministic timed automaton with 2m + 1 clocks and 2   l m m O(nlogn) kfut() 2 2 + 1 + 1  2 states that accepts the language of . 2 where fut() is a measurement of the time demanded to check if  holds, the semantics are de ned as: fut() = 0; p is a proposition.  fut( _ ) = max fut( );fut( ) 1 2 1 2 fut(:) = fut() ( a + 2 +max(fut( );fut( )); I = (a;1) 1 2 fut(U  ) = 1 I 2 b +max(fut( );fut( )); I = (a;b) or I = b;b 1 2 (m:jj) De nition 4.2.1. For all MITL formulas,B hasM() clocks andO((jj) ) locations, where    l m l m inf(I) sup(I) m =max 2 + 1; + 1 , and I is the set of time intervals included in .  jIj jIj I2I  The result of previous work clearly states that all MITL formulas can be translated into timed Buc  hi automata. Now, for the construction itself. The overall idea is as follows: 1. De ne the initial location s as the initial copy of the MITL formula:  . 0 init 2. Consider all possible initial actions which could yield a satisfying run and create one location for each such action. I.e. if the formula is  =a_b, the initial actions which could yield satisfying runs are a and b. Create edges and de ne invariants and clock constraints accordingly. 3. Create a non-accepting state which handle all other possible actions. In the example above this would be:(a_b). 4. Iterate over step 2 and 3 considering the locations created in step 2 rather than the initial location. When performing step 3 there is no need to create new non-accepting locations, it is enough to create new edges to the already existing non-accepting location. As for step 2, it might not always be a need to create a new location here either, in some cases a better solution is to create a transition back to itself or to another already existing location. 5. Mark the locations at the end of a formula, i.e. the locations which the system will remain in if the formula is satis ed, as accepting. 6. Add transitions to the non-accepting state and the accepting state, handling the time after the MITL formula, i.e. when the time bound has exceeded. These transitions must be constructed such that the sux of in nite words doesn't a ect the acceptance. For example the TBA constructed of the MITL formula a must not include transitions between accepting and b non-accepting states a ected by whether a holds for t b. This is generally done by adding transitions from the state to itself for all atomic propositions when t is outside the interval. 20

Advise: Why You Wasting Money in Costly SEO Tools, Use World's Best Free SEO Tool Ubersuggest.