Home

Model Repair via SAT Solving - AUB

1. SUI A sa that is s s a t iff s and t agree on all of the sub formulae and there is a transition from s to df t or vice versa and is the transitive closure of Saa We also define s t s tj Definition 13 Adjacency ignoring subformula abstraction Given a Kripke structure M So S R L AP and a CTL formula n we define an equivalence relation over S as follows e s t SUB s n AS SUB t N AS that is s s p t iff s and t agree on all of the sub formulae in AS Definition 14 Abstract model Let Given a Kripke structure M So S R L AP and a specification formula m we define the reduced model M M as follows 1 S s s S 2 So so so So s 4 8 2 e R 4 L S AP is given by L s L t That is the label consists of the atomic propositions if any that hold in all states of s 3 E O n Figure 15 Mutex abstraction by subformulae 25 Figure 16 Mutex repair of abstract by subformulae structure Consider the two process mutual exclusion structure M in Fig 3 with 7 A 69 and abstraction with respect to sub formula C1 C2 i e states that agree on the value of C1 C2 are considered equivalent By Definition 13 the equivalence classes of s p are none 1 N1N2 N1T2 TIN2 T1T2 C1N2 C1T2 N1C2 T1C2 and C2 C1C2 Fig 15 shows the resu
2. the execution of Repair M 7 Since the SAT solver is assumed to be sound V is actually a satisfying assignment for repair M 1 1 follows from Clause M is total of Def 8 2 holds by construction of M which is derived from M by deleting transitions and subsequently unreachable states For 3 let be an arbitrary state in Sj Since so was not deleted we have V X tt Hence by Clause 2 of Def 8 tt Hence by Th 2 so m Finally 4 follows from 1 3 and Def 5 Theorem 3 Completness If M is repairable with respect to m then Repair M 7 returns Kripke structure M Sj S R I AP such that M is total M C M and M S En Proof Assume that M is repairable with respect to 7 By Definition 5 there exists a total substructure MI 50 5 R HU AP of M such that S n We define a satisfying valuation Y for repair M T as follows Assign tt to E for every edge s t R and ff to every for every edge 8 4 Z Since M is total the is total section is satisfied by this assignment Assign tt to for all s 50 Consider an execution of the CTL model checking algorithm of Clarke Emerson and Sistla 11 for checking sg n This algorithm will assign a value to every formula o in 1 in every reachable state s of M Set V Xs to this value By construction of the model checking algorithm 11 these valuations will satis
3. CTL formula we define a propositional formula repair M 7 such that repair M 7 is satisfiable iff has a solution repair M is defined over the following propositions 1 Est s t R 2 X sc 5 3 Xsy s 5 0 sub n 4 86 5 0 n S and v sub m has the form A pV or Eloi The meaning of is that the transition s t is retained in the fixed model MI iff E is assigned tt true by the satisfying valuation V for repair M 1 The meaning of X is that state s is retained in the repaired model The meaning of Xs is that y holds in state s XT is used to propagate release formulae AV or EV for as long as necessary to determine their truth i e S in the worst case A satisfying assignment Y of repair M e g as given by a SAT solver gives directly a solution to model repair Denote this solution by model M V defined as follows Definition 7 model M V model M V So S R L AP where S s s SoA V X tt S s s AV AS tt R s t 81 RAVE tt L L S and AP AP Note that model M V does not depend directly on 7 Definition 8 repair M n Let M So S R L AP be a Kripke structure and CTL formula Let s t abbreviate s t is the conjunction of all the propositional formulae listed below These are grouped into sections where each section deals with one issue e g prop
4. Let be the set of atomic propositions corresponding to states including the start and all exit states Proposition 4 M X 4p Bu 37 Proof Construct a forward simulation f from M to By as follows A state of M that is in B is mapped to itself A state s of M that is not in is mapped as follows if startp is reachable from s then relate s to prep and if a state t is reachable from s along a path outside of B such that startpg is not reachable from t then relate s to postp Corollary 2 For any ACTL X formula f over AP p if By Ef then M E f Proof Follows immediately from Prop 3 and Prop 4 9 2 Verification of the coupling specification We define the abstraction BA of B as follows Definition 17 Abstract box Let Or be the subset of Og consisting of all exit states that reachable from The states of BA are startg intg U ie the start state all reachable exit states and a new state intg which represents the interior of B intg has the empty propositional labelling If B is acyclic then the transitions of BA are startg intg U intg s s ie there is a transition from the start state to the interior state and from the interior state to every reachable exit state If B contains cycles then we also add the transition intg intg i e self loop on intg which models the possiblity of remaining inside B forever The reachability proble
5. R gt V X Eav al 10 For case 2 we proceed as follows Let t be an arbitrary state such that s t R Then WA oV yj H we show that VG ale yj implies then we are done by CTL semantics The argument is essentially a repetition of the above argument for V X implies M s Ac Proceeding as above we conclude M t v and one of the same two cases as above M t Eo u E R VOCE Ava However note that in case 2 we are counting down Since we count down for n S then along every path starting from s either case 1 occurs which terminates that path as far as valuation of 2 0 is concerned or we will repeat a state before or when the counter reaches 0 Along such a path from s to the repeated state v holds at all states and so o Vv holds along this path We conclude that V holds along all paths starting in s and so M s 4 Right to left i e follows from s Assume that M s Ale holds Hence E y A pv 190 gt M t A gVV By the induction hypothesis V Aqiss 5 gt M t E A gVv We now have two cases 1 V X Since we have we conclude ajpvy and so we are done 2 Aus 5t gt M t AleV For case 2 we proceed as follows Let t be an arbitrary state such that 5 1 Then M t E A
6. 26 F3 SB1 amp SA2 F5 EA1 amp 2 E Fl SB1 amp SA2 F4 5 1 6 SA2 Figure 17 Barrier synchronization abstraction by subformulae F3 d 5 1 amp SA2 SRI S SA NA NA NA Y KR 5 RK Au EAL amp EB2 P cUm ANA ie a M Z n 2 7 NA Ka M SB1 amp SA2 Ke ANA NA NA NA NA E SS S 4 ki Figure 18 Barrier synchronization repair of abstract by subformulae structure 27 OE TEN S s q t s3 y SALSB2 7 TT oe pee a lt S6 SA1 EB2 EA1 EB2 ant 3 2 I S12 A 1 I x EBLEA2 r 59 1 5 2 515 1 2 511 581 582 Figure 19 Barrier synchronization concretization of repaired abstract by subformulae struc ture 8 Repair of Concurrent Kripke Structures We consider finite state shared memory concurrent programs P Stp P Px consisting of sequential processes Pi running in parallel together with a set Stp of starting global states For each P there is a finite set AP of atomic propositions that are local to only can change the value of atomic propositions in AP Other processes can read but not change these values Local atomic propositions are not shared 0 when i Z j We also admit
7. Eshmun checks the validity of ng v n by using the CTL decision procedure of 16 we check satisfiability of Y n By Th 4 we conclude that M E n 39 C timeout D negAck tmt nack Figure 27 Repaired box Bu for a single phone call Figure 28 Initial structure M for phone call example 40 Figure 29 Repaired structure M for phone call example 10 Overview of our Implementation The Eshmun Tool Eshmun is written in Java and uses the javax swing library for GUI functionality Graphviz 14 for Kripke structure visualization and SAT4jSolver 24 to check satisfiability Eshmun is an interactive GUI tool it allows users to create a Kripke structure M by adding states and transitions Users then enter a CTL formula 7 and proceed to repair M Users can mark a transition as non deletable by checking the retain button This is essential for example in preventing the deletion of transitions of the abstract box B4 Eshmun implements abstraction and will show the abstract structure the repair on the abstract structure and the concretization of this repair back to the original structure It also implements the CTL decision procedure 16 for checking validity of y 7 in hierarchical repair 10 1 Experimental results Table 1 gives experimental results for repairing mutual exclusion w r t safety and also barrier synchronization The structures used were generated by a Python pr
8. Figure 1 presents our model repair algorithm Repair M v which we show is sound and complete provided that a complete SAT solver is used Recall that we use model M Y to denote the structure derived from the repair of M w r t 1 as per Def 7 Theorem 2 Soundness Let M So S R L AP be a Kripke structure CTL formula and n S Suppose that repair M T is satisfiable and that V is a satisfying truth assignment for it Let M S9 S R AP Then for all reachable states s 5 and CTL formulae lt sub n V Xs tt iff M s EE Proof We proceed by induction on the structure of We sometimes write instead of tt and instead of V X ff Case tt iff case condition V Xs y tt iff Clause 6 propositional consistency of Def 8 V Xs y ff if induction hypothesis not M s iff CTL semantics M s y iff case condition M 5 Case v DO o tt iff case condition VU yvy tt iff Clause 6 propositional consistency of Def 8 V Xs 2 tt or V Xs y tt iff induction hypothesis M s or M s v iff CTL semantics M s v iff condition M s Case tt iff case condition V X tt iff Clause 6 propositional consistency of Def 8 tt and y tt iff D induction hypothesis
9. X sn X5 AGpVAGq AEXp X s AGpVAGq AEXp Xs AGpvAGq Xs EXp Xs AGpVAGq Xs AGp V Xs AGq We start by solving for X Xs AGp X X3 acp Xs p A Est gt X acp Esu gt X x Aen Xip Ets gt X AGp XZ AGp Xup A Eus gt X acp 3 X acp Xtp ff AGp Xup tt u A Est gt X acp Esu lt gt By replacing Xs p etc by their truth values we can simplify the above as follows It is more intuitive to work bottom up X1 AGp mE E gt X3 X AGp Eu gt E Aaen Es Esu gt X2 AGp XS acp Esu gt Eus gt 7E st Xs AEs t 13 Symmetrically we have Xs AGq It remains to solve for X Exp Xs Exp Esa V By replacing X and Xup by their values we get X Exp Est ff V Esu A tt Esu Therefore we now can solve for Xs producing Xs ES V SER A Esu ES A Esu The above solution implies that Repair M will remove the edge s t and all the resulting unreachable states as shown in Fig 2 Note that for 7 AGp V AGq we obtain Xs Es V u which admits two satisfying valuations i e removing either 8 4 or s produces the needed repair 5 Examples of Repair 5 1 Mutual exclusion safety We treat the standard two process mutual exclusion example in which P i 1 2 cycles through three states
10. how to automatically modify the program or circuit so that the specification is satisfied There appears to be no automatic repair method that is 1 complete i e if a repair exists then find a repair for a full temporal logic e g CTL LTL and 2 repairs all faults in a single run i e deals implicitly with all counterexamples at once For example Jobstmann et al 22 considers only one repair at a time and their method is complete only for invariants In Staber et al 26 the approach of Jobstmann et al 22 is extended so that multiple faults are considered at once but at the price of exponential complexity in the number of faults In Buccafurri et al 9 the repair problem for CTL is considered and solved using abductive reasoning The method generates repair suggestions that must then be verified by model check ing one at a time In contrast we fix all faults at once Zhang and Ding 29 present a model repair method which they call model update based on a set of five primitive update opera tions add a transition remive a transition change the propositional labeling of a state add a state and remove an isolated state one that has no incident transitions They also present a minimum change principle which essentially states that the repaired model retains as much as possible of the information present in the original model Their repair algorithm runs in time exponential in 7 and quadratic M Th
11. neutral preforming local computation tryng requested the critical section and critical inside the critical section P has three atomic propositions Ni Ti Ci In the neutral state Ni is true and Ti Ci are false In the trying state Ti is true and Ni Ci are false In the critical state Ci is true and Ni Ti are false The CTL specification 7 is AG C1 C2 i e and P gt are never simultaneously in their critical sections Figure 3 shows an initial Kripke strucure M which violates mutual exclusion and Fig 4 shows a repair of M w r t AG 2 C1 C2 Our tool shows the transitions to be deleted to effect the repair as dashed Initial states are colored green and the text atached to each state has the form name pi p amp where name is a symbolic name for the state and pi pa is the list of atomic propositions that are true in the state In Fig 4 the violating state C1 C2 is now unreachable and so AG C1 C2 is now satisfied This repair is however overly restrictive as follows If remains forever in its neutral state it is not possible for P gt to cycle indefinitely from neutral to trying to critical and vice versa This should be possible in a good solution to mutual exclusion Moreover whenever P5 enters the critical section it must wait for P to subsequently enter before it can enter again We show in the sequel how to improve the quality of the repairs 14 Figure 3 Mutex init
12. 290 2002 B Jobstmann Griesmayer and R Bloem Program repair as a game In CAV pages 226 238 2005 R Ladin B Liskov L Shrira and S Ghemawat Providing high availability using lazy replication ACM Transactions on Computer Systems 10 4 360 391 Nov 1992 Daniel Le Berre Anne Parrain et al The sat4j library release 2 2 system description Journal on Satisfiability Boolean Modeling and Computation 7 59 64 2010 S Shoham and O Grumberg A game based framework for ctl counterexamples and 3 valued abstraction refinement In CAV pages 275 9287 2003 5 Staber B Jobstmann and R Bloem Diagnosis is repair In Intl Workshop on Principles of Diagnosis June 2005 S Staber B Jobstmann and R Bloem Finding and fixing faults In CHARME 05 2005 Springer LNCS no 3725 C Stirling and D Walker Local model checking in the modal mu calculus Theor Comput Sci 89 1 1991 Yan Zhang and Yulin Ding Ctl model update for system modifications J Artif Int Res 31 1 113 155 Jan 2008 4T 5 6 propagate s if old s then has already been processed new s new s 6 return Dalready checked for larger index if A g Vu and old s for some m gt m then new s new s 6 return already checked for larger index if E oV4 and old s for some m gt m then new s new s 6 return case has not
13. 35 1 86 7 25 Dining Phil 0 48 0 59 0 67 0 74 0 81 1 20 Table 2 Times in seconds to repair given concurrent programs 10 2 Main modules The following is a concise definition of our tool s main modules e CTL Parser parses a CTL formula to generate a CTLParsed Tree object which is tree data structure representing e User Interface implements GUI interface between user and the other modules Model Checker takes as input a Kripke structure M So S R L AP and CTL formula and verifies if M satisfies e Model Repairer takes as input a Kripke structure M and a CTL formulae and return a repaired model with respect to d e Model Optimizer reduces the state space of created Kripke structures It implements the abstraction methods in section 7 e SAT Solver takes as input a CNF file and return a flag that specifies whether the CNF formulae is satisfiable or not In case it is satisfiable it also returns the satisfying valuation e Decision Procedure this module implements the CTL decision procedure given in 16 42 slope 2 Mutex e Dining Phil 100 seconds 100 0 1 0 01 5 10 15 20 25 50 Figure 30 Repair time for given programs Array of Characters CTL Parser CTLParsedTree Model Checker True False GUI Repair frml Krioke amp CTL Model Repairer User Interface SA
14. 5 3 Barrier synchronization In this problem each process P is a cyclic sequence of two terminating phases phase A and phase B i 1 2 is in exactly one of four local states SAi EAi SBi EBi correspond ing to the start of phase A then the end of phase A then the start of phase B and then the end of phase afterwards cycling back to SAi The CTL specification is the conjunction of the following 1 Initially both processes are at the start of phase SA1 SA2 2 P and P gt are never simultaneously at the start of different phases 8 1 SB2 AG 2 SA2 SB1 3 P and P gt are never simultaneously at the end of different phases 1 EB2 2 EB1 2 and 3 together specify the synchronization aspect of the problem P can never get one whole phase ahead of P gt and vice versa 18 The structure in Figure Fig 9 violates the synchronization rules 2 and 3 Our implementa tion produced the repair shown in Fig 10 S9 1 5 2 4 DU que EB2 EE ue 5 2 TA Adi Figure 9 Barrier syncrhonization initial structure 19 Eme ms SALEB2 1 5 2 1 VOS Bee Ze 512 1 X EB1 EA2 r _ _ I 24 211 4 59 1 5 2 515 1 2 MELOS rm a S14 4 Se s EB1 SB2 Figure 10 Barrier syncrhonization
15. M if V zj We show that K n Since V is satisfying assignment we have Au V ai V V bi V V ci Without loss of generality assume that tt similar argument for V b tt and Viel tt We have two cases Case 1 is a xj Then V z tt so s t Also since a 2 p AG p Since s t R M so p Hence M so ku Case 2 is a z Then ff so s t Also since a j ql AG p Since s t R M so Hence M so H n f is satisfiable follows from can be repaired Let 90 S L AP be such that C M M so We define a truth assignment V as follows V xj tt iff sj t We show that V f tt i e V a V V b V V ci for alli 1 n Since M so n we have M so el V v2 v v for all i 1 n Without loss of generality suppose that M so vl similar argument for y and M so v2 We have two cases Case 1 is a 2 Then y AG p Since MI so y we must have s t Hence V zj tt by definition of V Therefore V a tt Hence V V bj Hie Case 2 is a z Then AG p Since MI an el we must have s t Hence V x ff Therefore V a tt Hence Y a V V b V Y c 4 The Model Repair Algorithm Given an instance of model repair M n where M So S R L AP and 7
16. M s and iff gt CTL semantics M s v iff condition M 9 Case 6 tt iff case assumption V X axy tt iff Def 8 Aus V Est gt Arel tt iff boolean semantics of gt Aust 2 tt gt V X tt iff s reachable by assumption implies t isreachable and apply ind hyp Pasa 2 cem M t q iff C R so restriction of t to t s gt t i e t s t R does not matter M s iff case assumption Mie F Case tt iff gt case assumption VU Exp tt iff gt Def 8 Visor V Es A tt iff boolean semantics of Visor V Esa tt AV Xt p tt iff gt t is reachable from s by assumption and apply ind hyp Va 5 o iff gt C R so restriction of t to t s gt t i e t s t R does not matter M s EX iff gt assumption M E Case A pVw We do the proof for each direction separately Left to right i e implies s E A e Vu iff Def 8 1 Def 8 LE V Ju Esa iff Y is a boolean valuation function and so distributes over boolean connectives V Le Va gt VGL v if induction hypothesis M s E 9 P eV 8 0 R We now have two cases 1 Ky In this case M s H A e Vw and so M s E 2 Ag t
17. R1x WT R2x _ I 7 t18 t20 X SNT R1x ST R2x Figure 23 Repaired pair structure for R1x R2x 34 ul WT_R1x IN_R2y DN RIxN R2y A lt SNT RIx WT R2y _ x WT_R2y u6 EN E ____ IN_R2y u Ux lt 1 lt I I ne u10 i 1 lt 2 SNT RIXIN R2y MA e ull 1 ST R1x WT R2y 1 1 i aS kapuy OE I I C u I ae I _ _ IN_R1x ST_R2y yY VIN pod u15 e I I I u16 ST R1x DN R2y i I I Cd 19 SNT_R1x DN_R2y u22 u24 SNT_R1x SNT_R2y Figure 24 Repaired pair structure for R1x R2y 35 IN_R1x SNT R1x Cx WT Ox WT Cx amp WT Cx 9 WT IN R2x WT R2x DN R2x om R2x WT R2x e DN R2x 9 IN R2x o WT R2x DN R2x ST Rox IN R2y WT R2y DN R2y DN R2y DN R2y N Ris T_R1x IN_R1x 6 ST_R1x IN_R1x 6 ST_R1x ST R1x R2x T_R2 N R2x IN_R1x 6 WT R1x WI Ris SNT_R1x SNT_R1x R2y T R2 N R2y T R2y Figure 25 ESDS Program E MO e 2 A finite set D of boxes or supernodes The sets N and B are all pairwise disjoint 3 An initial node start Nj 4 A subset O of Ni called exit nodes 5 A labeling function X N 2 that labels each node with a subset of P 6 An indexing function Y B i 1 that maps each box of the i th structure to an in
18. a set SH x m of shared variables These can be read written by all checks that processes and have values from finite domains We define the set of all atomic propositions AP AP U UAPx Each P is a synchronization skeleton 16 that is a directed multigraph where each node is a local state of P which is labeled by a unique name s and where each arc is labeled with a guarded command 13 B A consisting of a guard and corresponding action A We write such an arc as the tuple s B Aj 57 where s is the source node and 5 is the target node Each node must have at least one outgoing arc i e a synchronization skeleton contains no dead ends The read write restrictions on atomic propositions are reflected in the syntax of processes for an arc s B gt Aj s of P the guard is a boolean formula over AP and the action Eshmun all shared variables are boolean i e atomic propositions that are not local to any process 28 A is any piece of terminating pseudocode that updates only the shared variables SH Let 5 denote the set of local states of P There is a mapping V S gt AP true false from local states of P to boolean valuations over AP for pj AP Vi si p is the value of atomic proposition p in s Hence as P executes transitions and changes its local state the atomic propositions in are updated since V s Z V s in general A glo
19. been processed new s new s U ae 6 new s new s U v Y conjoin X yvy Xs V C new s U v Y conjoin X X AXy forall t R s nett new t U py endfor conjoin Aue gr Est gt Anel EXy forall t R s nett new t U p endfor conjoin Vie pa Est Xt A o Vv new s new s U A pVy X at vay AlpVy m 1 n new s new s U y v forall t R s neu t new t U A pgVv 1 conjoin X s Lea V Are Sid Est gt Xfaipvy new s new s U v conjoin X X E e Vw new s new s U ElgVv Y conjoin X XT tov E ElpVy m 1 nk new s new s U y v forall t R s neu t 2 new t U A gVv 1 conjoin X ei vy Xen Xs V Vieni Est XT elev new s new s U v conjoin X p y Xs endcase new s new s amp D remove from new since it has been processed old s old s U k gt that has been processed Figure 33 Formula propagation 48 InitializeRepairFormula M n true conjoin V es Xs forall s So conjoin X gt forall s 5 co
20. of 22 Both and are equivalence relations over 5 and they also preserve the values of all the atomic propositions in 7 Hence we can define a quotient of M by these relations as usual Definition 11 Abstract Model Let pa p Given a Kripke structure M So S R L AP and a specification formula we define the abstract model M So S R L AP M as follows i S ja lees so So s 14 0 R S 5 AP is given by L s L s AP amp 2 8 4 t oa 1 2 P 1 2 Figure 12 Mutex bad repair of abstract by label structure 1 2 1 2 Figure 13 Mutex good repair of abstract by label model 23 Figure 14 Mutex concretization of repaired abstract by label structure Consider the two process mutual exclusion structure M in Fig 3 with 7 62 and abstraction by label i e states that agree on both C and are considered equivalent By Definition 10 the equivalence classes of are none 1 N1N2 N1T2 T1N2 T1T2 C1 C1N2 C1T2 C2 N1C2 T1C2 C1 C2 C1C2 Fig 11 shows the resulting abstract structure M which has four states corresponding to these equivalence classes Fig ure 12 presents a repair of M recall that transitions to be deleted are shown dashed This is not a good repair since the state C2 has been made unreachable so that process 2 cannot now ever enter its crit
21. of the Proposition 2 The length of grCon A e Tepair ny is x IMP x n M x ent Km where I is the number of pairs M is the size states transitions of the largest pair structure M and n is the length of the largest pair specification nij 31 Hence provided that the SAT solver remains efficient we can repair a concurrent program P Stp Px without incurring state explosion complexity exponential in K 8 1 Example eventually serializable data service The eventually serializable data service ESDS of Fekete et al 17 and Ladin et al 23 is a replicated distributed data service that trades off immediate consistency for improved efficiency A shared data object is replicated and the response to an operation at a particular replica may be out of date i e not reflecting the effects of other operations which have not yet been received by that replica Operations may be reordered after the response is issued Replicas communicate to each other the operations they receive so that eventually every operation stabilizes i e its ordering is fixed w r t all other operations Clients may require an operation to be strict i e stable at the time of response and so it cannot be reordered after the response is issued Clients may also specify in an operation x a set x prev of operations that must precede x client specified constraints CSC We let O be the countable set of all op
22. repaired structure Extensions of the Repair Algorithm We now present several extensions to the subtractive repair algorithm given in the previous section 6 1 Addition of States and Transitions The subtractive repair algorithm performs repair by deleting states and transitions In some cases it may be useful to add states and transitions e g as shown in the mutual exclusion example in Sect 5 2 Currently we can do this manually in Eshmun leading to an experimen tal interactive method for adding states and transitions A useful boundary case illustrated in the sequel is to add all possible transitions and then repair When the structure we are repairing is a Kripke multiprocess structure see Sect 8 the number of transitions tends to be linear in the number of states rather than quadratic and so this is not as burdensome as it seems 20 6 2 Repair of propositional assignments By omitting Clause 5 from Def 8 we remove the constraint that propositional labellings must be preseved This allows these labelings to be updated as part of the repair 6 3 Generalized Boolean Constraints on Transition and State Deletion We can prevent the deletion of a particular transition say from state s to state t by conjoining to repair M n This is useful for tailoring the repair and preventing undesirable repairs e g repairs that prevent a process from requesting a resource More generally we can conjoin arbitrary boolean fo
23. two have not yet resolved the truth of eu along the path in question To carry out the expansion correctly we use a version of X aj yy that is superscripted with an integer between 0 and n This imposes a well foundedness on the propositions and prevents for example a cycle along which holds in all states and yet the X aj vyj are assigned false in all states s along the cycle Finally Clauses 1 and 2 of Def 2 can be dealt with by viewing true as an abbreviation of p V p for some p AP and false as an abbreviation of p p for some p AP so they reduce to other clasues Note that the above requires all states even those rendered unreachable by transition deletion to have some outgoing transition This extra requirement on the unreachable states does not affect the method however since there will actually remain a satisfying assignment which allows unreachable state to retain all their outgoing transitions if some M C M exists that satisfies For s unreachable from so in assign the value to that results from model checking E This gives a consistent assignment that satsifies repair M n Clearly A does not affect Aa since s is unreachable from so Proposition 1 The length of repair M y is O S x n x d S x AP where S is the number of states in S R is the number of transitions in R n is the length of m AP is the numebr of atomic propositions in AP
24. used e repair M 1 a string which accumulates the repair formula which is being computed e 5 a subset of sub r Contains the formulae which have been propagated to s and whose truth in s affects the truth of 7 in so e marked s a boolean array initially all false An entry is set to true when formula s has been processed Figure 32 gives the overall algorithm ComputeRepairFormula We initialize repair M 9 by invoking InitializeRepairFormula which sets repair M 7 to the conjunction of Clause 2 5 of Definition 8 These clauses do not depend on the transitions in M and so can be computed with out traversing M Figure 33 gives the propagation step propagate which propagates formulae from the label of s to the labels of the sucessor states t R s of s When a propagation is performed propagateinvokes conjoin given in Figure 35 which updates repair M according to Definition 8 by conjoining the appropriate clause ComputeRepairFormula repair M ai InitializeRepairFormula M m forall so 50 new s m endfor Gm must hold in all initial states repeat until no change select some state s in M and some new s propagate s Figure 32 The model repair algorithm 11 Related Work The use of transition deletion to repair Kripke structures was suggested in Attie and Emerson 5 6 in the context of atomicity refinement a large grain concurrent program is r
25. whose guard holds and execute the corresponding action Using means we have at most one arc in each direction between any pair of local states To avoid clutter in the figures we replace B by just i e we omit empty actions In principle then we can repair a concurrent program by 1 generating its GSTD M 2 repairing M w r t 1 to produce and 3 extracting a repaired program from M In practice however this quickly runs up against the state explosion problem the size of M is exponential in the number of processes We avoid state explosion as follows In 2 4 an approach for the synthesis and verification of concurrent programs based on pairwise composition 29 N2 e T2 C2 N26 2 N2 T29 C2 c N2 6T206C2 P E N19T1 E T L 1 Figure 20 Concurrent program extracted from Fig 14 is presented for each pair of processes P that interact directly we provide a pair structure S Sij Rij Lij AP ij which is a multiprocess Kripke structure over P and Pj defines the direct interaction between processes P and P Hence if P interacts directly with a third process PX then a second pair structure Si Sik Rik Lik AP ix over P Pk defines this interaction So and Ma have the atomic propositions AP in common Their shared atomic propositions are disjoint The pairs of directly interacting processes are given by an in
26. y means that formula is true in state s of structure M and M s v means that formula is false in state s of structure M We define inductively as usual 1 M s true 2 s false 3 M s E p iff p L s where atomic proposition p AP 4 E e iff Mis 5 o v iff M s v and v 6 7 M s AXo iff for allt such that s t R M t 8 EXy iff there exists t such that s t R and M t 9 AlpVy iff for all fullpaths so s1 starting from s so Vk 20 Vj k M s Ay implies M sk Ew 10 M s iff for some fullpath 81 starting from s so Vk 20 Vj k M sj v implies v We use M E to abbreviate M 90 We introduce the abbreviations A QUv for for A yV for A trueUg EFy for E trueUg for AlfalseV cl for E falseVy Definition 3 Formula expansion Given a CTL formula q its set of subformulae sub y is defined as follows e sulpAw pAW U sublo U subl e sub q V ib pV vU sublo U e sub AXy U sub y e VA co m X SC lI m X 6 e Cp S 3 Model Repair Problem Given Kripke structure M and a CTL formula 7 we consider the problem of removing parts of M resulting in a substructure such that Definition 4 Subst
27. AP be a set of atomic propositions including the constants true and false We use true false as constant propositions whose interpretation is always the semantic truth values tt ff respectively The logic CTL 15 16 is given by the following grammar true false e e v e V e AXo EXy AlpVy where p AP and true false are constant propositions with interpretation tt f f respectively i e syntactic true false respectively The semantics of CTL formulae are defined with respect to a Kripke structure Definition 1 A Kripke structure is a tuple M So S R L AP where S is a finite state of states Sy C S is a set of initial states RC S x S is a transition relation and L S 2 P is a labeling function that associates each state s S with a subset of atomic propositions namely those that hold in the state State t is a sucessor of state s in M iff s t R We assume that a Kripke structure So S R L AP is total i e Vs S ds 5 s s R A path in M is a finite or infinite sequence of states 80 81 such that Vi gt 0 R fullpath is an infinite path A state is reachable iff it lies on a path that starts in an initial state Without loss of generality we assume in the sequel that the Kripke structure M that is to be repaired does not contain any unreachable states i e every s S is reachable Definition 2 M s
28. M 7 where M sg S R L AP S 80 81 5m t1 t and R 80 1 80 m 91 t1 m tm Le transitions from so to each of s1 Sm and a transition from each s to t for i 1 m The underlying set AP of atomic propositions is pi Pm q1 qm These propositions are distinct from the 21 used in the 3cnf formula f L is given by L so e L s p where 1 lt j lt m e L t q where 1 lt j lt m 1 is given by n A ei Ve v el 1 lt i lt n where e if a z then y AG p gt EXq e if a z then o AG p gt AX q e if b z then y AG p EXg e if b 72 then y AG p e if c z then AG p EXq e if c then 3 AG p gt AX q Thus if a 2 then the transition from s to t which we write as s t must be retained in and if a x then the transition s t must not appear in M It is obvious that the reduction can be computed in polynomial time It remains to show that f is satisfiable iff M T can be repaired The proof is by double implication f is satisfiable implies that can be repaired Let V 21 m gt tt ff be a satisfying truth assignment for f Define R as follows R so si si si 6 ti 1 lt d m U s ti V a tt i e the transition s t is present in M if V z tt and s t is deleted in
29. Model Repair via SAT Solving Paul Attie Kinan Dak Al Bab Mohamad Sakr Jad Saklawi Ali Cherri Department of Computer Science American University of Beirut paul attie aub edu lb kmdi4Qaub edu lb misi4 mail aub edu jad saklawi gmail com ahc14 mail aub edu June 22 2015 Abstract We consider the model repair problem given a finite Kripke structure M and a CTL formula 7 determine if M contains a substructure that satisfies 7 Thus M can be repaired to satisfy n by deleting some transitions We map an instance 1 of model repair to a boolean formula repair M 1 such that M T has a solution iff repair M n is satisfiable Furthermore a satisfying assignment determines which states and transitions must be removed from M to generate model of 7 Thus we can use any SAT solver to repair Kripke structures Using a complete SAT solver yields a complete algorithm it always finds a repair if one exists We also show that CTL model repair is NP complete We extend the basic repair method in two directions 1 the use of abstraction mappings i e repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M and 2 repair concurrent Kripke structures and concurrent programs we use the pairwise method of Attie and Emerson to represent and repair the behavior of a concurrent program as a set of concurrent Kripke structures with only a quadratic increase in the size of the rep
30. N1 T2 gt T1 T2 are now non deletable Removing either of T1 C2 gt T1 N2 or C1 T2 gt N1 T2 leaves T1 C2 C1 T2 respectively without an outgoing transition so is no longer total Hence we have to remove both T1 T2 T1 C2 and T1 T2 C1 T2 which leaves T1 T2 without an outgoing transition The problem is that in T1 T2 there is no notion of priority which process should enter first We can add this by adding a new proposition the usual turn variable to record priority among and P effectvely splitting T 1 T2 into two states This is a kind of repair that involves enlarging the domain of the state space which is different from adding a state over the existing domain which some repair methods currently do 10 29 Extending our method and tool to automate such repair is a topic for future work but we note that manual interaction and semantic feedback are helpful here and an initial step is to provide information about the reasons for the failure of a repair ke 2 N1 T2 7 I I I TLC2 N 7765 Ly NL C2 Figure 5 Mutex overconstrained repair 16 Figure 6 Mutex unrepairable due to retained request transitions Figure 7 Mutex only P is live 17 S1 T1 N2 53 C1 N2 7 P 2 N x 4 4 727 NM d NN o d NN SN 4 d nig 58 C1 C2 Figure 8 Mutex live solution
31. T Solver True False Deleted Trans Model Optimizer Krioke amp CTL Reduced Kripke True False frml Decision Procedure Figure 31 Tool main modules 43 10 3 Pseudocode for computing repair M m Figure 33 gives pseudocode for our algorithm to compute repair M from M So S R L AP and m The algorithm operates as follows We introduce a label s for each state s in M L s is a subset of sub 7 Initially so 7 and s 0 for all s 5 so The algorithm propagates formulae from the label of some state s to the labels of all successor states t of s This propagation is performed according to Definition 8 so that if for some CTL formula yp s and Definition 8 requires that some other CTL formula w related to be evaluated in every successor t then we add v to L t For example suppose A yVy s Then for every successor t of s we must add v and A yVy to L t Note that for each s we propagate at most one formula to the successors of s Once s has been processed in this manner we mark it so that we do not repreat the propagation We introduce a boolean array marked s for this purpose When a propagation is performed the appropriate conjunct is added to For the release modality we include the index with the propagated formulae so that we can count down properly We summarize the data structures
32. abstractions that are not necessariy correctness preserving since we can in many cases obtain larger reductions in the size of the structure than if we used only correctness preserving abstractions 7 1 Abstraction with respect to atomic propositions In order to abstract our model with respect to atomic propositions we start by defining two equivalence relations p and p Let be the set of atomic propositions that occur in n The first equivalence relation represents an abstraction strategy which takes adjacency of states into consideration Definition 9 Adjacency respecting propositional abstraction p Given a Kripke structure M So S R L AP and CTL formula n we define an equivalence relation over S as follows e spat L s n AP L t n AP s t Rv t s R at a mot S pat pa that is 8 t iff s and t agree on all of the atomic propositions of m and there is a transition from s to t or vice versa and p a is the transitive closure of Sne The next equivalence relation ignores adjancency of states This can result in the removal of existing cycles or the introduction of new ones Definition 10 Adjacency ignoring propositonal abstraction p Given a Kripke structure M So S R L AP and a specification formula we define an equivalence relation p as follows eszyt L s N AP L t n AP that is s p t iff s and t agree on all of the atomic propositions
33. air formula 3 repair hierarchical Kripke structures we use a CTL formula to summarize the behavior of each box and CTL deduction to relate the box formula with the overall specification 1 Introduction and Motivation Counterexample generation in model checking produces an example behavior that violates the formula being checked and so facilitates debugging the model However there could be many counterexamples and they may have to be dealt with by making different fixes manually thus increasing debugging effort In this paper we deal with all counterexamples at once by repairing the model we present a method for automatically fixing Kripke structures with respect to CTL 16 specifications Our contribution We present a subtractive repair algorithm fix a Kripke structure only by removing transitions and states roughly speaking those transitions and states that cause violation of the specification If the initial state is not deleted then the resulting structure satisfies the specification We show that this algorithm is sound and relatively complete An advantage of subtractive repair is that it does not introduce new behaviors and thus any missing i e not part of the formula being repaired against conjuncts of the specification that are expressible in ACTL 18 i e CTL without the existential path quantifier are still satisfied if they originally were Hence we can fix w r t incomplete specificati
34. ally chooses a repair from those available according to the valuation returned by the SAT solver This repair may be undesirable as it may result in restrictive behavior e g alternate entry into the critical section By constructing an abstract structure which for example tracks only the values of we obtain better repair which removes only the transitions that enter C1C2 We introduce four types of abstraction 21 1 abstraction by label preserves the values of all atomic propositions in n 2 abstraction by label with state adjacency preserves the values of all atomic propositions in and also preserves adjacency of states 3 abstraction by formula preserves the values of a user selected subset of the propositional subformulae of 7 4 abstraction by formula with state adjacency preserves the values of a user selected subset of the propositional subformulae of 7 and also preserves adjacency of states Two states are adjacent iff one is the successor of the other We define these abstractions as equivalence relations over the states of M The abstract structure is obtained as the quotient of M by the equivalence relations We provide a concretization algorithm Sect 7 3 which maps the repair of the abstract structure back to the original concrete structure to produce a possible repair of the original structure Since the resulting repair can always be model checked at no significant algorithmic expense we use
35. and d is the outdegree of M i e the maximum of the number of successors that any state in M has Proof repair M 7 is the conjunction of Clauses 1 8 of Def 8 We analyze the length of each clause in turn 1 Clause 1 O S since we have the term X for each so So and 50 C 9 2 Clause 2 O S since we have the term Xs for each s S Clause 3 O S x d since we have the term Xs V4 Es X for each s 9 4 Clause 4 O R since we have the term Est X X for each s t R 5 Clause 5 O S x AP since we have either or for each s S and p AP 6 Clause 6 O S n since we have one of X 5 V Xs Xs onp Xs Xs for each s S and each formula in sub r whose main operator is propositional and sub 7 is in O n Clause 7 O S x n x d since we have a term of size O d namely either Xs axy Au Es gt Arel Xsgxo Vg uasa for each formula in sub 7 whose main operator is either AX or EX 8 Clause 8 O S x n x d since the second S term is due to the superscripts m 1 S Each of these formulae has length O d The sum of lengths of all these formulae is O n x S x Summing all of the above we obtain that the overall length of repair M p is O n x d S x AP R Clearly repair M can be constructed in polynomial time
36. are straightforward We make the simplifying technical assumption that there is a bijection between states and propositions so that each proposition holds in exactly its corresponding state and does not hold in all other states This amounts to an assumption of alphabet disjointness between M and B M invokes B by entering startg and B returns a result by selecting a particular exit state T his assumption then amounts to an information hiding principle for hierarchical Kripke structures 9 1 Verification of the box specification To infer ng from gp we construct a version of which reflects the impact on B of being placed inside M We call this By the M situated version of B Definition 16 M situated version of B The M situated version of denoted Bm is as follows Include all the states and transitions of B Add two interface states prep abd postp Add a transition from preg to startp the start state of and a transition from every s i e every exit state of to If in M there is a path from some s back to startp then add a transition from postp to preg If in there is a path from the start state of M to an exit state of M such that does not enter B then add a transition from preg to postp preg represents all states of M from which the start state of is reachable postg represents all states of M that are reachable from some exit state of B
37. at repair M n is satisfiable iff M contains a substructure that satisfies 7 Furthermore a satisfying assignment for repair M 1 determines which transitions must be removed from M to produce M Thus a single run of a complete SAT solver is sufficient to find a repair if one exists Soundness of our repair algorithm means that the resulting M if it exists satisfies 7 Com pleteness means that if the initial structure M contains a substructure that satisfies 7 then our algorithm will find such a substructure provided that a complete SAT solver is used to check satisfaction of repair n While our method has a worst case running time exponential in the number of global states this occurs only if the underlying SAT solver uses exponential time SAT solvers have proved to be efficient in practice as demonstrated by the success of SAT solver based tools such as Alloy NuSMV and Isabelle HOL The success of SAT solvers in practice indicates that our method will be applicable to reasonable size models just as for example Alloy 21 is Furthermmore our method is intended for the construction of models that serve as specifications and which can be coinsrtructed interactively by a user By definition these cannot be flat Kripke structures of thousands of states or more since a user cannot handle this We do however deal with state explosion issues by providing for hierarchical Kripke structures and concurrently composed Kripke s
38. ative acknowledgement and posAck positive acknowledgement timeout and negAck lead to failure i e state fail and posAck leads to placement of the call i e state ok Fig 28 shows the overall phone call system with replaced by B4 Ma makes two attempts and so contains two instances of By If the first attempt succeeds the system should proceed to the success final state If the first attempt fails the system should proceed to the start state of the second attempt If the second attempt succeeds the system should proceed to the success final state while if the second attempt fails the system should proceed to the abort final state The relevant formulae are 1 specification formula for M AG ack V i e if either attempt receives a positive ack then eventually enter success state 2 specification formula ng for B AG ack AFok i e a positive ack implies that the phone call will be placed We repair Bm w r t rp using Eshmun the transition from posAck to fail is deleted as shown in Fig 27 3 coupling formula e AG ok AFsc AAG fl1 AF snd2 i e if either call is placed then eventually enter success state and if first attempt fails go to second attempt We repair MA w r t y using Eshmun checking retain for all internal transitions of By send int int gt ok int fl The transitions from fail to abort and okay1 to abort are deleted as shown in Fig 29
39. bal state is a tuple 81 8 01 Um where s is the current local state of P and U1 Ug is a list giving the current values of the shared variables in SH Let s 81 8 01 be the current global state and let P contain an arc from node s to node s labeled with B If holds in s then a possible next state is al 51 55 SK Up Um where vj Um are the new values respectively for the shared variables z1 m resulting from the execution of action A The set of all and only such triples 8 7 8 constitutes the nezt state relation of program P As stated above local atomic propositions are implicitly updated since P changed its local state from s to 8 The appropriate semantic model for a concurrent program is a multiprocess Kripke structure which is a Kripke structure that has its set AP of atomic propositions partitioned into AP U SU and every transition is labeled with the index of a single process which executes the transition Only atomic propositions belonging to the executing process can be changed by a transition Shared variables may also be present The structure of Fig 3 is a multiprocess Kripke structure The semantics of a concurrent program P Stp P Px is given its global state transition digram GSTD the smallest multiprocess Kripke structure M such that 1 the start states of M are Stp and 2 M is closed under the next state re
40. dex greater than i That is if Y b j for a box b of structure K then b can be viewed as a reference to the definition of the structure K 7 An edge transition relation E Each edge in E is a pair u v with source u and sink v e source either is a node of K or is a pair w1 w2 where wl is a box of K with 101 j and w2 is an exit node of Kj e sink v is either a node or box of Kj For simplicity of notation and exposition we restrict the discussion to two levels of hierarchy and one kind of box only which we refer to as B and we assume a single occurrence of the box B in M We assume without loss of generality that the start and exit states of box B do not lie on a cycle wholly contained in B We regard a box as performing some subsidiary computation and signalling the result by means of selecting a particular exit state Our method for repairing M w r t is as follows 1 Write a specification formula for we assume by induction on hierarchy level that B has been repaired w r t ng We infer under suitable assumptions that M satisfies np 2 Write a coupling formula p which relates the behavior of to that of M We repair M w r t 3 Prove gp o m i e that ng q m is a CTL validity We do this by implementing the CTL decision procedure 16 and checking satisfiability of the negation Hence from the previous two steps infer M n 36 We show below how to effec
41. efined naively e g by replacing a test and set by the test followed nonatomically by the set In general this may introduce new computations corresponding to bad interleavings that violate the specification These are removed by deleting some transitions 44 The use of model checking to generate counterexamples was suggested by Clarke et al 12 and Hojati et al 20 12 presents an algorithm for generating counterexamples for symbolic model checking 20 presents BDD based algorithms for generating counterexamples error traces for both language containment and fair CTL model checking Game based model checking 25 28 provides a method for extracting counterexamples from a model checking run The core idea is a coloring algorithm that colors the nodes in the model checking game graph which contribute to violation of the formula being checked The idea of generating a propositional formula from a model checking problem was presented in Biere et al 7 That paper considers LTL specifications and bounded model checking given an LTL formula f a propositional formula is generated that is satisfiable iff f can be verified within a fixed number k of transitions along some path Ef By setting f to the negation of the required property counterexamples can be generated Repair is not discussed Some authors 22 26 27 have considered algorithms for solving the repair problem given a program or circuit and a specification
42. eir algorithm appears to be highly nondetermin istic with several choices of actions e g do one of a b and c The paper does not discuss how this nondeterminism is resolved The main correctness result is given by Theorem 8 which encompasses soundenss completeness minimality of change which the authors call admissibility and complexity The proof of soundness and completeness is five lines of informal prose The proof of complexity does not address the nondeterminism of the repair algorithm Chatzieleftheriou et al 10 presents an approach to repairing abstract structures using Kripke modal transition systems and 3 valued semantics for CTL They also aim to minimize the num ber of changes made to the concrete structure to effect a repair They provide a set of basic repair operations add remove may must transition m change the propositional label of a state and add remove a state Their repair algorithm is recursive CTL syntax directed 12 Conclusions We presented a method for repairing a Kripke structure w r t a CTL formula 7 by deleting transitions and states and implemented it as an interactive graphical tool Eshmun This allows the gradual design and construction of Kripke structures assisted by immediate semantic 45 feedback Our method can handle concurrent and hierarchical Kripke structures which can be exponentially more succinct than the equivalent flat structure A crucial point is that we do not
43. ends the result of to Cx R2x moves through four local states initial state IN R2x then state WT_R2x after it receives x from Rix then state DN R2x after it performs and finally state R2x when it stabilizes x R2y moves through four local states initial state IN R2y then state WT_R2y after it receives y from its client which is not shown then state DN R2y after it performs y then state ST R2y when it stabilizes y For each pair we start with a naive pair structure in which all possible transitions are present modulo the above sequences We then repair w r t these pair specifications Client replica interaction pair specification for Cx R1z where z Cx client x R1x replica x e AG WT_R1x WT Cx z is not received by R1x before it is submitted by Cx e R1x V WT_CxAEG WT_R1x if z is submitted by Cx then it is received by Rix 32 51 1 2 22 2 0 52 m lt e _ IN_Cx WT_R1x UN CLWT RIX _ _ DN_Cx WT_R1x 4 OM OGWT RIX eer qum s9 nr SSAK _ DN_Cx DN_R1x DN Cx DN R1xj pau MET nac EN d s8 Se 120 X sll 3 IN_Cx ST_R1x _ DN_Cx ST_R1x k SS EE o a WT_Cx SNT_R1x DN_Cx SNT_R1x Figure 22 Repaired pair structure for Cx R1x e AG WT_Cx AF DN_Cx if Cx submits z then it eventually receives a result e AG DN Cx SNT_R1x Cx does not receive a result before it is sent by R1x The re
44. erations R the set of all replicas client x be the client issuing operation z replica x be the replica that handles operation x We use z to index over operations c to index over clients and r r to index over replicas For each operation x we define a client process and a replica process RZ where c client x r replica x Thus a client consists of many processes one for each operation that it issues As the client issues operations these processes are created dynamically Likewise a replica consists of many processes one for each operation that it handles Thus we can use dynamic process creation and finite state processes to model an infinite state system such as the one here which in general handles an unbounded number of operations with time We use Eshmun to repair a simple instance of ESDS with one strict operation z one client Cx a replica R1x that processes z another replica R2x that receives gossip of z and another replica R2y that processes an operation y x prev There are three pairs Cx R1x R1x R2x and R2x R2y Cx moves through three local states in sequence initial state IN Cx then state WU Cx after Cx submits z and then state DN Cx after Cx receives the result of x from Ris 1 moves through five local states initial state IN Ris then state WT_R1x after it receives x from Cx then state DN Rx after it performs z then state ST R1x when it stabilizes x and finally state SNT_R1x when it s
45. ersity of Beirut Beirut Lebanon 2015 To appear in Formal Methods in System Design 4 P C Attie and E A Emerson Synthesis of concurrent systems with many similar processes ACM Trans Program Lang Syst 20 1 51 115 Jan 1998 5 P C Attie and E A Emerson Synthesis of concurrent systems for an atomic read atomic write model of computation extended abstract In PODC 1996 6 P C Attie and E A Emerson Synthesis of concurrent programs for an atomic read write model of computation TOPLAS 23 2 187 242 2001 7 A Biere A Cimatti E M Clarke and Y Zhu Symbolic Model Checking without BDDs In TACAS 99 LNCS number 1579 1999 8 M C Browne E M Clarke and O Grumberg Characterizing finite kripke structures in proposi tional temporal logic Theoretical Computer Science 59 115 131 1988 9 F Buccafurri T Eiter G Gottlob and N Leone Enhancing model checking in verification by AI techniques Artif Intell 1999 10 George Chatzieleftheriou Borzoo Bonakdarpour ScottA Smolka and Panagiotis Katsaros Ab stract model repair In AlwynE Goodloe and Suzette Person editors NASA Formal Methods volume 7226 of Lecture Notes in Computer Science pages 341 355 Springer Berlin Heidelberg 2012 11 E M Clarke E A Emerson and P Sistla Automatic verification of finite state concurrent systems using temporal logic specifications TOPLAS 1986 12 E M Clarke O Grumberg K L McM
46. esponding arcs all exist We must therefore check that for all j k that if contains some transition by P in which it changes its local state from s to ti then Mik also contains some transition by p in which it changes its local state from s to ti This ensures that every set of corresponding arcs contains a representative from each pair program P for all j I i and so our definition of pairwise synthesis produces well defined result We call this the process graph consistency constraint since it states in effect that P PF have the same graph the result of removing all arc labels Consider again the three process mutual exclusion example and suppose that contains a transition in which P moves from T1 to but that does not contain a transition in which P moves from T1 to Then it would not be possible to compose arcs from P and to produce an arc in which P moves from T1 to Cl To enforce this constraint in our repair we define a boolean formula over transition variables whose satisfaction implies it Consider just two structures Mij Mix For Mj and local states si ti of P let siji tis 229 Spi 2 tiz be all the transitions in Mj that 1 are executed by P 2 start with P in a and 3 end with P in t Likewise for pair structure and the same local states ac fe let s i th 84 i t be all the transitions in Mj that 1 are executed by P 2 start with PF in
47. fy all of the constraints given in the propositional labeling propositional consistency nexttime formulae and release formulae sections of Definition 8 Hence all conjuncts of repair M are assigned tt by V Hence V repair M 7 tt and so repair M is satisfiable 7 amp Now the SAT solver used is assumed to be complete and so will return some satisfying as signment for repair M n not necessarily V since there may be more than one satisfying assignment Thus Repair M oi returns a structure M So S R L AP rather than failure By Cor 1 M is total M C M and M 80 m Repair M n model check M So E n if successful then return M else compute repair M as given in Section 3 submit repair M 7 to a sound and complete SAT solver if the SAT solver returns not satisfiable then return failure else the solver returns a satisfying assignment V return model M Y Figure 1 The model repair algorithm 12 normal transitions Ene m aa deleted transitions deleted states Figure 2 Simple Kripke structure 4 1 Example repair formula We show how repair M 7 is calculated manually for the simple Kripke structure in Fig 2 and the CTL formula 7 AGp V AGq EXp We omit the clauses dealing with totality of the model We use AGp rather than A falseVp but with the same index superscript for couting down
48. g Vw If we show that yj follows from t E then we can con clude V X by Definition 8 Proceeding as above we conclude V X y and one of the same two cases as above e so by Definition 8 VOX yj holds t u R HUT au As before in case 2 we are counting down Since we count down for n S then along every path starting from s either case 1 occurs which terminates that path as far as establishment of is concerned or we will repeat a state before or when the counter reaches 0 Along such a path from s to the repeated state call it v w holds at all states By Definition 8 From M v v and induction hypothesis holds Hence X S holds Thus along every path starting from s we reach state w such that HX ave holds for some m 0 n Hence by Definition 8 V X holds Case amp Elo this is argued in the same way as the above case for A pVw except that we expand along one path starting in s rather than all paths The differences with the AV case are straightforward and we omit the details Corollary 1 Soundness If o returns a structure Sb S R L AP then 1 is total 2 M C M 3 5 and 4 M is repairable 11 Proof Let V be the truth assignment for repair M n that was returned by the SAT solver
49. ial structure S8 C1 C2 Figure 4 Mutex repaired structure 5 2 Mutual exclusion interactive design using semantic feedback We add liveness to the mutex example by repairing w r t AG 2 C1 C2 AAG T1 AFC1 A AG T2 AFC2 We start with the structure shown in Fig 3 This yields the structure of Fig 7 in which D cycles repreatedly through neutral trying andcritical while P gt has transitions at all Obviously this repair is much too restrictive We notice that some transitions where a process requests the critical section by moving from neutral to trying e g N1 2 to N1 T2 are deleted Since a process should always be able to request the critical section we mark as retain all such transitions The retain button in Eshmun renders a transition s t not deletable by conjoining to repair M 7 thereby requiring to be assigned true After marking all such request transitions there are six and re attempting repair we obtain that the structure is not repairable By dropping say AG T2 2 we repair w r t AG C1 A C2 AG T1 AFC1 and obtain a repair given in Fig 8 We observe that AG T1 AFC1 was previously violated by the cycle T1 N2 T1 T2 gt T1 C2 T1 2 which is now broken By symmetric reasoning AG T2 2 was previously violated by the cycle N1 T2 gt T1 T2 gt C1 T2 N1 T2 Inspection shows that we cannot break both cycles at once T1 N2 gt 1 2 and
50. ical section To address this we checked retain for transitions none 1 none 1 C32 since the critical sections should always be reachable Figure 13 shows the resulting repair and Fig 14 gives the concretization of this repair to the full model of Fig 3 Notice that this is the best repair in that the minimum number of transitions needed to effect the repair are deleted and no state other than the bad state C1C2 is made unreachable More importantly the crucial frame property that processes can always request access is now satisfied 7 2 Abstraction with respect to sub formulae We can obtain larger reductions in the size of the state space by dropping the requirement that we preserve the values of all the atomic propositions in 7 cf predicate abstraction In some cases it may be necessary only to preserve the values of some propositional subformulae in 7 For example in mutual exclusion only the value of A is of interest Let 8 be a set of propositional sub formulae of 7 that is specified by the user Let SUB t AS be the set of sub formulae in AS that are satisfied by the state t e SUB t f f AS and M t f Definition 12 Adjacency respecting subformlua abstraction 2 4 Given a Kripke structure M So S R L AP and CTL formula we define an equivalence relation 25 4 over S as 24 follows e s sa t SUB s n AS SUB AS s t Rv t 8 R
51. illan and X Zhao Efficient generation of counterexamples and witnesses in symbolic model checking In Design Automation Conference ACM Press 1995 46 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 E W Dijkstra A Discipline of Programming Prentice Hall Inc Englewood Cliffs N J 1976 John Ellson Emden Gansner Lefteris Koutsofios Stephen C North and Gordon Woodhull Graphvizopen source graph drawing tools In Graph Drawing pages 483 484 Springer 2002 E A Emerson Temporal and modal logic Handbook of Theoretical Computer Science pages 997 1072 1990 E A Emerson and E M Clarke Using branching time temporal logic to synthesize synchronization skeletons Science of Computer Programming 2 3 241 266 1982 A Fekete D Gupta V Luchango N Lynch and A Shvartsman Eventually serializable data services Theoretical Computer Science 220 113 156 1999 O Grumberg and D E Long Model checking and modular verification TOPLAS 16 3 843 871 1994 David Harel Statecharts a visual formalism for complex systems Science of Computer Program ming 8 3 231 274 1987 R Hojati R K Brayton and R P Kurshan Bdd based debugging of design using language containment and fair ctl In CAV 793 1993 Springer LNCS no 697 D Jackson Alloy a lightweight object modelling notation ACM Transactions on Software Engi neering and Methodology 11 2 256
52. incur state explosion in dealing with concurrent and hierarchical structures for concurrent structures the size of the repair formula grows quadratically with number of processes in the worst case and for hierarchical strctures we repair one level at a time and so avoid the exponential blowup causes by replacing boxes by their definitions We also provided experimental results from our implementation which validated our avoidance of state explosion Future Work Future work includes using our implementation to repair larger examples and case studies Next we will work on supporting more formal models that express concurrent programs namely I O Automata and BIP We want to expand the specifications logic to include ATL which will help us repair and model multi agent games and systems There are many other directions we could expand our work in including repairing infinite state model using abstractions and additive repair by adding transitions and or states References 1 Rajeev Alur and Mihalis Yannakakis Model checking of hierarchical state machines ACM Trans Program Lang Syst 23 3 273 303 2001 2 P C Attie Synthesis of large concurrent programs via pairwise composition In CONCUR 99 10th International Conference on Concurrency Theory number 1664 in LNCS Springer Verlag Aug 1999 3 P C Attie Synthesis of large dynamic concurrent programs from dynamic specifications Technical report American Univ
53. lation of P Effectively M is obtained by simulating all possible executions of P from its start states Stp A program satisfies a CTL formula 7 iff its does Conversely given a multiprocess Kripke structure M we can extract a concurrent program by projecting onto the individual process indices 16 If M contains a transition from s 8 UL E Sors eS Uh then we can project this onto P as the arc s B where checks that the current global state is en 8i SK U1 Um and A is the multiple assignment z1 Zm vj Ui Le it assigns v to x l 1 m For example the concurrent program given in Fig 20 is extracted from the multiprocess Kripke of Fig 14 Each local state is shown labeled with the atomic propositions that it evaluates to true Take for example the transition in Fig 14 from 52 to s4 this is a transition by from N1 to T1 which be taken only when T2 holds It contributes an arc N1 T2 e T1 to Pi where denotes the empty action which changes nothing Likewise the transition from 80 to 81 contributes N1 N2 e T1 and the transition from s5 to 87 contributes N1 C2 T1 We group all these arcs into a single arc whose label is N2 T2 C2 ce The operator is a disjunction of guarded commands B B gt A means nondeterministically select one of the two guarded commands
54. lting abstract structure M which has two states corresponding to these equivalence classes Figure 16 gives the repair of Fig 3 w r t AG C1 A C2 The concretization of this repair to the full model of Fig 3 gives Fig 14 the same repair that we obtained from abstraction by label Unlike abstraction by label however we obtained this repair immediately and did not have to use the retain button 7 3 Concretizing an abstract repair to repair the original structure Abstract repair does not guarantee concrete repair When we concretize the repair of M we only to obtain a possible repair of which we then verify by model checking We concretize as follows The abstraction algorithm keeps a Map data structure that maps a transition in M to the set of corresponding transitions in M If a transition in M is deleted by the repair of M then we delete all the corresponding transitions in M to construct the possible repair of M The benefit of such abstractions is that we can in many cases obtain larger reductions in the state space than if we used only repair preserving abstractions 7 4 Example barrier synchronization Fig 17 shows the result of abstraction by subformulae applied to the barrier synchronization Kripke structure in Fig 9 Fig 18 show a repair of this structure and Fig 19 shows the concretization of this repair to the structure of Fig 9 Again this produced a minimal repair in which all frame properties are preserved
55. m for hierarchical Kripke structures is solvable by a polynomial time depth first search see Theorem 1 of Alur amp Yannakakis 1 Let be the result of replacing by M and let be the set of atomic propositions corresponding to the start state of B the exit states of B and all states of M that are not in B Proposition 5 M X Proof Construct a forward simulation f from M to MA as follows A state of M that is not in B is mapped to itself in Likewise the start state of and every exit state of are mapped to themselves this is possible since BA contains these states Internal states of B are all mapped to the state intg of Corollary 3 For any ACTL X formula f over if Ma f then M E f Proof Follows immediately from Prop 3 and Prop 5 9 3 Heirarchical repair Theorem 4 If v By gp and gg then M Proof From and Cor 2 we have M ng From and Cor 3 we have M E y From M E 9p M E e and gp o we have M E n 38 Figure 26 Box Bu for a single phone call 9 4 Example phone system We illustrate hierarchical repair using the phone call example from 1 Fig 26 shows the M situated version of a box B that attempts to make a phone call from the start state send we enter a waiting state wait after which there are three possible outcomes timeout negAck neg
56. njoin X pal Eau Xt forall s t R conjoin E X X1 forall s S p APN L s conjoin X p forall s S p AP L s conjoin X Clause 1 Clause 2 Clause 3 Clause 4 Clause 5 Clause 5 Figure 34 Initializing repair M conjoin f g 3 case f f does not contain either of Auc g f f Es gt Xo forall t R s 9 2 g A Est gt Xty f Vieni Esa gt forall Ris g g V Est gt Xt 1 f Vw m Xs LE V Ju Rs Es gt X laeve 1 1 gt forall t Mal g g A Est gt g Xs A Xp V g 1 f Xs A LE V Vents Esa forall t R s g g V Est X ovt g X Xd Xu v X g SH nu endcase repair repair M n g m Figure 35 Adding conjunct to repair M n 49
57. ogram N gives the number of processes in mutual exclusion and the number of barriers in barrier synchronization Table 2 gives experimental results for different concurrent programs expressed as concurrent Kripke structures The experiments were conducted on a linux computer using openJDK 7 with 4GB of ram and 3 3GHz CPU These agree closely with Prop 2 For mutex quadratic growth is expected since the number of pairs is N N 1 2 and the number of pairs that P is involved in is N 1 and so we expect quadratic growth with N For dining philosophers in a ring the number of pairs is N and the number of pairs that P is involved in is 2 and so we expect linear growth with N The point of Eshmun is not to handle large state spaces but to provide an interactive environment with semantic feedback for the design and construction of small medium sized structures These are to be composed concurrently and or hierarchically to yield a complex structure which would be exponentially large if flattened out 41 Program N Basic Abst by Abst by Name repair label subformulae Mutex 2 0 083 0 026 0 036 Mutex 3 0 51 0 25 0 038 Mutex 4 2 34 0 84 0 17 Mutex 5 89 08 2 48 1 59 Barrier 2 0 31 0 11 0 017 Barrier 3 0 67 0 21 0 047 Barrier 4 1 03 0 76 0 11 Barrier 9 1 81 1 04 0 26 Table 1 Times in seconds taken to repair the given programs Processes 5 10 15 20 25 50 Mate 0 33 0 64 0 84 1
58. ons We extend the basic repair method in several directions 1 the addition of states and transi tions and the modification of the atomic propositions that hold in a state i e the propositional labeling function of the Kripke structure and 2 the use of abstraction mappings i e repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M and 3 the repair of hierarchical Kripke structures 1 by using a CTL formula to summarize the behavior of each box and CTL deduction to relate the box formula with the overall specification and 4 the repair of concurrent Kripke structures i e several Kripke structures that are composed in parallel and that synchronize on common operations 2 Finally we show that the model repair problem is NP complete We have implemented the repair method as GUI based tool Eshmun available at http eshmuntool blogspot com which also provides a user manual All of the examples in this paper were produced using Eshmun Formally we consider the model repair problem given a Kripke structure M and a CTL or ATL formula 7 does there exist a substructure M of M obtained by removing transitions and states from M such that satisfies 7 In this case we say that M is repairable with respect to 7 or that a repair exists Our algorithm computes in deterministic time polynomial in the sizes of M and 7 a propo sitional formula repair M such th
59. ositional consistency s t implicitly range over S Other ranges are explicitly given Essentially repair M n encodes all of the usual local constraints e g holds in s iff p holds in all successors of s i e all t such that s t R We modify these however to take transition deletion into account So the local constraint for AX becomes holds in s iff holds in all successors of s after transitions have been deleted to effect the repair More precisely instead of Xs Ax Niet Xt we have Xs Axy Ju gt Xt Here s t abbreviates s t R The other modalities EX AV EV are treated similarly We deal with AU EU by reducing them to EV AV using duality We also require that the repaired structure M be total by requiring that every state has at least one outgoing transition 1 some initial state so is not deleted V soe So 2 M satisfies m i e undeleted initial states satisfy m for all 60 Xso gt 3 is total i e each retained state has at least one outgoing transition to some other retained state for alls 5 X V is Xi 4 If an edge is retained then both its source and target states are retained for all s t Est gt Xs Xi 5 Propositional labeling for all s S for all p APN L s for all p AP L s 6 Propositional consistency for all s S for all sub n En Xs for all pV p s
60. paired pair structure is given in Fig 22 Pair specification for R1x R2x where x O x strict R1x replica x e AG SNT_R1x ST R2x the result of a strict operation is not sent to the client until it is stable at all replicas The repaired pair structure is given in Fig 23 CSC constraints pair specification for R1x R2y where x O y x prev 1 replica x R2y replica y e AG DN_R1x gt DN_R2y operation y in is performed before z is The repaired pair structure is given in Fig 24 Fig 25 gives a concurrent program P that is extracted from the repaired pair structures as discussed above By the large model theorem 2 4 P satisfies all the above pair specifications 9 Repair of Hierarchical Kripke Structures We now extend our repair method to hierarchical Kripke structures As given by Alur amp Yannakakis 1 a hierarchical Kripke structure K over a set P of atomic propositions is a tuple K1 Ky of structures where each K has the following components 1 A finite set N of nodes 33 t2 IN_R1x WT_R2x tl WT_R1x IN_R2x t5 IN_R1x DN_R2x t3 DN_R1x IN_R2x ki A Ee I 11 l ST_R1x WT_R2x t17 Ta T RIxST R2x huq EN ZI I d t10 IC MEL I SNT R1x IN_R2x _ A 114 1 I I _ SNT
61. rmulae over the and Xs to repair M e g Est Ban adds the constraint that either all three transitions s t sl U s 1 are deleted or none are Likewise we can add constraints for the removal of states Such constraints are helpful for the interactive design of finite Kripke structures 6 4 Dealing with state explosion A key drawback of our method so far is that Kripke structures even when used as specifications may be quite large To address state explosion we extend in the following three sections of the paper the basic repair method in three directions 1 to use abstraction repair an abstract model and then concretize the repair to obtain a repair of the original model 2 repair of concurrent Kripke structures as used for example in Statecharts 19 3 repair of hierarchical Kripke structures 1 7 Repair using Abstractions We now extend the basic repair method to use abstraction mappings i e repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M The purpose of abstractions is two fold 1 Reduce the size of M and so reduce the length of repair M n has length quadratic so repairing an abstract structure significantly increases the size of structures that can be handled 2 focus the attention of the repair algorithm which in practice produces better repairs Our repair method nondeterministic
62. ructure Given Kripke structures M So S R L AP and M S S J H AP we say that is a substructure of M denotedvM C M iff Sy So S C S C R and pce Definition 5 Repairable Given Kripke structure M So S R L AP and CTL formula n M is repairable with respect to if there exists a Kripke structure So S R L AP such that is total C M and M So n Definition 6 Model Repair Problem For Kripke structure M and CTL formula we use M m for the corresponding repair problem The decision version of repair problem is to decide if M is repairable w r t The functional version of repair problem is to return an that satisfies Def 5 in the case that M is repairable w r t n 3 1 Complexity of the Model Repair Problem Theorem 1 The decision version of the model repair problem is NP complete Proof Let be an arbitrary instance of the CTL model repair problem NP membership Given a candidate solution 50 5 R I AP the condition C M is easily verified in polynomial time M S5 n is verified in linear time using the CTL model checking algorithm of 11 NP hardness We reduce 3SAT to CTL model repair Given a Boolean formula f A lt lt ai V bi V ci in 3cnf where aj b c are literals over the set z4 of propositions i e each of aj bj is 7 or z for some j 1 m We reduce f to
63. s and 3 end with PE mt Then define grCon i 2 k Si ti 1 I 3 For clarity of sub superscripts we use E s t rather than here Now define grCon to be the conjunction of the grCon t j k Si ti taken over alli 1 K j k I i j Z k and all pairs s t of local states of P Then our overall repair formula is grCon A repair Mi m 5761 Eshmun generates this repair formula from the pair structures and their respective spec ifications In particular it computes grCon automatically and conjoins it into the repair formula A satisfying assignment of this formula gives a repair for each w r t nij and also ensures that the repaired structures satisfy the process graph consistency constraint A concurrent program Stp P Px can then be extracted as outlined above By the large model theorem of 2 4 P satisfies A jjer mij Let n I i ie ni is the number of pairs that P is involved in The length of grCon is then linear in Zoe since we take overlapping pair structures those with a common process two at a time j k I i j Z k and we repeat this for every P It is also linear in the size of the pair structures By Prop 1 the length of each repair Mi rij is quadratic in the size of and linear in the length of nij So overall the length of the repair formula is quadratic in the n quadratic in the size of the Mij and linear in the length
64. t these repairs without incurring an generate an exponential blowup in size of the structure being repaired To show that the method is sound we use weak 1 stuttering forward simulations 8 18 which means that our results are restricted to ACTL X the universal fragment of CTL without nexttime 18 Definition 15 Weak forward simulation Let M So S R L AP and M S Si RU AP be Kripke structures such that AP 2 Let AP C AP A relation H C S S is a weak forward simulation relation w r t AP and from t to t iff 1 H t t and 2 for all s s 8 implies L s AP L s and 2b for every fullpath from s in M there exists a fullpath from s in and partitions of n of x such that for all i gt 1 Bi B are both nonempty and finite and every state of is related to every state of Write M lt MI iff there exists a weak forward simulation H w r t AP and such that Vs Sods 5 His s Note that we do not consider fairness here Let A be set of atomic propositions Proposition 3 Suppose M lt for some set AP of atomic propositions Then for any ACTL X formula f over AP if M f then ME f Proof Adapt the proof of Theorem 3 in Grumberg and Long 18 to deal with stuttering That is remove the case for AX and adapt the argument for AU to deal with the partition of fullpaths into blocks The details
65. teraction relation I a symmetric relation over the set 1 A of process indices We extract from each pair structure Mj a corresponding pair program p Pi which consists of two pair processes pi and Pi We then compose all of the pair programs to produce the final concurrent program P Composition is syntactic the process P in P is the result of composing all the pair processes P Bh For example 3 process mutual exclusion can be synthesized by having 3 pair programs P P P P4 P3 P2 which implement mutual exclusion between each respective pair of processes These are all isomorphic to Fig 20 modulo index substitution Then the process solution P P P gt Ps is given in Fig 21 where only is shown P and being isomorphic to P modulo index substitution results from composing P and Pj In the arc from T1 to C1 is the composition using the operator of corresponding arcs in P and P For example the arc from T1 to in P2 namely T1 N2 2 C1 and the arc from to C1 in PP namely 1 N3 6 are corresponding arcs since they have the same source and target local states namely T1 and Cl Their composition given the arc T1 2 T2 gt e amp N3 5 ce 6 5 e C1 The meaning of B gt A amp B gt A is that both and B must hold and then A and A must be executed concurrentl
66. tructures These correspond to arbitrarily large flat structures but require only a linear increase in the size of the formulae that the SAT solver must handle Furthermore they can be handled interactively by a user since each component Kripke structure is small The rest of the paper is as follows Section 2 provides brief technical preliminaries Section 3 states formally the CTL model repair problem and shows that it is NP complete Section 4 presents our model repair method and shows that it is a sound and complete solution to the model repair problem Section 5 presents two example applications of our method mutual exclusion and barrier synchronization Section 6 extends the methjod to deal with the addition of states and transitions and the modification of the atomic propositions that hold in a state It also gives some optimizaitons that improve the running time in some cases shows how to increase the expressiveness of repairs by using generalized boolean constraints and discusses state explosion Section 7 shows how to reapir abstract strucutres and then concretize the resulting repair to obtain a repair of the original structure Section 9 shows how to repair hierarchical Kripke structures Section 8 discusses the repair of concurrent Kripke structures Section 10 discusses our implementation the Eshmun tool Section 11 discusses related work Section 12 concludes 2 Preliminaries Computation Tree Logic and Kripke Struc tures Let
67. ub n X vao V Xs for all p Aw sub n Xs o y 7 Nezxttime formulae for all s S for all sub n Xs Axy Pus gt Xio for all sub n Vas a Esa 8 Release formulae Let n S i e the number of states in M Then for all s S for all AjgVwv sub n m 1 n Xs alve Xs Alvy Laus V Au bat gt Ate 0 XA Vy Xs for all E g Vv sub n m 1 n XS Ela m m 1 Xs V Vas Est A Eegiel for all E pVw sub n X The various clauses of Def 8 handle corresponding clauses of Def 2 Clause 5 handles Clause 3 of Def 2 Clause 6 handles Clauses 4 5 and 6 of Def 2 Clause 7 handles Clauses 7 and 8 of Def 2 Note here the use of the edge booleans E to remove from consideration in the determination of whether s satisfies AXy or an edge that is to be deleted as part of the repair so that is false Clause 8 handles Clauses 9 and 10 of Def 2 as follows Along each path either 1 a state is reached where Jean is discharged v or 2 gVv is shown to be false ay v or 3 some state eventually repeats In case 3 we know that release also holds along this path Thus by expanding the release modality up to n times where n is the number of states in the original structure M we ensure that the third case holds if the first
68. y It is a conjunction of guarded commands Hence the meaning of T1 N2 e T2 gt e N3 gt gt C1 is that P can enter its critical state C1 iff P gt is in either its neutral state N2 or it trying state T2 and also P3 is in either its neutral state N3 or its trying state The other two arcs of P are similarly constructed We use only when the actions of the guarded commands update disjoint sets of variables so that the result of execution is always well defined Let j 3 I so that I i is the set of proceses that P interacts directly with For each j I i we create and repair pair structure w r t a pair specification nij From we extract pair program P Pi Process P in the overall large program is obtained by composing the pair processes P for all j I i as follows 3 Def 15 pairwise synthesis P contains an arc from s to t with label Ger ch Bj gt AL iff for j I i P contains an arc from s to t with label Bi A Recall that two arcs in Pi PP correspond iff they have the same source and target nodes An N26 T26 C2 N26 T2 amp ae N39 e N3 lt N20 2 N3 T3 Figure 21 Concurrent program extracted from Fig arc in P is then a composition of corresponding arcs in all the Pi I t For this composition to be possible it must be that the corr

Model Repair via SAT Solving - AUB

Contents

Download Pdf Manuals

Related Search

Related Contents