Sigali User's manual
Contents
1. R X Y X 0 Qo Xo 0 The SIGALI function that gives access to this new system is implicit_sys syst The result is an I PDS for implicit PDS From a structure point of view it is a 5 tuple X X Y R Qo and the functions that gives access to the components of this I PDS are respectively state_var_I state_var_next _I event_var_I trans_rel_I initial_I controllable_var_I By loading the library Orbite 1lib you have access to the two following commands e P Orbite S_Imp returns the set of reachable states of the implicit system S_Imp e S 1 Pruned S_Imp Orbite is an implicit Dynamical system where all the states are reachable 1 4 Fix point Computation amp Function definition Fix point computation can also be performed For example given po 0 Pitt peti the corresponding expression in SIGALI is loop x x72 1 init 0 Of course such sequences do not always converge This is not checked by the system New function construction Starting from the existing functions it is also possible to define new functions The syntax is the following def f x y z with intern_l _ sigali expression intern_2 sigali expression do SIGALI body of the function For example assume we want to compute the set of reachable states from Sol P in one step of an implicit system Sr The corresponding function succ P is the following def succ P with X state_var_I S_I X_Next state2. e chrono false stops the clock 1 2 2 Symbols and declarations A symbol or an identifier can be assigned to an expression in the following format symbol lt expression gt For example ep a2 b c 2 assigns the identifier p to the expression a7b c Variables can be declared by the command declare or ldeclare For example e declare a b c d takes one or more parameters e ldeclare a b c d takes only one parameter as a list The order of the variables corresponds to the order of declaration For example in the previous example the order isa lt b lt c lt d The command indeter lists all the indeterminate symbols In order to declare variables in a given order one can use the commands declare after declare_first or declare_suff For example if the variables x lt y lt z are already declared the command e declare_after a b c will declare the variables according to the following order x lt y lt z lt a lt b lt c eax lt b lt c lt a lt y lt _z if you use declare_first a b c e declare_suff a b c will declare the variables a_1 b_ 1 c__1 in the following order a lt a_l lt b lt b1l lt c lt c_l We can manipulate list of variables as follows If L_1 and L_2 are two lists of variables then e L union_lvar L_1 L_2 is the list of variables which contains the variables of L_1 and L2 e L inter_lvar L_1 L_2 performs the intersection of the two lists e L comp_lvar L_1 is the co
3. C_Dup z 11
4. SIGALI User s manual Herv Marchand Eric Rutten amp Michel Le Borgne March 30 2004 Abstract SIGALI is a model checking tool based which manipulates Polynomial Dynamical Systems PDS that can be seen as an implicit representation of an automaton as intermediate models for discrete event systems It offers functionalities for verification of reactive systems and discrete controller synthesis It is developed jointly by Espresso and Vertecs The techniques used consist in manipulating the system of equations instead of the sets of solution which avoids the enumeration of the state space Each set of states is uniquely characterized by a polynomial and the operations on sets can be equivalently performed on the associated polynomials Therefore a wide spectre of properties such as liveness invariance reachability and attractivity can be checked Many algorithms for computing predicates states are also available 1 The model checker SIGALI 1 1 Basic facts about SIGALI The theory of Polynomial Dynamical Systems uses classical tools in algebraic geometry such as ideals varieties and comorphisms The techniques consist in manipulating the system of equations instead of the sets of solutions which avoids enumerating the state space 1 1 1 The mathematical framework an Overview Let Z Z1 Z2 Zp be a set of p variables and Z 37 Z be the ring of polynomials with variables Z Thus Z 37 Z is the set of all polyn
5. _var_Next_I S_I Y event_var_I Y Rel trans_rel_I S_I do rename exist X intersection P exist Y Rel X_Next X 1 5 Cost functions SIGALI also offers the possibility to manipulate integers Let X x1 Xn be declared variables of the system Then a cost function is a map from Z 37 to N which associates to each x 1 n of Z 37 some integer k When f x is not defined then we assume that f x oo To encode these functions we make the use of the ADD Arithmetic decision diagrams The ADD are similar to the TDD expect that we attach integers to the leaves of the ADD For example let X lt Y be two variables in Z 3z7 and f a cost function such that PX foto ofrfay ifajf aj i MDE EE Es Bars fls e s5s s s 4 s s8s Then the ADD that represents the function f is given by the graph of Figure 2 AAA 3 Figure 2 Exemple d un ADD In order to build and manipulate cost functions the following SIGALI operations are available e a const n build the constant function equal to the integer n e a var X n1 n2 n3 given a declared variable X and 3 integers f a_var X n1 n2 n3 build the cost function such that xX 1 e a X a X 1 s ci X X 0 ci X e Given two cost functions f and f2 one can perform the sum and the product of f and f2 by simply using the classical operators and x e ami
6. ables represented by a vector in Z 3Z e Y is the set of m event variables represented by a vector in Z 3Z e Q X Y 0 is the constraint equation e X P X Y is the evolution equation It can be considered as a vectorial function from Z 3Z t to Z 3Z and e Qo X 0 is the initialization equation We now explain how one can use the model checker SIGALI in order to analyze the obtain polynomial dynamical system 1 2 The SIGALI commands amp Operations 1 2 1 General Commands Starting and exiting The SIGALI environment can be started by the sigali command A prompt Sigali appears To quit one can use the SIGALI command quit e quit Loading the file of a model The z3z 1ib file which contains the model of the system or any other SIGALI files can be loaded by using the load or the read command For example in case of a file filename z3z the command is e read filename Trace By the trace command it is possible to save in a file all the commands executed and results obtained in the Sigali environment e trace filename opens the file for trace e fintrace closes the current trace file All commands executed and the corresponding responses in between are saved in the trace file Execution time SIGALI allows the measurement of the time taken for each computation e chrono true starts the clock After each subsequent command the time taken for the computa tion is displayed
7. arting from the initial states that reaches x If syst is a dynamical system and g is the canonical generator polynomial of a set of states F e Reachable syst g is True if and only if E is reachable from the initial states of syst 2 3 2 Attractivity Definition A set of states F is attractive for a set of states E iff every trajectory initialized on E reaches F If syst is a dynamical system and g is the canonical generator polynomial of a set of states E e Attractivity syst g is True if and only if E is Attractive from the initial states of syst 3 Synthesis of controllers using SIGALI 3 1 Essentials of the control synthesis problem For controllable polynomial dynamic systems the set of events Y can be partitioned into two sets Y and U where e Y is the set of uncontrollable events e U is the set of controllable events The PDS can now be written as Q X Y U 0 a P X Y U Q X 0 Let n m and p be the respective dimensions of X Y and U The trajectories of a controlled system are sequences t ye ut in Z 3Z such that Qo ao 0 and for all t Q xt yt uz 0 and t 1 P axt yt ut The events yz uz include an uncontrollable component y and a controllable component uz The controller The PDS can be controlled by first selecting a particular initial state xo and then by choosing suitable values for u1 u2 Here we only consider static control policies where the value of t
8. ely Of course these variables must occur in p Note that we can use the command init _lconst to declare the list of constants e g lconst init_lconst 3 0 is a list of 3 elements that are equal to 0 i e lconst 0 0 0 e rename p lvar1 lvar2 replaces in p the it variable of lvar1 by the it variable of lvar2 e subst p lvari 1p1 replaces in p the it variable of lvar1 by the i polynomial of 1p1 In case of the functions e l_eval lp1 lvari lconst e l rename lp1 lvar1 lvar2 e l subst lp1 lvari 1p2 the first argument is a list of polynomials instead of one polynomial and they perform the same function as their counterparts for each polynomial of the list 1 2 4 System of Polynomials manipulation The canonical generator of a polynomial system given by a list of polynomials can be computed by the function gen The command is gen lpoly where lpoly is a list of polynomials For example e gen a b c a 2 1 gives the canonical generator of the polynomial system given by the two polynomials a b c and a 2 1 The previous command can also be given as e gen a b c a 2 1 If Pi a b cand Po a 1 then the previous command will compute the polynomial P P 6 P2 P P3 which entails that the solution of P will be the solution that are common to P and P2 e equal p1 p2 compares two polynomials p1 and p2 and test whether they are equal or not Complemen
9. he control ut is instantaneously computed from the value of x and y Such a controller is called a static controller Formally it is a system of two equations Eo 0 Co X 0 where the latter equation determines the initial states satisfying the control objectives and the former describes how to choose instantaneous controls When the controlled system is in state x and an event y occurs any value u such that Q x y u 0 and C z y u 0 can be chosen The behavior of the system composed with the controller is then modelled as Q X Y U 0 C X Y U 0 xX P X Y U Q X 0 C X 0 Control objectives ensuring properties like invariance reachability attractivity etc are called tra ditional control objectives There are also other kinds of control objectives which can be expressed as partial order relations over the states of the PDS These are called optimization control objectives SIGALI provides functionalities for synthesis of controllers ensuring traditional as well as optimization control objectives There does not exist pre existing SIGALIfunctionalities Instead one have to load different libraries in which SIGALI functions are written 3 2 Loading of the necessary libraries For controller synthesis ensuring traditional control objectives the Synthesis 1ib file must be loaded e S c S_Invariance S prop or equivalently SSecurity S prop If prop encodes a set of states S_Invariance S prop computes a contr
10. ical systems systems and processes Systems are general dynamical systems in which null transitions basically self loops are taken into account even when all the signals are absent whereas in a process null transitions are excluded i e No transition can take place in the absence all the signals Dynamical systems can be automatically derived from either SIGNAL programs or Matou programs thus allowing to allowing the modeling of reactive systems by means of Mode Automata From a Signal Matou programs a file is automatically generated it contains the following data e events is a list of variables encoding the event variables e states is a list of variables which encodes the states variables e controllables is a subset of events and corresponds to the controllable event variables See section 3 for more details e evolutions is a list of polynomials one for each state variables which corresponds to the evolution of each state variables e initialisations is a list of polynomials the solutions of this polynomial systems correspond to the initial states of the system e constraints is also a list of polynomial encoding the constraints part of the polynomial dynamical system i e Q X Y 0 If one want to construct from these sets a process respectively a system the following command has to be used e syst processus events states evolutions initialisations constraints controllables Conversely if syst is a dynamical sys
11. is the duplicated cost function of C X where X_1 is for example obtained as follows Sigali gt duplicate_states declare _suff state_var S next one have to declare C_Dup i e same as for C but with the variables of the set duplicate_states Nb No automatic reordering gt set reorder 0 the variable order must be as follows X1 gt X1_1 gt X2 gt X2_1 So if you plan to use the functions of this library then never use the reodering after the use of declare_suff state_var S Once you plan not to use these functions any more then you activate again the automatic reordering The different functions of the Synthesis_ Partial_Order_Relation 1lib are Supervisor_Lower_than S C C_Dup duplicate_states gives access to a controlled system such that whatever the current position of the system S under control the supervisor will make the system evolve into the state x such that forall x reachable from the current position C x lt C Dup x Lower_than S C C_Dup duplicate_states build the controlled system idem for Supervisor_Greater_than S C C_Dup duplicate_states and Greater_than S C C_Dup duplicate_states ie C x gt C_Dup z idem for Supervisor_Striclty_Lower_than S C C_Dup duplicate_states and Striclty_Lower_than S C C_Dup duplicate_states ie C x lt C_Dup z idem for Supervisor_Striclty_Greater_than S C C_Dup duplicate_states and Striclty_Greater_than S C C_Dup duplicate_states ie C x gt
12. may take So each path from the root to a leaf assigns a unique sequence of values to the variables and the value of the leaf gives the value of the polynomial for that particular assignment For example if p is the polynomial a b c and the ordering is a lt b lt c then p is represented by SIGALI as follows The TDD representation of p is shown in Fig 6 subformula 0 b 1 c 0 1 cal 2 a2 2 o In order to avoid repetitions in listing portions occuring more than once are labelled as n n 0 1 2 These repetitions tend to occur when two or more edges enter a non leaf node in the TDD While reading the TDD the label subformula n wherever it occurs is to be replaced by the portion labelled n the command size P gives the number of nodes of the TDD that encodes the polynomial P Lists The list of polynomials equations etc are written as follows a b c d is a list of polynomials and a b x a d 2 b 2 is an equation system Of course a symbol can be assigned to a list or an equation system as well For example e list a b a b 0 1 e equations a 2 b 2 c a and b If p is a polynomial 1p1 and 1p2 are two lists of polynomials lvar1 and lvar2 are two lists of variables and lconst is a list of constants with values 0 1 or 1 then e eval p a b c 0 1 1 evaluates the polynomial p after substituting 0 1 and 1 for a b and c respectiv
13. mplementary list according to all the declared variable e L diff_lvar L_1 L_2 is equal to L1 L2 e given a list of variables L and a variable a belong_lvar a L is true whenever a L 1 2 3 Polynomials and equations Polynomials We can write polynomial expressions lists of polynomials etc All the usual polyno mial operations are also available For example the polynomial a b b is written a7 2 b b 2 A symbol can be assigned to a polynomial P a 2 b b 2 Note that the variables a b have to be declared first in order to specify this polynomial Now given a polynomial P over the variables L e varof P gives access to the variable set of P e nbvar P gives the number of variables of P e nb_solution P X gives the number of solution of the equation P X 0 where X is a set of variables that must contains varof P Representation of polynomials A variable or polynomial can only take values belonging to F3 1 0 1 In SIGALI a polynomial is represented by means of a Ternary Decision Diagram TDD which is an extension of a Binary Decision Diagram BDD In a TDD each non leaf node represents a variable and each leaf node is a value of the polynomial An arbitrary ordering of the variables must be done to facilitate the assignment of a node to a variable Further each non leaf node has 3 edges emanating from it labelled by the 3 possible values 1 or 2 0 1 that the corresponding variable
14. n f1 f 2 is such that Vz Z 37 amin fi x fe x min f x falx e amax f1 f2 is such that Yz Z 37 amax fi x fo x max fi x falx e apart P f1 f2 f3 build a cost function such that a_part P f1 2 3 x fl if P x 0 f2 if P x 1 and f3 if P x 1 8 e amargmin f Y given a cost function f defined over X UY a margmin f Y is a function say f over the variables X such that f X miny f X Y i e Vy f x lt f x y e amargmax same as a_margmin but with the max e P a_iminv f n is a polynomial such that P x 0 amp f x n e amaxim f is the minimum value taken by f and a_minim is the maximum value taken by f e P a_inf f n is a polynomial such that P x 0 amp f x lt n a sup is also defined e R a_cost2rel f1 f 2 Given two cost functions over X1 and X2 with the same cardinality a_cost2rel f1 f2 is a polynomial R X1 X2 such that R x1 2 0 amp f1 x1 lt f2 2 2 Verification of systems using SIGALI SIGALI provides certain functionalities for the verification of the properties of a dynamical system 2 1 Liveness Definition A dynamical system is alive iff Yx y such that Q x y 0 dy such that Q P z y y 0 In other words a system is alive iff it contains no sink states If syst is a system or a process then e alive syst is True if and only if syst is alive 2 2 Safety Properties 2 2 1 Invariance Definition A set of sta
15. oller that ensures the invariance of with respect to the system S The controlled system is the output of this function e S c S_Reachbale S prop If prop encodes a set of states E S Reachable S prop computes a controller that ensures the reachability of E from the initial states The controlled system is the output of this function To ensure the attractivity one have to use the S S_Attractivity S prop command For dealing with optimization control objectives two additional files Synthesis_Partial_order bib and Synthesis_Optimal_Control bib must also be loaded 10 e The file Synthesis_Partial_Order 1ib contains the definition of a function called S_Free_Max which helps in choosing a control such that the system evolves in the next instant into a state where the maximum number of uncontrollable events are admissible e The file Synthesis_Partial_Order_Relation 1lib contains function definitions for the synthesis of optimal controllers The goal is to synthesize a controller that will choose a control from amongst all the admissible controls in such a way that the system evolves into a state according to a given choice criterion This criterion is expressed as a cost function relation on the set of states Intuitively speaking the cost function is used to express priority between the different states that a system can reach in one transition Technical Restiction Input C X is the cost function used for the control C_Dup X_1
16. omials of p variables Given an element of Z 37 Z P Z1 Z2 Zp shortly P Z we associate its set of solutions Sol P C Z 37 def k Sol P 21 Ze Z 37 P z1 Ze 0 1 It is worthwhile noting that in Z 37 Z Z Z1 Z Zk evaluate to zero Then for any P Z Z 37 Z one has Sol P Sol P Z Z We then introduce the quotient ring of polynomial functions A Z Z 37 Z lt zr z gt where all polynomials Z Z are identified to zero written for short Z Z 0 A Z can be regarded as the set of polynomial functions with coefficients in Z 37 for which the degree in each variable is lower than 2 showed how to define a representative of Sol P called the canonical generator Our techniques will rely on the following For all polynomials P Po P Z 37 Z e Sol P C Sol P2 whenever 1 P P gt 0 inclusion e Sol P1 N Sol P2 Sol P p P2 intersection where Pi P I P2 P2 2 e Sol P1 U Sol P2 Sol P P2 union and Z 37 Sol P Sol 1 P complementary lEspresso Web Site http www irisa fr espresso 2Vertecs Web Site http www irisa fr vertecs 1 1 2 Dynamical systems Basics A dynamical system can be mathematically modelled as a system of polynomial equations over Z 3Z Z the Galois field of integers modulo 3 of the form Q X Y 0 Xx P X Y 3 Q X 0 where e X is the set of n state vari
17. tation Let g be a polynomial and V its set of solutions then the generator of the complement of V is obtained by e complementary g Intersection Let p1 and p2 be two polynomials and V1 and V2 be the corresponding set of solutions then e intersection p1 p2 is the canonical generator of Vi N V2 The number of arguments can be greater than 2 For example one can write intersection p1 p2 p3 p4 Union Let p1 and p2 be two polynomials and V1 and V2 be the corresponding set of solutions then e union p1 p2 is the canonical generator of Vi U V2 As in case of intersection the number of arguments can be greater than 2 Tests of inclusion Let p1 and p2 be two polynomials and V1 and V2 be the corresponding set of solutions then e subset g1 g2 is True if and only if Vi C V2 1 2 5 Existential universal variable elimination Given a polynomial P over the variables X Y then we define the Existential universal variable elimina tion as follows e P exist Y P is a polynomial such that Sol P x 3y P x y 0 e P forall X P is a polynomial such that Sol P a2 Vy P x y 0 1 2 6 Automatic reordering The set_reorder 1 exists also with the parameter 2 performs an automatic variable reordering using heuristics This is very useful to decrease the size of the TDD set_reorder 0 stops the automatic reordering 1 3 Systems and Processes SIGALI distinguishes between two categories of dynam
18. tem as described by 3 constructed by the command system or process then the 6 components of syst can be accessed by e event_var syst returns the event variable set of a system i e the vector Y e state_var syst returns the state variable set of a system i e the vector X e evolution syst returns the vector of polynomials encoding the evolution equations i e Pi X Y Pr X Y e initial syst returns the polynomial encoding the initial states of the systems e constraint syst returns the constrains polynomial Q X Y e controllable_var syst returns the controllable variable set of a system i e the vector U with U CY See section 3 for more details 1 3 1 Some special sets If g is the canonical generator of a set of states F then e pred syst g is the canonical generator of the set of predecessors of E e all_succ syst g is the canonical generator of the set of states such that all successors belong to E e adm_events syst g is the canonical generator of the set of events admissible in F If g is the canonical generator of a set of events F then e admstates syst g is the canonical generator of the set of states compatible with at least one of the events in F 1 3 2 Implicit System Starting from a system modeled as an PDS S as described in Equation System 3 for some particular analysis it is important to have access to the implicit corresponding implicit PDS of the form 4
19. tes E is invariant for a dynamical system iff for every state x in E and every event y admissible in x the successor state x P x y is also in E If syst is a dynamical system and g is the canonical generator polynomial of a set of states F e invariant syst g is True if and only if E is invariant for syst For example in case of the process doublem one can specify a property pr eq etat_1 etat_2 The invariance of this property can then be tested by the command e invariant pf gen pr_eq where pf is the process constructed by the command system 2 2 2 Invariance under control Definition A set of states E is control invariant for a dynamical system iff for every state x in E there exists an event y such that Q x y 0 and the successor state x P x y is also in E If syst is a dynamical system and g is the canonical generator polynomial of a set of states F e Invariant_under_control syst g is True if and only if E is control invariant for syst 2 2 3 Greatest control invariant subset Given a set of states E there exists a set F which is the greatest control invariant subset of If syst is a dynamical system and g is the canonical generator of E then e greatest_inv syst g e greatest_c_inv syst g gives the canonical generator of F 2 3 Reachability Properties 2 3 1 Reachability Definition A set of states E is reachable iff for every state x E there exists a trajectory st
Download Pdf Manuals
Related Search