Home

here - Departamento de Matemática

1. Chapter 4 Towards EpCTL In this chapter we define the computation tree extension to EPPL called exoge nous probabilistic computation tree logic EpCTL and present a weakly complete Hilbert calculus and a model checking algorithm for it 4 1 Syntax The syntax of EpCTL can be easily obtained from the syntax of EPPL The idea is that at the level of global formulas we also introduce the usual CTLmodalities In table 4 1 we present the syntax by mutual recursion and recall the definition of classical formulas and probability terms Table 4 1 Syntax of EpCTL B pl 81 8 B basic formulae t z 0 1 5 t tt probabilistic terms 5 08 t t J 6 6 gt 6 EX AFS El U6 global formulae where p A z Z The basic formulas probabilistic terms and global formulas without temporal modalities have the same intuitive meaning as in EPPL Each modality is composed by two symbols the first one is either E or A and the second one either X F or U The first symbol quantifies over computation paths starting at some state s one of the symbols is the existential quantification E for there exists and the other one the universal quantification A for all The second symbol is used to describe temporal behavior X stands for next F for sometime in the future and U for until So EX6 holds if there exists a path starting at s such that 6 holds in the ne
2. e Lift gt Feppr D 1 gt G2 gt 081 gt D183 e Eqv 4 FEPPL LS dl e RCF Hepp t lt to for each instantiation of a valid analytical inequality e Prob Hepp f T 1 e FAdd Ferr J B1 A 82 0 2 S 81 V B2 SB Cf 02 e Mon Ferr 0 61 82 D Cf B1 lt Cf B2 Inference Rules e Mod i i D 62 Epp 02 Proof As is common in completeness results we use a contrapositive argument if 6 then If 6 A formula 6 is said to be consistent if Y So if we prove that every consistent formula has a model we get the completeness result Observe that if then If that is is consistent Therefore if we can prove it has a model If So we will prove that every consistent formula has a model Assume by contradiction that 6 is consistent and the SAT algorithm returns no model Let A e exhaustive conjunction of literals ve I dg By the completeness of propositional logic it follows that F Vecaep dg and by GTaut we have FUA zx If is consistent then there is e consistent and if 6 has no model then the consistent e has no model as well If the SAT algorithm returns no model for e it must be because of one of the following two causes i it cannot find a V at the second foreach ii for all viable V the SatReal algorithm returns no model We will now show that for both cases we can contradict
3. If is 01 then M s IH 6 iff M s I 6 iff M s IK iff M s Ik 0 and nd If is amp D do then M s lt 6 iff M s 6 or M s IH da iff M s I dy or M s IH iff M s IH 6 and 6 6 gt do If is EXd then M s IH EX6 iff there is s s R such that M s lr iff there is s s R such that M s le 6 iff M s IF EXS and 6 EX If is AF then M s lr AF iff for all path 7 in R starting in s there is i gt O such that M x I iff for all path 7 in R starting in s there is i gt 0 such that M rr IF 6 iff M x I AFO and 6 AF i If is E 6Uda then M s IH E 0 Uda iff there is a path 7 in R starting in s and gt 0 such that M r IF 62 and M 7 IF dy for all 0 gt j lt iff there is a path 7 in R starting in s and gt O such that M m IF ds and M m IF for all 0 gt j lt i iff M s IH E Udo and 6 E 01U s We need one final remark before we are able to prove the completeness of HC pctt Like before we denote by at 6 d1 6x the set of atomic EPPL formulas in 5 We define for i 0 11 the formula dj if the j th bit of is 1 6 otherwise k di A Pj where pj j l Let V Jic 4 i where A is the set of Boolean k vectors such that q is an EPPL consistent formula Of course FeppL Y and so by the previous theorem FPepcri Y Now let 6 be an EpCTL formula such that lrepcr
4. and suppose that M S R L is a CTL model such that M s If AGW gt 5 Then M s lr AGW and M s If 6 Consider the EpCTL model M s US R L such that S s S s s amp R is the subset of states reachable from the state s R is the restriction of R to s US and L s is the EPPL model that satisfies one of the formulas i with A and such that M s IF di This model exists since W is satisfied in all s S and all in V are consistent Therefore M s If AGW gt But Fepcri Y and by soundness lrepcri Y So M s If which is a contradiction We conclude that if Ikepctt then Iker AGY gt 40 CHAPTER 4 TOWARDS EPCTL Theorem 4 3 4 The axiomatization H CEpcrt is complete Proof Let l epct 6 By the previous discussion IHcrt AGU D 9 Using the completeness of HCcrL we have Fer AGU 3 8 From Lemma 4 3 1 we get Fepctt AGW gt Hence we are able do the following derivation in EpCTL 1 FW Theorem 2 F AGU AGen 3 F AGY D6 Theorem 4 F Modus Ponens 2 3 Therefore HCkpcrt is complete 4 4 Model checking algorithm for EpCTL The EpCTL MC algorithm can easily be obtained from the CTL MC algorithm replacing the propositional symbol checking step with the EPPL model checker Like in the CTL MC for Kripke structures in order to check a formula 6 we label each state of the probabilistic Kripke structure with the set of subformulas
5. 0 wi Q but because A wi 0 wi X 1 which means there is wi w such that w Xd i e X fact Y IF Ai We now prove that M i mil x In the conditions of our sample space mil u Xx 1 utw Een Blw 1 Seven p wj 1 Hw Since fact w u w if w Q 0 otherwise M i 5 fact w 5 fact w 5 fact w 5 uwi 5 0 wie 2 wi EQ wi dQ wien wi dQ BG 1 Bi 1 Bi 1 Bi 1 Bi 1 Y ae WL oP ww 0 Bw 1 bred pacer me me 24 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL It is now straightforward to check that T t ti xs We omit the rest of the proof as it is a simple but lengthy exercise of induction over 3 5 Optimizations The tool produced in the scope of this work is not a blind implementation of the algorithm of the previous section several optimizations are used in order to reduce the time in average it takes to model check a formula Unfortunately none of these will actually reduce the worst case complexity in which the program runs In this section we will justify the major implementation deviations from the algorithm and prove their soundness 3 5 1 Equivalent SPBCs Figure 3 3 Equivalent SPBCs Example 3 5 1 Consider the SPBCs represented in Figure 3 3 It is easy to see that the joint distributions of Xp Xp Xps and Yp Yp Yp3 are as presented in Table 3 1 We have seen that under our assumption
6. V IH Albfg e and V WV B for all 8 lbfo_ e do kh Luev Zo 1 N Mev 0 lt zu foreach a lig e do 8 K KN OS fr veV vlk B end p SatReal k if p no model then Hp D z veVy Yo Plvar s return V pp and assignement p end end end return no model We claim that Algorithm 1 decides the satisfiability of an EPPL formula in PSPACE and to support this claim we explain the algorithm and its soundness Given an EPPL formula we start by computing line 1 its global atoms bfn ig 6 and at 6 This sets take O d space to store Now we cycle over all exhaustive conjunctions e such that vs IH Opus Observe that if has a model m y then for all 9 at d this model is such that either m y IF 6 or m y If 6 Therefore there is an exhaustive conjunction e such that m y is a model of e and in this case ve IF dj On the other hand if has no model then all e such vs IF dg have no model Hence to find a model for it is enough to find a model for an e such that ve IF 6 At each step of the cycle of the second line of the algorithm we only need to store one such which requires only 2 5 COMPLETENESS OF EPPL 11 polynomial space To check if there is an EPPL model for we start by computing lb fole lbfo e and lig e which can be stored in O e Given Remark 2 2 1 it is enough to check f
7. because each vertex does not store the information of who its children are This information is not relevant when computing the probabilities and is therefore discarded In a factorization there is a factor for each vertex of the SPBC so this data structure occupies linear space in the number of vertices of the SPBC Factorizations are actually the only structure needed to represent the EPPL model so as far as space is concerned this is a very reasonable data structure As we will see time complexity will not be sacrificed by this decision figure 4 5 Ta 0 99 nox 6 var8 0 5 my T Figure 4 Part of a factorization MTBDD MTBDDs are structures used to represent real valued Boolean functions in a canonic form In this program we use an external package with the implementation of these structures and of the functions that manipulate them Despite having many proprieties that are not necessary in the present program MTBDDs will play a major role in implementing a temporal exten sion of this model checker and therefore it was decided to use this package instead of others that are more limited in scope figure 5 In Table 1 at the end of the document we present the correspondence between the symbols in the syntax described in the main reference the actual symbols used in the implementation and their internal representation 51 11227374 Ff T1 T2 T
8. 165 194 Polimetrica 2005 P Baltazar and P Mateus Verifying probabilistic systems with EpCTL Await ing publication 2008 P Baltazar P Mateus R Nagarajan and N Papanikolaou Exogenous prob abilistic computation tree logic Electronic Notes in Theoretical Computer Science pages 1635 1790 2001 A Sernadas and C Sernadas Foundations of logic and theory of computation College Publications 2008 EPPL model checker User Manual Welcome to the EPPL model checking tool for probabilistic Boolean circuits for unix based OS This tool was developed as part of a master s degree thesis and we advise reading the main reference before using the program This is only an operational manual but we shall assume the reader is familiar with the basics of formal logic and model checking when employing technical terms Operational guide If you want to use the MC as a black box you need no compiling options just open the console specify the path up to the MCEPPL folder and type path MCEPPL make run If you choose to edit any of the files used type path MCEPPL make clean followed by path MCEPPL make to recompile If you wish to add any files you should probably edit the makefile in the folder When running the program if you see something similar to Figure 1 you should be fine 47 48 EPPL MODEL CHECKER USER MANUAL EPPL Welcome to the EPPL model checking tool for PBCs What do you wish to do 1 Load a ne
9. EX f Xp w en Xp w 1 where u denotes the measure over the probability space underlying in the ran dom vector Xp Xp Proposition 3 5 5 Given SPBC B that has one deterministic gate the random variable X induced by that vertex is completely dependent of par X by means of v when seen as a Boolean formula Proof For all w w1 wn E Q P Xp Uil Xp a Wi l 2029 pi wi lios pi 1 Ti 1 o zat 20 1 fws pi wr i1 CTS O if w pilwr i i Let us suppose by contradiction that u w Xp w pilpar Xp H 7 1 Then there is W w Xy 7 gi par X such that u W gt 0 As W is finite there is wi wf 13006 W such that u w gt 0 P Xp wi par Xp par wi 0 5 zi 0 because wi vw g par w On the other hand as P par X par w gt 0 because wf Q P Xp wi par Xp par wi i P Xy wilpar Xp par gt 0 P par X par w because wi Q This is a contradiction Remark 3 5 6 At this point it is convenient to notice that since our sample space is finite and has no elements with measure zero verifying m y lr OP is the same as verifying if f B m 1 indeed if m y lr DB then Q GC therefore 28 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL 1 p Q u X5 1 ie Lf 6 m 1 On the oher hand if m y Y OB QF X5 1 and there is w
10. O 6 time since sub y 6 lt pst S lt 6 and bfo 5 lt 6 The cycle runs in O 6 All four rounds of the algorithm take O 2 6 fact or less time So the algorithm runs in O 2 fact as well This is slightly less time efficient than the algorithm proposed in 19 However the present algorithm does not require writing out explicitly an EPPL Model a structure that takes exponential space in A nor it requires at any step the use of such large structures In fact none of the arrays B M T G take more than O space and the input itself takes O y O O fact So the algorithm takes O y 6 n 8 space whereas the one proposed in 19 needs O 2 y This is what we gain from using PBCs at the cost of a little temporal efficiency Proposition 3 4 1 X fact y IF if and only if Algorithm 2 returns 1 l if xX fact YF i 0 if Xfacts Y WA If B i 1 then for all wi 2 either fact wi 0 or fact wi 4 0 and Ai u 1 In the first case w Q and we need not consider it In the second Proof We will first prove that B i case wi Q and wi X 1 Since we run trough all wi 2 we also exhaust all wi Q and each one verifies w X D meaning that Q Re i e X fact Y F Ai If B i 0 then for at least one wf fact w gt 0 and A w 0 Since fact wi gt
11. Q X grimi w 1 Boios reo P1 On the other hand let w fue Q0 X gn fo 1 By the same Eso reasoning mutatis mutandis we conclude that w io Q Xg w 1 This proposition allows the following simplification in the algorithm by replac ing all variables induced by deterministic gates with the function induced by the corresponding formula the number of valuations that have to be considered halves for each deterministic gate as one of each of the two valuations that only differ in the deterministic variable would have measure zero and therefore doesn t need to be considered Remark 3 5 6 shows that given the particular structure of our sample space we may consider subformulas of the form O8 as f 8 1 We refrain from doing 3 5 OPTIMIZATIONS 29 so in our implementation for efficiency reasons As we can see from the basic algo rithm we always have to run exhaustively trough all 2 valuations in 2 in order to compute f B y 7 Whereas to compute x fact y IF UB the computation ends as soon as we find a suitable valuation The process of computing x fact y IH L18 can be further refined using deterministic gates and the program explores this property Theorem 3 5 8 Given a basic formula 8 and a SPBC induced EPPL Model x fact then Xfact Y M OG iff A em is satisfiable as a propositional formula where D denotes the s
12. Z ranging over elements of algebraic real numbers Together with the constants 0 and 1 addition and multiplication we are able to express all algebraic real numbers Finally measure terms terms of the form f 8 intuitively represent the measure of the set of valuations that satisfy 6 Global formulae are either of the form 06 comparison formulas ty t2 or built upon these by the connectives e 2 Formulas like L18 allow us to check if all valuations induced by the sample space satisfy 8 We will use the intuitive abbreviation 9 8 for LI 8 06 is satisfied if there is at least one valuation induced by the probability space that satisfies 9 but despite the notation it is not a modality since we do not have formulas such as D H Like we did for basic connectives we will assume U N and comparison operators gt lt gt introduced as abbreviations in the classical way Notions of occurrence and substitution of terms t and global subformulas 6 in the global formula 6 are defined as usual For the sake of clarity we shall often drop parentheses in formulas and terms if it does not lead to ambiguity We also introduce the following sublanguage of probabilistic state formulas which do not contain any occurrence of measure terms lt I gt a zJ0 il a a aa Terms of this sublanguage will be called analytical terms and formulas will be call
13. a whitespace then comes the labeling basic formula with syntax as above followed by another whitespace and finally the labeling float The SPBC file from Example 2 2 2 for instance would be Xpl 1 0 5 Xp2 1 0 5 Xp3 Xpl Xp2 1 3 6 2 A simple case study We now introduce as an example of application of the MC tool a simple hypo thetical case study on reliability and quality control Gates that compute usual Boolean functions like conjunction or disjunction of multiple inputs are massively produced due to their many applications However gates for more unusual functions are often required In such cases one of the approaches used is to build a circuit that computes the function and have the whole circuit acting as a single gate This is usually done automatically through the function s minterm form also known as sum of terms form To build a minterm representation one takes all configurations of inputs that yield result 1 and for each of them considers the product of all variables that take value 1 in that configuration and 1 minus the variables that take value 0 in that configuration The minterm representation is the sum of all such products Example 3 6 1 Consider the Boolean function represented in table 3 2 Since only the configurations 0 0 1 0 1 0 and 1 0 0 yield the result 1 its minterm form is f z y z 1 z 1 y z 1 z y 1 2 1 y 1 2 So Figure 3
14. and the Boolean function f that we will 3 2 PROBABILISTIC BOOLEAN CIRCUITS 17 Figure 3 1 Sample gate represent by a formula in the obvious way We will henceforth adopt these syntactic representations of PBCs which we shall call Specifications of probabilistic Boolean circuit SPBC An arrow of a PBC or SPBC represents the dependency relation between the head where the arrow points to and the tail where the arrow comes from one needs the values of the propositional symbols in order to compute the value of the labeling function We will make use of graphical representations of SPBCs borrowing from standard notation of Boolean circuits and extending upon it each vertex will be represented by a box either labeled with the function f or with a characteristic shape for widely used connectives The expected value of the Bernoulli random variable R will be written under the box and it s labeling variable representing the output of the probabilistic computation will be as usual placed after the box The lines entering from the left of the box represent the outputs of other gates that are to be used as inputs Consider as an example Figure 3 1 It represents a gate that computes falx1 2 max x1 2 where x and zz are given as input coming from similar gates and fz is represented by x V x3 13 represents the result of the probabilistic computation that returns the value of f3 with probability 0 7 and 1 f3 other
15. coin tossing heads checking Example 2 2 2 with only one coin now We allow ourselves to non deterministically toss the coin first or look at the face up first We can model the outcome space with the set of propositional symbols A p pi Po that will induce Bernoulli random variables De 1 0 stands for coin shows heads tails p 1 0 stands for coin has not been looked at p 1 0 stands for if coin has been looked at outcome was heads tails The experiment can be modeled by a probabilistic Kripke structure M S R L with S 151 52 53 84 55 R s1 82 81 83 82 4 53 55 and L t Q 2 ui X for i 1 5 such that 4 3 COMPLETENESS OF EPCTL 37 Q 1 0 0 and amp n 1 0 0 1 95 1 0 0 0 0 0 and p2 1 0 0 12 0 0 0 1 2 Q 1 1 1 and us 1 1 1 1 Q4 1 1 1 0 1 0 and w4 1 1 1 4 0 1 0 1 2 Qs 1 1 1 0 1 1 and ps 1 1 1 5 0 1 0 1 2 The formula EF J pc A pi po gt 0 states that there is some course of actions where the coin has been checked as heads and yet the tails face is up The formula f p gt 0 gt AG Ulp po states that if the tails face of the coin is up then for any course of actions the checked value and the face of the the coin will agree Recall that a CTL model is a Kripke Structure a tuple M S R L where S is the set of states RC S x S is the accessibility
16. it suffices to prove that P X Xy X5 P Y Y Yp for all w Q Let w w Wa Q then Pp As Uil Xp a Wi 1 es Xp wi TE Ds um 1 Dd NN Bi Ba pan Bi Ba e Case r r and pS pr pP ui very Wi 1 pP ui 4 1 because yP gt eP o 1 if Wi oe wi sg 401 E 1 if Wi PP ui ving 041 Wisi O if ua pP wi very 4041 O if a pP ui 4041 Bo Uii P B9 i Bi Bi B B ri 9 Bi a a z J i o oP i dB 1 dii Jor oa 17 O oP a 1 Tal ir iga Pp Yo Wi Yp _ Wi1 Yp w1 26 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL Ba e Case r 1 r and pf e mpb pP ui es Wi 1 1 PP ui cs Wi 1 because yP e p22 Bi i B3 0 fu Apr us wi l if wi zv ww a 1 if Wi pP wi very 401 0 if Wi PE un sw 1 wi 72 1716 By 1 rP1 1 Wi P B e Bi Ti depa t 1 E pci 1 1 w p7 e 1 r 6 Ba 7775 22 Pp Yo wil p lug Wi Yp uw 4 1 So for each w1 Wn Q the i th factor is also equal Proposition 3 5 3 Let By Xp p ea E Lp p ca B2 Wp p eh E Lo tp ca be SPBCs that have equal underlying graphs and equal labels for real numbers and formulas in all vertices except they may differ in any number of pairs Xp Ypi in the conditions of Lemma 3 5 2 Then Bi B are equivalent Proof The resu
17. number of different 5 classes Let w1 w2 Q such that wi 5 wo Base true by definition Step e In the case we have X g u1 1 Xglw1 1 Xg w2 X 28 wa e In the case 51 gt 02 we have X 8 a 01 max 1 E Xp w1 Xg w1 max 1 Xp w2 Xp w2 X 3 82 2 Let propu be the subset of propositional symbols of 6 such that X w 1 We denote by w s the s class of w Lemma 2 3 2 Let w Q ls Mto Hw D 17 A w Xp w 0 p prop 8 p prop 9 Nprop 5 Moreover w s F Proof For the first claim observe that if wi 5 wa then prop 6 prop 0 Since Xp pea are random variables and F is closed to finite intersections we prove the last claim Taking an EPPL model m Q F y X and an EPPL formula we define the quotient model m Q F u X where e Y 0 5 is the finite set of classes e F 9 is the power set c algebra e u B u UB for all B F e X us Xp w for all p A 8 CHAPTER 2 STATE LOGIC EPPL The quotient model is well defined Proposition 2 3 3 Let m 0 F u X be an EPPL model and Y an EPPL formula then m 0 F pw X is a finite EPPL model Proof By Lemma 2 3 1 Q is a finite set If B 7 then UB U s 5 s B is in F by Lemma 2 3 2 By definition we get that y s s u s a and p UM u 0 1 So y is a finite pro
18. of 6 satisfied by the EPPL model labeling that state starting with simpler subformulas This labeling is straightforward for all non temporal connectives For formulas of the form EX we label with EX all states that have a successor labeled with 6 We denote this procedure by Label EX For formulas of the form E U 5 we reason backwards We consider the con verse relation R71 the set of states labeled by 5 S and proceed by labeling with E 61U6 all states reached by at least one path considering R starting in one element of S where every state is labeled with 01 We denote this procedure by Label EU Instead of considering AF we explain the procedure for EG since checking AF is the same as checking EG 0 To check EG over M S R L consider the sub structure M S R L obtained from the original probabilistic Kripke structure where we remove all states not labeled with 6 and restrict R and L in the obvious way Now we take the decomposition of S R into strongly connected compo nents It should be clear that in any non trivial of these components EG holds since all states of the cycle are labeled with 0 and we label them accordingly We can now work backwards using the converse relation R to likewise label all states that can be reached by a path in which each state is labeled with 6 Then EG will also hold in the respective states of the original structure M and only i
19. of data structure representations To smooth the comprehension of the program we now describe and justify the ones we use in our implementation e Variables Variables are internally represented by positive ints each time the parser reads a variable name that is not yet initialized it increments a counter and initializes a fresh variable labeled by that number e Term Variables Term variables are represented by negative ints lower than 30 each time the parser reads a term variable name that is not yet initialized it decrements a counter and initializes a fresh term variable labeled by that number 49 e assignements assignements are connected lists of a structure consisting of one int the internal representation of the term variable one pointer to the real name of the term variable as specified by the user one float the value attributed to the variable and one pointer to the next term variable figure 2 35 te 0 5 T 36 van 1 Figure 2 Part of an assignement e Connectives Connectives are represented by a structure composed of one of 23 reserved negative ints standing for the connective itself and up to two pointers to the arguments of the connective e Formulas Formulas both global and basic are represented by trees of con nectives Variables are abusively represented as 0 ary connectives but easily distinguished because they are labeled with positive int
20. probabilities float ProductSum int val factorization fact float p int i int n ProductSum is a well known algorithm used to compute a product over a set of terms where information someway propagates in a directed way from term to term in our case the information of the i th entry of a valuation may be needed only in factors with index equal or greater than 1 Although this function is called an exponential number of times in A thus not re ducing the complexity class this is still much more efficient than running through each valuation in 2 and checking its probability individually int Box pformula formula int n Box computes the satisfaction of O6 where 8 is represented by formula Since createpformula substitutes all deterministic gate induced variables with their respective formula by Theorem 3 5 8 of the main reference all we need to do is run a conventional SAT algorithm over the negation of formula float evaluateterm gformula formula list terms terms factorization fact int n evaluateterm recursively evaluates a propositional term using the assignement given as input which is stored in terms for evaluating term variables and the 53 function Measure for measure terms e int evaluategformula gformula formula factorization fact int n list terms terms evaluategformula mimics the last part of Algorithm 2 evaluating global sub formulas of the input formula using the above
21. relation and L S 2 maps each state to a valuation over 4 3 Completeness of EpCTL A complete axiomatization for EpCTL is obtained simply by joining a CTL cal culus and the EPPL axioms Table 4 2 Complete Hilbert calculus HCepcr for EpCTL e Axioms EPPL all valid EPPL formulas Taut all instantiations of propositional tautologies EX EpCTL EX 91 U 03 amp EX 4 U EX s X Feperi AX T n EX T EU Fepcri E 1U95 02 U 91 N EXE 6 Uda AU Fepcri A 01U65 92 U 61 N AXA 01U69 AG1 Fepctt AG 63 D d2 N EX 3 D 93 D A 1U95 AG2 Fepctt AG s D d2 N 61 D AX03 D s D E 01U05 AG3 Feperr AG d1 D 52 D EX D EX 3 e Inference rules MP 61 D 62 Fepcrr 62 AGen Fepctt AGS As for EPPL the soundness of these axioms is straightforward and we refrain 38 CHAPTER 4 TOWARDS EPCTL from presenting it Te completeness is a bit harder and once again we follow the proof in 19 First we notice that EpCTL incorporates CTL Lemma 4 3 1 Ha then FepcTL Proof The result follows from HC ACEper Now we prove that reasoning in EpCTL over EPPL formulas coincides with EPPL reasoning Theorem 4 3 2 Let be an EPPL formula Then FEpctL 6 iff FeppL Proof If Hepcrt 6 then Fepcrt 6 by soundness of EpCTL Let m be an EPPL model and M 1 R L a temporal model such
22. state logic and it s temporal extension This work is very well covered in 19 and therefore we will provide only the general guidelines We de rive a small model theorem for EPPL which allows us to propose a PSPACE SAT algorithm for the state logic This SAT algorithm is then used to obtain a weakly 1 2 CHAPTER 1 INTRODUCTION complete Hilbert calculus for EPPL One such calculus is also obtained for the tem poral extension EpCTL and a general model checker for this logic is proposed The presentation is structured as follows In Chapter 2 we present the state logic EPPL Syntax and semantics are introduced Afterwards the small model theorem is derived and the SAT algorithm described We finish the chapter pre senting the complete Hilbert calculus for EPPL In Chapter 3 we explain the implementation of the model checking algorithm for EPPL for digital circuits We start by setting notation and implementation con straints We then describe a structure that accurately models faulty digital circuits and how it relates to EPPL A presentation of the algorithm follows along with a proof of its soundness and completeness An informal complexity analysis is also provided Since efficiency concerns are taken into account several optimization op tions are then discussed and their soundness is explained In Chapter 4 we introduce the temporal extension EpCTL much in the same way we did with EPPL in Chapter 2 We start by defining the
23. syntax and semantics of the logic then proceed to present a complete Hilbert calculus for it Finally we present the general model checking algorithm for EpCTL and discuss integration of the MC for EPPL from the previous chapter in this extended algorithm Finally in the Conclusion we assess our work and what remains to be done as well as presenting some questions for further research Main contributions The contributions of the thesis are twofold e Model checking noisy digital circuits we improved the EPPL model checking algorithm from EXPSPACE in the number of propositional symbols to PSPACE by taking advantage of realistic independence assumptions used when building the circuits e A tool that implements the previous algorithm that is a model checker that receives as input an EPPL formula and an unreliable digital circuit and outputs 1 if the formula is satisfied by the circuit and 0 otherwise Chapter 2 State Logic EPPL A probabilistic logic is necessary in order to reason about probabilistic states We will consider for this purpose the Exogenous Probabilistic Propositional Logic EPPL 17 In this chapter a succinct description and a complete Hilbert calculus for EPPL is presented as basic knowledge of the logic is required for the following chapters For a more complete reference on the logic please refer to 16 17 19 18 2 1 Syntax The syntax of EPPL follows the exogenous approach described in 1
24. that L 1 m y for some assigne ment y Hence M 1 IF 6 iff m y lr 6 So FeppL 6 By completeness of EPPL we get that FEPPL The converse follows from HCeppL C HCepcrt Consider the subset of EPPL formulas composed by modal formulas O6 and inequalities t lt t2 We will call this set the set of atomic formulas of EPPL and denote it by at EPPL Now take E to be a countable set of propositional symbols used to write CTL formulas and consider a bijective map A at EPPL gt E This bijection can be extended by structural induction to a map A EpCTL gt CTL that translates EpCTL formulas to CTL formulas e A L8 8 e A t1 lt t2 A t1 t2 e A 6 D dy A d1 gt A 82 e 20 A 6 e A EX EXA 5 e A AFS AFA 6 e A E 91U55 E A 01 UA 62 We denote by the translation of the EpCTL formula 6 by A Satisfaction is defined as expected The map A can also be used to translate a probabilistic Kripke structure M S R L to the CTL model M S R EL where amp L s iff M sl A for all CTL propositional symbol E 4 3 COMPLETENESS OF EPCTL 39 Lemma 4 3 3 Let M S R L be an EpCTL model Then M S IFEpCTL iff M S lFevr Proof The proof follows by induction on e Base If is L18 or ty t2 then M s I 6 iff M s I 6 by definition e Step
25. 0 43 xii CONTENTS Bibliography 45 EPPL model checker User Manual 47 List of Figures 3 1 3 2 3 3 oF WwW N RA Sample patera aa aa a Pad CY x DAS d d 17 SPBC for double coin tossing example 18 Equivalent SPBCs e e e 24 Circuit representing Boolean function f 32 EPPL MC tool environment eee 48 Part of an assignement 49 Representation of 0 x1 gt ti lt f x2 V z3 49 Part ot a factorizationi iu scor seo oo b DAE IRE RA 50 MTBDD for a Boolean function leen 51 xiii xiv LIST OF FIGURES List of Tables 2 1 2 2 3 1 3 2 4 1 4 2 Syntax o EPP zt ue sp berto Pane e a UE UR 3 Complete Hilbert calculus for EPPL 12 Distributions of X and Y 000000000 25 Function f 20 dp tae ddl OW ee ee bebe VR hA 31 Syntax OD EpCTE ra ete ie E TE E dad bork I 35 Complete Hilbert calculus HCepctt for EPCTL 37 Correspondence between syntaxes and internal representation 53 XV Xvi LIST OF TABLES Chapter 1 Introduction There are numerous situations where reasoning about probabilistic systems is necessary in fields as diverse as randomized algorithms security distributed sys tems reliability or quantum computation When working with these systems considering formal logics that capture their probabilistic behavior is a good way
26. 1 to 2 do If G w 0 amp amp fact w gt 0 B i 0 break Y end end for j 1 to sub d do miis f 6 M i 0 for j 1 to 2 do IFB 1 M i M i fact w y end end for i 1 to pst d do switch t do case 2 T i z 5 case 0 or 1 T i ti case t t T i 2 T 3 T l case t ty T i T 3 1 l case m t T i M j T l case mj t T i MG TO case t m T t 2 T j M l case tjm T i T M 0 end end for i 1 to gsf d do switch 6 do case L18 G i B j case tj lt ti G i T TO case m ti G i M j T case tj lt mu G i TG M D case m lt mi G i M j M I case 0 D G i max 1 G 3 G l case 5 G i 1 G j end end Assuming that all basic arithmetical operations take O 1 time we see that the first part of the algorithm takes 555 254 5 O 2 O B O fact 3 4 THE BASIC ALGORITHM 23 Oa coso QU Xs ens OU act O 2 O 8DO 9 fact O 2 6 fact The second part takes likewise Xy Besig O 2 O 8 O fact O 2 9 fact The third cycle runs O times each case being a basic operation or taking O 8 time since both suby 9 lt and pst d lt The cycle runs in O 6 Finally the last cycle runs O times each case taking
27. 3 0 9999 Y1 10 5 Y2 10 5 Y3 10 5 NY1 Y1 1 NY2 Y2 1 NY3 Y3 1 A4 NY1 amp NY2 amp Y3 0 9999 A5 NY1 amp Y2 amp Y3 0 9999 A6 Y1 amp NY2 amp NY3 0 9999 O2 A1 A2 A3 0 9999 This is the SPBC that we introduce in our tool We now want to check the property If the inputs on both boards agree then will the outputs also agree with probability greater than the security parameter p which is expressed by the formula oa e vo ca e vo aa Y3 gt 014 02 gt p In the tool s notation HS X1 lt gt Y1 amp X2 lt gt Y2 amp X3 lt gt Y3 gt 01 lt gt 02 gt fp Now if we check this formula using the security parameter for the toy p 0 999 the MC returns that the property holds for the introduced circuit meaning that Hypotetical Co can use the cheaper version of the circuit for this purpose If we run the MC with the stricter security parameter of 0 99995 the test fails meaning that it is not wise to produce the cheap circuits for the medical devices 34 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL This does not mean that the medical devce circuit has to be the most expensive possible Playing a little with the MC we can show that the Or gate or one of the And gates and no more can be substituted by the cheaper version without significant reduction of the circuit reliability producing a more affordable circuit
28. 3 T4 0100 0101 0111 1000 1010 1011 otherwise Hi ro tol co coll KA Za o MIO c Figure 5 MTBDD for a Boolean function Quick library of functions We now provide a very brief description of the main functions in our program e factorization createfactorization char filename int n deterministics dep createfactorization takes a file where a SPBC is specified and recursively builds a factorization that will be stored in memory Also taken as arguments are a pointer to an allocated int that keeps track of how many variables have been created so far and a pointer to the list of deterministic gates and their respective formula this list starts as empty e pformula createpformula char string factorization fact deterministics det createpformula creates a basic propositional formula from a string either the labeling formula in a SPBC description a subformula of a global formula or an isolated basic formula in a file As described in the previous section formulas are trees of connectives and the internal representation of variables are positive int Therefore one needs the factorization as a translator tool from the names of variables given as input to their internal representation If any of the variables in the formula are induced by deterministic gates they are substituted by the respective propositional formula in the process This way no variables indu
29. 4 represents a circuit that computes this function 31 32 23 f 0 0 0 10 0 0 1 1 0 1 0 1 0 1 110 1 0 0 10 1 0 1 1 1 1 0 10 1 1 1 0 Table 3 2 Function f lthe minterm form for a Boolean function is an analog of the disjunctive normal form for a formula that represents it 32 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL T1 T1 T2 19 T3 T3 Figure 3 4 Circuit representing Boolean function f Now suppose a circuit manufacturing company we will call it Hypothetical Co for ease of reference that produces the above circuit for two different purposes say a medical device controller and a toy controller An independent entity preforms quality control on the circuits produced Actual quality control over a lot of circuits is preformed in a way very similar to the following e two produced circuits are randomly chosen e a uniform random input is chosen from 0 1 k the number of inputs of the circuit e the input is fed to both circuits and the output is read e if the outputs disagree the circuits fail the test Otherwise they pass The lot is rejected if a significant specified by the buyer proportion of failures occur These controls usually test for very high reliabilities so that the probability of a false positive ca be neglected The objective of Hypothetical Co is to produce the cheapest possible circuits that still pass the quality contr
30. 8 We start with a base language propositional in this case and define a language at an higher level taking base formulas as terms The formulas of the base language basic formulae are simply classical proposi tional formulas over a finite set of propositional symbols A that is our abstraction of the program variables and states We introduce a set of probabilistic terms that represent real numbers to allow for quantitative reasoning The formulas of the second level global formulae allow us to perform proba bilistic reasoning over basic formulae and probabilistic terms The syntax of the language is given by mutual recursion as presented in Table 2 1 b p 8 8 gt 8 basic formulae t z 10011 S Alero tt probabilistic terms OB t t 8 6 gt global formulae where p A z Z Table 2 1 Syntax of EPPL Although we use the syntax in Table 2 1 for all theoretical purposes in this work the syntax of formulas in the tool itself differs very slightly in order to simplify the 3 4 CHAPTER 2 STATE LOGIC EPPL actual implementation The deviations are dully explained in the Annexes Classical abbreviations for propositional connectives like disjunction 8 V Ba conjunction 8 82 and equivalence 81 lt gt 2 are used freely throughout this work for basic formulae Probability terms denote elements of the real numbers We assume a finite set of real variables
31. IH 61 D 62 iff m y IH do or m y Il Closed terms are defined as terms where no real variables appear A global formula involving only closed terms is called a closed global formula As the denota tion of closed terms is independent of the assignement we will drop the assignement from the notation in such cases Remark 2 2 1 Let Vm vu w Q be the set of all valuations over A in duced by m Consider for each i 0 1 l the set B v Vm u pi ires V p o tay for pi pjaj A and in the n th bit of i Let Bm be the set of all such B Observe that an EPPL model m Q F u X induces a proba bility space Pm Vm Fm Hm over valuations where Fm C 2 is the c algebra generated by Bm and um is defined over Bm by um B u w Q v Bj for all B Bm Moreover given a probability space over valuations P V F y we can construct an EPPL model mp V F u X where X v v p Since X5 1 w E 0 Xg w 1 w E Q Blu 1 it is easy to see that m and mp satisfy precisely the same formulas Example 2 2 2 Consider an EPPL model describing the toss of two fair coins and checking if any of them comes up heads 1 Each coin represents a probabilistic bit as does the checking action that is the set of propositional symbols is A p1 p2 p3 where p models one coin pa models the other coin and p3 models the checking action The outcome of tossing the two coins and c
32. Q such that w Xs 0 Since u w gt 0 and X51 N X5 0 6 Alma X 1 lt 1 n 18 OS is actually introduced as an abbreviation of f 8 1 but slight dif ferences in semantics do not allow us to take this shortcut in this work Finally we can claim the following result Proposition 3 5 7 Let X be completely dependent of X Xp by means i 1 of f m be an EPPL model induced by a SPBC y an assignement and 6 a global formula Then Pi 1 m l iff m y IF So e yi Proof Notice that all nonbasic subformulas of remain unchanged by the substi tution Therefore if we prove both that f B m Lf 8 Im and that fpi 1 m y IH OB iif m y IF f opos the result will follow In view of Remark 3 5 6 we need only prove that f Bl Lf Bro oe pm LS Bm n X5 1 ww EN Xp 1 URE mola A o idee Xa 1 aa c O LEA Py Pi pi We show that w E 0 Xg v 21 2 o Q0 X grina w 1 noia wand DA Ease and has no elements with measure zero by elementary measure theory w Xi41 w HXi w Xi w 9 Let w w EN Xg w 1 As w EN Xp w f Xp w Xp w Then it must be the case that X ri 1 w 1 as all functions in the re fis sP1 cursive definition of X grita are evaluated in the same way as in Xg and Prop m pi f Xp w Xp w agrees with Xp w Therefore w w
33. X X7 Q 2 1 lt i lt n where X is the state of the coin at time 1 lt i lt n 1 and Xj is zero if the coin will never be in state heads from time n and one otherwise In this case the basic formula Bo pi1 A pa 1 pn represents the configuration 0000 and m IF f Bo lt 0 but m Y 0 80 Given that we are working towards a complete Hilbert calculus for EPPL through a SAT algorithm it is relevant to understand whether EPPL fulfills a small model theorem If this is the case then an upper bound on the size of the satisfying models would imply the decidability of the logic since it would be enough to search for models up to this bound 2 3 Small model theorem The technique used in 10 to obtain a small model theorem is adapted in 19 for EPPL Let 6 be an EPPL formula We denote the sets of inequalities basic subformulas and propositional symbols occurring in by ig 6 bsf 6 and prop respectively Given a formula and an EPPL model m 0 F pu X we define the following 2 3 SMALL MODEL THEOREM T relation on the sample space Q wy s we iff Xp w1 Xp w2 for all p prop Lemma 2 3 1 The relation s is a finite index equivalence relation on Q and if Wi vs Wa then Xg w1 Xg wa for all B bsf 6 Proof Clearly s is an equivalence relation since equality is an equivalence relation as well The set prop is finite so it allows only a finite
34. a solution model to x Since x is polynomial on and the set of variables in k is polynomially bounded by the Sat Real will compute the solution in PSPACE If such solution p exists we have succeeded in finding a model for 6 Hence we return V mp and Yp Where up v is p x and y is the restriction of p to var As stated in Remark 2 2 1 this is enough to construct an EPPL model If there is no solution p then we cannot find a solution for the set V of valuations and have to try with another V Finally if for all e and V we are not able to find a solution then there is no model for 2 5 Completeness of EPPL It is shown in 18 that EPPL is not compact therefore it is impossible to obtain a strongly complete axiomatization for EPPL Nevertheless weak completeness is enough for verification purposes since a program specification generates a finite number of hypothesis The EPPL SAT algorithm allows us to show that the calcu lus presented in Table 2 2 is weakly complete The soundness of the calculus of Table 2 2 is straightforward and so we focus on the completeness result Theorem 2 5 1 The set of rules and axioms of Table 2 2 is a weakly complete axiomatization of EPPL 12 CHAPTER 2 STATE LOGIC EPPL Table 2 2 Complete Hilbert calculus for EPPL Axioms e CTaut Hepp 06 for each valid propositional formula 8 e GTaut Hepp for each instantiation of a propositional tautology 4
35. and Computation 87 1 2 78 128 1990 H Hansson and B Jonsson A logic for reasoning about time and reliability Formal Aspects of Computing 6 5 512 535 1994 H Hermanns M Kwiatkwoska G Norman D Parker and M Siegle On the use of MTBDDs for performability analysis and verification of stochastic systems Journal of logic and algebric programming 56 1 2 23 67 2003 13 A F Karr Probability Springer Verlag 1993 45 46 14 15 16 17 18 19 20 21 BIBLIOGRAPHY M Kwiatkowska G Norman and D Parker Probabilistic model checking in practice case studies with PRISM SIGMETRICS Perform Eval Rev 32 4 16 21 2005 Marta Kwiatkowska Gethin Norman and David Parker PRISM Probabilistic symbolic model checker In TOOLS 02 Proceedings of the 12th International Conference on Computer Performance Evaluation Modelling Techniques and Tools pages 200 204 London UK 2002 Springer Verlag P Mateus and A Sernadas Exogenous quantum logic In Proceedings of CombLog 04 Workshop on Combination of Logics Theory and Applications pages 141 149 2004 P Mateus and A Sernadas Weakly complete axiomatization of exogenous quantum propositional logic Information and Computation 204 5 771 794 2006 P Mateus A Sernadas and C Sernadas Exogenous semantics approach to enriching logics In G Sica editor Essays on the Foundations of Mathematics and Logic volume 1 pages
36. babilistic measure over Q If we prove that satisfaction is preserved by the quotient construction then any sat isfiable formula has a finite discrete EPPL model of size bounded by the formula length Theorem 2 3 4 Small Model Theorem If 6 is a satisfiable EPPL formula then it has a finite model using at most 2 6 1 algebraic real numbers Proof Let m Q F u X be an EPPL model of 6 and m m s its quotient model that is a finite discrete EPPL model of size 2 P P 21 In the quotient model m we need a real number for each valuation over prop therefore we need at most 2 real numbers We start by proving that m satisfies 6 Note that m and m agree in the denotation of probabilistic terms The only non trivial case are the terms f 8 For 8 bsf 6 and using Lemma 2 3 2 we get f Sly Xp 1 WU XG 19 Xp 1 Lf Fm for any assignement of the real variables By structural induction on terms of 6 we get that m and m agree on inequations For any subformula 18 of 6 we have that m y lr O8 iff Q Xx 1 iff O X5 1 iff m y IF L18 Now since m and m agree on inequations ty lt t2 and modal formulas OZ we get by structural induction that m is a model for Finally we will simplify m to obtain a model m Q 29 u X of 6 such that Q lt 2 6 1 Let bsf 6 B1 8
37. ced by deterministic gates ever appear in internal rep resentation of formulas e gformula createterm char string list terms list factorization fact deterministics det int t createterm creates a term from a string The second argument is used as a translator from input given term variable names to their internal represen tation The factorization and list of deterministic gates are given as input 52 EPPL MODEL CHECKER USER MANUAL because it may be necessary to call createpformula in order to parse a basic subformula in a term of the form f 8 The pointer to the allocated int keeps track of how many term variables have been created so far gformula creategformula char string factorization fact list_terms terms deter ministics det int t creategformula creates a global formula from a string the sole line in a file The other arguments are only needed because this function will call createterm and createpformula float Measure pformula formula factorization fact int n Measure returns the probability of a given basic formula It is essentially a cycle that in each iteration computes the next valuation that satisfies the formula actually it computes several valuations in each cycle since we allow don t care values uses a product sum algorithm and the method proposed in Proposition 3 3 3 of the main reference to compute its their probability and adds it to the sum of the previously computed
38. e is a whitespace after each connective The syntax should be clear var stands for any variable name stands for amp stands for A stands for V gt stands for gt and lt gt stands for Variable naming is duly covered in the Appendix For terms the syntax is as follows t term 0 1 9 t t dt t The syntax is straightforward the only connective that needs explaining is which stands for f Remember the variable naming conventions for term variables The seemingly redundant around the variables and constants are necessary in order to contextualize the parser Finally for global formulas the syntax is 46 e lt de gt t e lt ti e gt dled 16 9 amp amp 6 o 9 gt 6 lt gt 9 Once again the peculiar parenthesis are necessary to contextualize the parser As for connectives lt gt and stand for themselves stands for stand for gt and amp amp gt lt gt stand for N U D respectively Take for example axiom FAdd from Table 2 2 For this tool s purposes it should be written as 5 amp 55 0 gt HSV 82 5A 62 As for SPBCs the file with the description should contain one line for each vertex The line starts with the name of a fresh labeling variable that will be 3 6 EPPL MC TOOL 31 _ identified with the induced random variable followed by an
39. ed analytical formulas This language is relevant because it is possible to apply the SAT algorithm for the existential theory of the real numbers to any analytical formula 2 2 Semantics The models of EPPL are tuples m Q F u X where Q F p is a probability space and X X pea is a stochastic process over Q F u where each X is a Bernoulli random variable that is X ranges over 2 0 1 Therefore each w Q induces a valuation v over A such that v p Xp w for all p A In addition each basic EPPL formula 8 represents the measurable subset w Q 5 v 1 where B v is the denotation of 8 by vw Moreover each basic EPPL formula 6 also induces a Bernoulli random variable X8g 0 2 e X sy w 1 Xa w ha X 81 82 7 max 1 Xp w Xa w 2 2 SEMANTICS 5 A simple argument of structural induction shows that w Q B v 1 iw EN Xg w 1 Given an EPPL model m 9 7 X and assignement y for real variables the semantics of global formulas is defined in the following way e Denotation of probabilistic terms E 2 m yz Dlm 0 m y 1 amp ta deny ltilm y t21m y 1 t2 my Dl Eo KS Olm p X5 1 is the probability of observing an outcome w such that v satisfies B e Satisfaction of global formulas m l 08 if Q X5 1 m y le ty lt to iff t X ta my m lk 9 iff m y IF m
40. ed in e Given an exhaustive conjunction e of literals of at 9 we denote by lbfg e the set of basic formulas such that 8 lbfg e if OG occurs positively in e that is not negated Similarly the set of basic formulas that occur nested by a O in e is denoted by lbfy e Finally we denote all the inequality literals occurring in e by lig e Given a global formula a in lig e we denote by TM the analytical formula where all terms of the form f 8 are replaced in a by 35 ey ur g tv Where 10 CHAPTER 2 STATE LOGIC EPPL each x is a fresh variable We need a PSPACE SAT algorithm of the existential theory of the reals numbers that we denote by SatReal We assume that this algorithm either returns no model if there is no solution for the input system of inequations or a solution array p where p x is the solution for variable x We denote by var the set of real logical variables that occur in Given a solution p for a system with X variables and a subset Y C X we denote by pjy the function that maps each element y of Y to p y Algorithm 1 SatEPPL 6 Input EPPL formula Output V y denoting the EPPL model m V 2 1 X and assignement y or no model compute bfn ig and at 6 foreach exhaustive conjunction e of literals of at 9 such that ve IF 05 do compute Ibfn c lbfo e and lig e foreach V C 2 ro such that 0 lt V lt 2 1
41. ely SPBCs are built in such a way that some degree of independence is maintained between the variables We will explore this property in order to get an efficient representation of the EPPL model associated to each PBC For this we will need a very simple proposition Lemma 3 3 1 Let X4 X be discrete random variables Then for all 11 tn Q P X euo Xn n Ewes ti Xi 1 Li 1 A1 21 i l where P X til Xii Li 1 X1 21 u l P X zi Xi 1 i 1 X1 1 if P Xi 1 zi 1 X1 101 4 0 0 otherwise Proof The proof is presented by induction in n Base P X z PX z Step If P X 1 Xn 1 Xn 1 0 then P X 1 Xn Ln 0 because w X w z1 Xn w n C w Xi w 21 Xn 1 w tn If P X 2z1 Xn 1 z4 1 Z0 then P X 24 Xn tn P Xnr LX 21 54 Xn 1 Un 1 P X1 21 Xn 1 n 1 by definition of con 3 3 FACTORIZATIONS AND BAYESIAN NETWORKS 19 ditioned probability By induction hypothesis P X t1 Xn 1 Tn 1 M P X a Xii Li Xi 21 Therefore P X Tips na eT PX zi Xi 1 A aes 21 We shall henceforth drop the superscript in P whenever no ambiguity arises A rewriting of a joint distribution function in the above form is called a factorization Since representing the conditional distributions P Xp Xp _ Xp in the worst case may take O 2 space using factorizat
42. eneral EPPL MC algorithm if we restrict ourselves to structures where the image of the map L is in the set of EPPL models induced by SPBCs Unfortunately programs written with the probabilistic programing language presented in 19 do not generate such models and it is unlikely that a really useful language that generates them exists In fact a simple reatribution of a variable has the potential to break the acyclicity of a SPBC We could circumvent this problem by introducing a new variable for each such command but this would be unfeasible by obvious efficiency reasons Another more likely solution to be exploited in future work is to use MTBDDs Since a MTBDD is a canonical way to represent a 42 CHAPTER 4 TOWARDS EPCTL function f 0 1 R an EPPL model can be represented by a MTBDD using as little space as possible T his representation can be further refined in some cases by using factorizations to decompose the set of propositional symbols into independent subsets and representing each one with a smaller MTBDD However although canonical these representations do not avoid taking exponential space in A Chapter 5 Conclusion In this work we presented in detail the implementation of a PSPACE model checking tool for non reliable digital circuits using a very expressive probabilistic logic The model checker itself is a flexible tool with the potential to be adapted for more complex structures albeit at the cost of co
43. et of deterministic gates in the SPBC Proof If s _ p1 38 satisfiable there is a valuation w 2 A D st G y e 1 Let w 2 be the valuation that coincides with w in all p AX D and that has wi y w 1 w1 for all p D this computation should be made by index order fact w Tk Tidus o 1 ri wyi pe ri oso 1 rir wi ps Hemp Ti o FU ps ILep 1 0 T I eA p Tias pi 1 r b1 wi gi IIperplidw gi 1 r 01 w 6 Each ri and 1 r in the last product is greater than zero and one of the 6 in each term is 1 It follows that fact w gt 0 that is wER 8 w 1 as we have seen in the proof of Proposition 3 5 7 Since p w gt 0 w Q then x fact I DB iff there is w Q s t w X3 0 i e there is w Q s t w X Cy 1 ie there is w Q s t 28 w 1 which we have just proved If ecos 255 is not satisfiable for all valuations w 21D we have that pie D e Pos TON py 1 For each w 24 only the w 2 built in the same way as in the first part of the proof verifies fact w gt 0 i e w Q if wi pi w 1 wW1 for some p AX D the corresponding term in fact w ridu o 1 7 d1 w 1 0 0 1 0 and fact w 0 Furthermore there are no more valuations in Q than those of this MD a pie D form or there would be w 20 s t Eo ap 0 Once again by proposition 3 5 7 8 w 1 This is true fo
44. functions However unlike Algorithm 2 instead of starting by evaluating all subformulas this routine tries to evaluate as little of them as possible in order to reduce computing time EPPL Symbol Computer Symbol Internal Representation amp amp 1 IUC D IO JIC Y lt gt VIA vI A HS y n ER 0 propositional 0 1 propositional 1 0 term 0 1 term 1 21 Table 1 Correspondence between syntaxes and internal representation
45. gical gates which happens in practice The following definition builds upon the concept of Boolean circuit allowing a proba bilistic error Definition 3 2 1 A probabilistic Boolean circuit PBC is a directed acyclic graph where each vertex i is labeled with a Bernoulli random variable R with expected value r a fresh Boolean variable x and a Boolean function g 0 1 0 1 with domain in the variables labeling vertices pointing to i A vertex whose indegree is zero is called an input vertex and its labeling variable is called an input variable A vertex whose outdegree is zero is called an output vertex and its labeling variable is called an output variable A vertex that is neither an input vertex nor an output vertex is called an internal vertex If there is an arrow pointing from vertex i to vertex j 7 is said to be a child of and is said to be a parent of j The set of parent vertices of a vertex i is denoted by par i Each non input vertex represents a logical gate that computes the Boolean function expressed by the formula f This computation returns the correct output with probability r The variable x does the double duty of identifying the vertex and representing the outcome of this probabilistic computation For implementation purposes we notice that in order to specify a vertex we only need the associated expected value r that we will represent with a floating point between 0 and 1 the variable x
46. hecking is described by m 000 011 101 111 2 001 011 101 111 X where p zyz 1 Xp 1yz x and X zyz y and Xp zyz z for all x y z 0 1 s t z maz z y It is easy to see that m lr 1 1 1 1 f pa 1 1 1 which we abbreviate to ml f ps 3 6 CHAPTER 2 STATE LOGIC EPPL Example 2 2 3 Consider the more sophisticated experiment of tossing a fair coin until the outcome is heads 1 s This process can be modeled by the struc ture m Q F u X over a countable infinite set of propositional symbols A in 05 Pn Ts where Q 00 0111 k gt 0 F 2 k and X Q 2 is the state of the coin at time N for all p A with p 00 0111 k gR I for k gt 0 and zero otherwise m is not an EPPL model as A is infinite If we were to push the definition and consider the same semantics allowing infinite sets of propositional symbols we would have for example m IH O p gt pi41 for all i N Given the configuration 00 0111 we could represent it by the basic formula Ep apo A apr NdR but the configuration 0000 could not be represented by any basic formula because we don t allow infinitary conjunctions To avoid this limitation we can group all variables of some index or higher in a single variable and consider instead the model m Q F u X over A p1 Pny such that Q F u as above and
47. ifi INSTITUTO SUPERIOR T CNICO Model Checking Probabilistic Systems David Jo o Barros Henriques Disserta o para obten o do Grau de Mestre em Matem tica e Aplica es J ri Presidente Prof Dra Cristina Sernadas Orientador Prof Dr Paulo Mateus Vogal Prof Dr Carlos Caleiro Vogal Prof Dr Jaime Ramos Marco de 2009 ii Resumo Neste trabalho apresentamos a implementacao de uma ferramenta de verificagao de modelos eficiente para f rmulas de uma l gica probabilistica formal EPPL so bre circuitos digitais n o fi veis Para aumentar a efici ncia capitalizamos em v rias propriedades espec ficas destas estruturas ainda assim o programa mant m se muito flex vel permitindo f cil adapta o a outros modelos mais complexos Tamb m introduzido um m todo para minimizar problemas de espa o em verificadores de modelos sobre um subconjunto de sistemas probabil sticos repre sent veis por redes Bayesianas Para tal consideramos factoriza es dos processos estoc sticos associados aos espa os de probabilidades gerados pelos sistemas Sao discutidas implica es de considerar uma extens o temporal sobre a l gica proposto um algoritmo de verifica o para o caso temporal e s o apresentadas op es de implementa o Palavras chave Sistemas probabil sticos verifica o de modelos circuitos digitais l gica temporal l gica probabil stica iii iv Abstract In this
48. ions is not in general an effi cient way of representing EPPL models as we could need 7 O 2 O 2 1 space However in a SPBC each variable induced by a vertex depends exclu sively on the variables of vertices that point to it and so P Xp Xp _ Xp P Xp par X p o The structure we just described is known as a Bayesian network Definition 3 3 2 A Bayesian network relative to a set of random variables is a directed acyclic graph where each vertex is labeled with one of the variables and the joint distribution of those variables can be written as the product of the conditioned probability of each vertex and its parents P X is Xn TIE P Xilpar X Bayesian networks have the expressive power to determine all EPPL Models since one can always consider the Bayesian network where the parents of the vertex labeled with X are all vertexes with label Xx k lt i effectively performing a factor ization However we have seen that in the worst case there are no gains in space representation from using this approach relative to using the explicit description of the probability distribution Nevertheless Bayesian networks are a well studied object and perhaps some results from their general theory could yield interesting consequences when studying SPBCs 20 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL Fortunately SPBCs have another property that further reduces the complex ity of the Model Checking algor
49. isfies the same formulas Due to this identification the elements of the sample space will be abusively referred to as valuations We will also assume that there are no valuations in with zero measure so it is possible that some valuations are not represented in Q Under these assumptions knowledge of the joint distribution of the random vari ables X is enough to describe an EPPL Model Given P x Xp Xp gt pn 15 16 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL e Q x 24 P Xp 41 24X5 24 gt 0 F 2 e u w P Xp wi Xp Wn Q being finite it is enough to define u for each singleton set w C Q Since we have to deal with computer representation probabilities will be rep resented by floating points and not symbolically by algebraic real numbers This is not a major theoretical problem as floating point numbers represent rational numbers which are algebraic numbers however issues of lack of precision for us ing floating point representation cannot be easily avoided In this work we do not preform an error analysis due to floating points which is also the case for other model checkers like PRISM However we do try to minimize the number of op erations that manipulate probabilities in order to slow the propagation of these errors 3 2 Probabilistic Boolean circuits Boolean circuits are the standard choice to model digital circuits However they lack structure to account for error in lo
50. ithm the probability of correctly computing the Boolean functions expressed by the labeling formulas ie P X pi par Xp is known With this information we can prove the following result Theorem 3 3 3 Let X Xp be the variables induced by the vertices of a SPBC and z4 n a valuation then n P Xp fi X Pn tn Meg Tide git 1 ri di Ti Pi where r is the real number labeling i and dz p i i E Li Pil eo Bir O if a c1 1 Proof In this proof we denote by par Xp par x the set fr Q Xp Ti Xp par Xp In view of Lemma 3 3 1 it suffices to prove that P Xp zi Xy ti 1 Xp 207 fa Fn e Using the Total Probabilities theorem with the partition Q Q 5 U Qr p where Q2 y Q zx pi t 1 81 we have PX tilde 21 PG a par X par zx P Xp pilpar Xp x P Xp xilpar Xp par xi Xp pilpar Xp P Xp 4 pilpar Xp x P X vilpar Xp par zi Xp pilpar Xp ri X Plz pilpar x 1 ri x P vi 4 gi par z d x and P xi gi par x if zi al if Ti pilar so di 1 ie 1 Xi pilas nadia if x pila dii 1 4 Lay LJ 0 Ly Ti 1 0 Pla vi par zi O 21 pi gt This Theorem provides a very simple way of computing the probability of any given valuation as we need only to check for each vertex if the denota
51. liability and furthers some previous work It also raises a few interesting questions and problems which we believe may constitute an interesting topic of 43 44 CHAPTER 5 CONCLUSION further research Bibliography 10 11 12 S Basu R Pollack and M Roy Algorithms in Real Algebraic Geometry Springer 2003 R Bryant Graph based algorithms for boolean function manipulation EEE ToC 35 8 677 691 1986 R Chadha L Cruz Filipe P Mateus and A Sernadas Reasoning about probabilistic sequential programs Theoretical Computer Science 379 1 2 142 165 2007 V Chvatal Linear programming Freeman 1983 E Clarke M Fujita P McGeer K McMillan J Yang and X Zhao Multi terminal binary decision diagrams an efficient data structure for matrix rep resentation Formal Methods in System Design 10 2 3 149 169 1997 Edmund M Clarke and Bernd Holger Schlingloff Model checking Handbooks of automated reasoning 190 3 2007 C Courcoubetis and M Yannakakis The complexity of probabilistic verifica tion Journal of the ACM 42 4 857 907 1995 E A Emerson and J Y Halpern Decision procedures and expressiveness in the temporal logic of branching time STOC pages 169 180 1982 R Fagin and J Y Halpern Reasoning about knowledge and probability J ACM 41 2 340 367 1994 R Fagin J Y Halpern and N Megiddo A logic for reasoning about proba bilities Information
52. lt follows by transitivity of the equivalence relation and Lemma 3 5 2 Henceforth we will assume that all SPBCs labeling real numbers are at least i This can be done because we can always build a SPBC with this property that is equivalent to any SPBC given In any vertex of the original SPBC with labeling number r less than 3 we change the labeling formula y to p and labeling num ber 1 r 3 5 2 Deterministic gates Suppose a SPBC where one of the vertices is labeled with the real number 1 This amounts to saying that the connective of the digital circuit that is modeled by that vertex is completely reliable deterministically providing an output for given sets of input rigorously providing the correct output for given sets of input with probability one but since the sample space is finite and does not have elements with measure zero we allow ourselves the language abuse 3 5 OPTIMIZATIONS 27 We will call a vertex with this property a deterministic gate Deterministic gates will allow some simplifications in our algorithm essentially removing one symbol from A for all implementation purposes The idea is that if x qi 2 4 21 with r 1 then we can substitute all instances of X in all formulas that need to be verified by pi Xp _ Xp Definition 3 5 4 Let X Xp be discrete random variables X is said to i 1 be completely dependent of Xp Xp by means of f if po Xp w
53. mputational resources mainly space Since it has been designed with efficiency concerns several optimizations were implemented and thoroughly justified We also introduced an alternative way of representing EPPL models generated by probability spaces over valuations through the factorization of the joint proba bility distribution of the variables of the associated stochastic process Although no efficiency improvement is guaranteed only a little independency between the variables is needed to make this procedure worthwhile It is possible to expand the model checker to arbitrary EPPL models despite the fact that doing so breaks the PSPACE complexity We have already proposed in Chapter 4 an approach to this problem using MTBDDs This data structure can easily be integrated in the present tool and seems promising in terms of effi ciency Another useful research path would be the development of a programming language that generates probabilistic Kripke structures whose labeling functions returned only SPBC generated EPPL models We leave these approaches to be ex plored Building upon the last suggestion the implementation of the extension of the MC to check over EpCTL formulas could also prove valuable In fact as we have seen in Chapter 4 a simple adaptation of any standard CTL model checker is enough to successfully implement an EpCTL one Overall our work provides a useful and effective tool with clear applications in circuit re
54. n those because there are no more states labeled by 6 We denote this procedure by Label EG In the model checking algorithm for EpCTL described below we denote by subcr the ordered list of global subformulas of 6 4 4 MODEL CHECKING ALGORITHM FOR EPCTL 41 Algorithm 3 alg epctl Input temporal model M S R L and EpCTL formula 6 Output M with states where 6 is satisfied labeled with 6 for i 1 to subcri 0 do switch do case 08 or t lt t3 forall s S do if CheckEPPL L s 0 then Label s Label s U 06 or Label s U ty te end end case forall s S do if s then Label s Label s U 795 end end case 0 D forall s S do if 6 s or s then Label s Label s U gt di end end case EX Label EX case E 0 U i Label EU case AG LabelAG end end The soundness of this algorithm can be checked following the proof in 6 with minor adjustments namely in the first case If we use the algorithm presented in 19 to preform the EPPL checking the temporal model checking procedure will run in O l J Q S R time the outer for runs O 9 times the EPPL MC cases take O 2 S time and the other cases take O S R time It is clear that Algorithm 3 can be adapted to check EpCTL formulas over models M S R L using Algorithm 2 instead of the g
55. ogic cannot specify transcendental real numbers with a single formula we need an infinite number of formulas to be able to specify a transcendental real number so the solution of the system can be made just with algebraic real numbers The size of the representation of the algebraic real numbers can increase without any bound Fortunately thanks to the fact that the existential theory of the real numbers can be decided in PSPACE we find a bound on the size of the real repre sentations in function of the size of the formula which will lead to a SAT algorithm for EPPL 2 4 Decision algorithm for EPPL satisfaction Given an EPPL formula we will denote by ig the set of all subformulas of of the form ty to by bfg d the set of all subformulas of 6 of the form O8 and at 6 bfy Uig s By an exhaustive conjunction e of literals of at 6 we mM mean that e is of the form o4 N N az where each a is either a global atom or a negation of a global atom Moreover all global atoms or their negation occur in e so k at d Given a global formula 6 we denote by dp the propositional formula obtained by replacing in 6 each global atom a with a fresh propositional symbol Pa and replacing the global connectives and D by the propositional connectives and gt respectively We denote by v the valuation over propositional symbols Pa such that ve pa 1 iff a occurs not negat
56. ol Cheaper components are less reliable than ex pensive ones We will show how to use our MC tool to ease the decision making procedure Suppose the toy circuit board has an accepted failure ratio of Tomo and the medical device circuit board has an accepted failure ratio of 55 55 Suppose also that Not gates are easy to make and very reliable so we will assume they always perform the computation correctly And and Or gates on the other hand have two versions a cheap one with 0 9999 reliability and an expensive one with 0 999999 The cheapest circuit is described in our tool as X1 10 5 X2 10 5 X3 10 5 NX1 CX1 1 NX2 7X2 1 NX3 7X3 1 A1 NX1 amp NX2 amp X3 0 9999 A2 NX1 amp X2 amp X3 0 9999 3 6 EPPL MC TOOL 33 A3 X1 amp NX2 amp NX3 0 9999 O1 A1 A2 A3 0 9999 The first three lines represent the input uniformly distributed in 0 1 the three next ones represent the Not gates that are completely reliable then we have the three And gates and finally the Or output gate all with the lowest 0 9999 reliability available In order to simulate the quality control we simply replicate the circuit which is the same as running an equal one in paralel X1 10 5 X2 10 5 X3 10 5 NX1 X1 1 NX2 X2 1 NX3 X3 1 A1 NX1 amp NX2 amp X3 0 9999 A2 NX1 amp X2 amp X3 0 9999 A3 X1 amp NX2 amp NX3 0 9999 O1 A1 A2 A
57. or models where the state space O is given as a set of valuations of the basic propo sitional symbols Moreover thanks to the small model theorem Theorem 2 3 4 it is enough to search for sets of valuations V such that V lt 2 6 1 V has to satisfy the modal literals O6 and LB occurring in e that is for all 8 lbfg e and v V we have that v lr 8 which can be written as V IH Albfr e and for all B Ibfo lt there exists v V such that v If B wich can be written as V If 8 for all 8 lbfo4 e These are exactly the conditions in the guard of the second cycle of the program In the body of this cycle we will check if there is a model of e taking such V as the set of states that is if there is a solution for the inequations in lig e Since we only have to store a set of valuations V with V 2 6 1 at each step of the cycle once again we need only polynomial space Next we search for a model of the inequations in liq having a set of states V To this end we consider a fresh real logical variable x for each v V representing its probability The idea behind this step is to build an analytical formula amp that specifies the two probability constrains expressed in the fifth line and the inequations in lig e Two lines further the formula amp is finished by replacing the terms f 8 in lig by Doev virg tv In line 9 we call the Sat Real algorithm for
58. p in mind that whenever this algorithm returns 0 it should be interpreted as wt Q because we have no ele ments with measure zero in 2 The first part of the algorithm runs through all subformulas of the form O6 and through all valuations checking for each valuation both if it is in Q and if it does not satisfy the basic formula If both answers are positive for any valuation there is w Q such that w X 5 1 otherwise Q X5 1 The values of 03 are stored in a Boolean bfo 6 array B Then the algorithm runs through all subterms of the form f 8 and through all valuations checking for each valuation if it is in Q and if it satisfies the basic formula 6 If both answers are positive it then adds the measure of the valuation to M i the i th entry of the real suby 0 array M where the values of f 8 are stored The third part performs all other term evaluations it stores them in a real pst 6 array T Finally the algorithm evaluates all global subformulas to a Boolean gsf array G where G i 1 iff x fact y IF di for all 1 i gsf 6 where x fact is the model induced by fact and return as output G gsf CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL Algorithm 2 CheckEPPL fact y Input Factorization fact assignement y and a formula 6 Output Boolean value G gsf for i 1 to bfn do A is UB Bi 1 for j
59. r all w Q and so X fact Y IF OB The previous proposition allows us to compute Xfact y IF OG with a single application of a SAT algorithm for propositional logic Although still in the same complexity class of the direct computation of y fact y IH 08 the SAT problem is very well studied and many clever algorithms have been proposed to solve it Upon the use of one such algorithm we improve our own since our approach in the basic algorithm was to run through all of the 2 valuations 30 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL 3 6 EPPL MC tool 3 6 1 Syntax differences Although operational aspects of the actual implementation of the tool are left for the Appendix there are differences between the syntax of EPPL and that of the actual tool that we will discuss at this point In practice the tool parses strings inputed by the user and since ASCII en coding does not allow the representation of all EPPL symbols we need to find intuitive substitutes There are also slight differences in parenthesis that ease the implementation of the parsing tool We start by defining the syntax for basic formulas B var C8 1 6 amp 8 8 6 0 6 gt 6 8 lt gt 8 Since the parser is quite strict when using the tool we advise not to deviate from the above syntax This includes droping parenthesis or assuming associativity One should pay close attention to spacing ther
60. ro Baltazar for informally co advising me whenever the need arose My thanks extend to my closer friends both new Bruno Montalto Iris Ferreira Luis Pereira Manuel Martins Rui Palma and old time Ana Neves Bruno Mar tins Catarina Ferreira Diana Sequeira Joao Lopes Tomaz Saraiva for making these last few years so enjoyable and ultimately teaching me far more than any course could aspire to do Thank you all vii viii ix Ao meu irm o Contents Resumo Abstract Acknowledgments 1 Introduction 2 State Logic EPPL 29 AO y rba wis so ces cated th d Gaga ute mex mx e e pae sema d t fe 2 2 y Semantics 409 ik i EM Aaa A 2 3 Small model theorem 200004 2 4 Decision algorithm for EPPL satisfaction 0 0 2 5 Completeness of EPPL 0 4 3 Verifying Digital Circuits with EPPL 3 1 Notation and conventions 3 2 Probabilistic Boolean circuits 3 3 Factorizations and Bayesian networks 3 4 The basic algorithm 3 5 Optimizations 3 5 1 Equivalent SPBCs 3 5 2 Deterministic gates 3 6 EPPL MC tool 3 6 1 Syntax differences 3 6 2 A simple case study 4 Towards EpCTL dl Syntax e eat duo ae a he s 4 2 Semantics s 2 24 44 Fence 4 3 Completeness of EpCTL 44 Model checking algorithm for EpCTL 5 Conclusion xi vi o o 0 W 15 15 16 18 21 24 24 26 30 30 31 35 35 36 37 4
61. s knowledge of the joint distribution is enough to fully describe the EPPL model Since both SPBCs from Figure 3 3 induce the same distribution function we conclude that they generate the same EPPL model The previous example shows that different SPBCs can induce the same EPPL model Notice that PBCs corresponding to these SPBCs are not equal yet they 3 5 OPTIMIZATIONS 25 Table 3 1 Distributions of X and Y w Wi W2W3 P X W1 Xp Wa Xps E 43 Pi W1 Y wa Y w3 000 1 0 6 x 1 0 5 x0 3 0 06 0 4x 1 0 5 x 1 0 7 0 06 001 0 14 0 14 010 0 06 0 06 011 0 14 0 14 100 0 09 0 09 101 0 21 0 21 110 0 21 0 21 111 0 09 0 09 still induce the same EPPL model We shall say that two SPBCs induce the same EPPL model are equivalent Equivalence between SPBCs is obviously an equivalence relation Lemma 3 5 2 Let Bi Xp pica E Lp p eA B2 Ypi p cA EL pica be SPBCs that have equal underlying graphs and equal labels for real numbers and formulas in all vertices except one pair X Yp where X is labeled with the real number ry and the formula x and Y is labeled with ry py If either yz vy propositionally and rz ry or fx amp 0y and rz 1 ry then By B are equivalent Proof B and B are equivalent as long as the factorizations induced by them are equal As all terms in the factorizations except the th are equal
62. s instead of negative ints This representation allows for both an efficient interpretation of formulas often knowledge of the interpretation of one of the subtrees is enough to in terpret the whole formula and for easy inclusion of subformulas an operation that will be commonly used in the program It occupies linear space in the number of connectives and variables in the formula having one node for each of these symbols figure 3 Figure 3 Representation of 2D z1 gt ti f x2 V x3 e Valuations Valuations are represented by arrays of n 1 ints The value of the variable labeling vertex i is represented in the th element of the 50 EPPL MODEL CHECKER USER MANUAL array A 2 represents a don t care value allowing for several valuations to be represented on the same array Factor A factor represents a mix between one vertex of a SPBC and the respective term in the product that describes the joint distribution of the random variables of the stochastic process Is is a structure that consists of one int the labeling variable one float the labeling real number one pointer to the labeling formula one pointer to the real name of the variable as specified by the user and one pointer to the next vertex by numeric order of labeling variables Factorizations A factorization is the connected list of all factors It is not a representation of the SPBC itself
63. the consistency of e In case i no V can be found at the second foreach it cannot be because V gt 2 0 1 thanks to the small model theorem This means that if we remove the bound 0 lt V lt 2 1 and consider all possible sets of valuations the algorithm would also fail In particular take V 2 7 it must happen a V If Albfo e or b V IF 8 for some 8 lbfo4 e For case a we have that If Albfg e and so Y 8 for some 8 lbfg e or equivalently lr 8 gt 1 But by completeness of the propositional calculus we have that 8 gt L by CTaut we have that O 8 gt L and by Lift and EqvL we have that 08 from which follows e which contradicts the consistency of e In case b there is 8 lbfg e such that B is a tautology Then by CTaut L18 From the last derivation we get e which contradicts the consistency of e In case ii the algorithm returns no model for all viable V computed in the 2 5 COMPLETENESS OF EPPL 13 second foreach Thanks to the small model theorem it means that the algorithm would also return no model for all V such that V IF Albfo e and V If 8 for all 6 lbfo e 2 1 independently of the bound on the size of V The sets of valuations satisfying 2 1 are closed for unions and therefore there is the largest V fulfilling 2 1 say Vmax and for this set the algori
64. thm would return no model Let VC gprop 6 V Vinax since e is consistent it is easy to see that amp e N Nvey LI7G is consistent where 3 is a propositional formula that is satisfied only by valuation v Therefore Fe De Moreover F Albfa e 10 for all v V from which we derive that E Ngemfo 8 gt NveveOBy and so e D el and therefore amp e Thus if e is consistent then e is also consistent and if there is no model for e then there is no model for e as well and the algorithm will fail precisely in line where it returns a model By RCF we have RU S where Ko each variable x by the term f 8 with 6 a propositional formula that is satisfied only by v By Prob FAdd and Mon we have U 6 gt f 6 0 thus we can derive is the formula k where we replace E e gt Mweve J Bv 0 2 2 and FAdd and RCF we obtain that From F g 8v E Nveve f Bv 0 2 Naetig 6 O 2 3 Finally by CTaut we have F Naetiq s 4D e 2 4 So from 2 2 2 3 and 2 4 we obtain with tautological reasoning D me from which we conclude H ne This contradicts the consistency of e and thus the consistency of 6 For this reason there must be a model for e and consequently a model for 14 CHAPTER 2 STATE LOGIC EPPL Chapter 3 Verifying Digital Circuits with EPPL In this sec
65. tion we discuss a model checker for EPPL with applications to simple unreliable digital circuits Its actual implementation in the C programming lan guage is presented in the appendix To model unreliable digital circuits we devise and propose the concept of probabilistic Boolean circuits PBC A PBC is able to model any digital circuit with faulty logical gates that is gates that are prone to an error with a certain known probability which is reasonable since actual hardware components explicitly state their reliability We will show how EPPL can be used to achieve this goal 3 1 Notation and conventions At this point it is convenient to make a disambiguation for the rest of this chap ter the word Model capitalized will be used to denote EPPL models whereas the word model not capitalized will be used without this connotation It has already been seen that each w Q induces a valuation v over A In this chapter this association will be injective which amounts to saying that the sample space Q is finite and for each valuation v 2 there is at most one wy 2 This is a reasonable assumption because one only works with variables of the stochastic process X or continuous functions of these variables and is therefore unable to distinguish between different elements of that induce the same valuation Fur thermore as already observed in Remark 2 2 1 given any Model there is always a Model over valuations that sat
66. tion of the labeling formula by the valuation yields the same value as the denotation of the induced variable by the valuation and return the real number labeling the vertex or its complement according to the result The product of all such values will be the desired probability 3 4 THE BASIC ALGORITHM 21 3 4 The basic algorithm We now describe the basic algorithm for model checking EPPL formulas in EPPL models induced by SPBCs Let 6 be an EPPL global formula In the following algorithm the arrays bfg 0 Ar An subs 9 ma Ms pst d t1 tr 98f 0 61 du df de note respectively the list of subformulas of of the form O the list of measure subterms of of the form f 8 the list of probabilistic subterms of that are not measure terms the ordered tuple of basic subformulas of The symbol w represents the i th valuation in 2 for some enumeration of y valuations over A B w represents the algorithm that computes the denotation of 9 by wt which is well known to take O 8 time fact w represents the algorithm that computes P X wi Xp wi As we can see from Theorem 3 3 3 this algorithm takes O fact time where fact is the size of the factorization induced by the PBC Observe that O fact O n 8 with 8 being the length of the largest labeling formula of the PBC and n the num ber of propositional connectives in A One should kee
67. to formulate properties they may or may not satisfy Furthermore the development of model checking tools for formulas in such languages over structures generated by the systems is clearly beneficial when study ing the satisfaction of said properties In 11 14 and 15 one such logic PCTL and the respective model checking tool PRISM are proposed These are now widely accepted and used in several applications PCTL however only allows for probabilistic reasoning over transitions and in many cases the probabilistic reason ing must be considered over states EPPL 17 and it s temporal extension EpCTL 20 on the other hand are logics that allow for quantitative probabilistic reasoning about states and we will consider them in this thesis The main focus of this work is to detail the development and implementation of a Model Checker for EPPL over digital circuits Traditional digital circuits model checking tools assume that each logical gate in a circuit is completely reliable deter ministically providing an output for a given input This is an increasingly unrealistic assumption as hardware circuits become more and more miniaturized they also be come more sensitive to noise from outside sources either macrophysical or in more recent years microphysical Due to it s stochastic nature EPPL proves ideal to model these circuits Besides the model checking algorithm itself we present several relevant results concerning both the
68. w PBC specification 2 Model check an EPPL formula over the loaded PBC 3 Get the probability of a basic formula in the loaded PBC 4 Quit Figure 1 EPPL MC tool environment The current version of the MC allows you do do three operations to load a new SPBC to model check a global formula over the EPPL model generated by the loaded SPBC or to check the probability of a basic propositional formula over the EPPL model generated by the loaded SPBC SPBCs and EPPL formulas are syntaticaly complex and it is very easy to make a mistake when writing them For this reason the program reads it s input from previously created files This way if you make a mistake you won t need to rewrite the whole thing again A few notes on variable naming One important thing you have to remember when writing formulas and SPBCS is all variables and term variables must end with a whitespace This is a convention very easily overlooked so please pay close attention to it Variable names cannot include the symbols whitespaces other than the end ing one or start with a 0 or a 1 So var8 is an acceptable name but neither var 8 nor var8 are Avoid assigning your variables exotic names and everything will run smoothly The syntax of formulas and SPBCs is thoroughly explained in the main reference Computational representation of data structures Even well designed algorithms can be severely hampered by a bad choice
69. wise SPBCs play a central role of this work because each SPBC generates an EPPL Model where the stochastic process X is composed of random variables induced by the vertices their labeling functions and their labeling real numbers Essentially P Xp z1 Xp Tn represents the probability of vertices taking the config uration x1 Zn Furthermore as will be shown these Models can be efficiently stored and checked We will frequently refer to vertex i of a PBC by it s induced random variable X Example 3 2 2 Recall the EPPL model introduced by Example 2 2 2 It is simple to see that the SPBC presented in Figure 3 2 induces this model Observe that all the relevant information is much more efficiently encoded in the PBCS than it would be if we explicitly wrote out the probability function 18 CHAPTER 3 VERIFYING DIGITAL CIRCUITS WITH EPPL Figure 3 2 SPBC for double coin tossing example 3 3 Factorizations and Bayesian networks In general an EPPL Model representation requires an exponential space in A which we will denote throughout this section by n unless stated otherwise This is due to the existence of Models where each pair of propositional symbols are de pendent for such Models even the most efficient representation would have a worst case scenario that would require writing out explicitly all of the values corresponding to the probability attributed to each valuation occupying O 2 space Fortunat
70. work we present the implementation of an efficient model checking tool for formulas of a formal probabilistic logic EPPL over non reliable digital circuits In order to increase efficiency we capitalize on several specific properties of these structures however the tool remains very open ended allowing for adaptation to other more complex models A method to minimize space problems on model checkers over a subset of prob abilistic systems representable by Bayesian networks is also introduced For this we consider factorizations of stochastic processes associated with the probability spaces generated by the systems Implications of considering a temporal extension to the logic are discussed a model checking procedure is proposed for the temporal case and implementation options are presented Keywords Probabilistic systems model checking digital circuits temporal logic probabilistic logic vi Acknowledgments I would like to express my sincerest thanks to all people that through their support made this thesis possible Above all else I must thank my family for supporting me in all senses of the word for shaping me as I am today and for possessing an apparently unending pool of affection and patience towards me I would also like to thank my advisor Professor Paulo Mateus for his extraor dinary and contagious enthusiasm and of course for all his technical advise and time A word of thanks should also go to Ped
71. x and Q5 X 5 1 C Q Observe that k lt 6 Then we can build a system of k 1 equations Len Ty p Xg 1 Lwen Ty p Xp 1 wen To 1 for which we know that there is a non negative solution x p w for all w N From linear programming it is well known that if a system of k 1 linear equations has a non negative solution then there is a solution p for the system with at most k 1 variables taking positive values 4 Then we can construct a model m such that Q w O p zx gt 0 and p w p x Observe that 2 4 DECISION ALGORITHM FOR EPPL SATISFACTION 9 m le t4 lt te iff m IF t t2 for each inequation t lt t2 occurring in However it might be the case that m lr O6 and m If O8 for some subformula B of 6 since O C Q Then for each subformula 18 of 6 such that m If O68 and m I OP there exists wg OQ such that vws If 8 We can now construct the model m where Q Q U wg Q NQ m OS and m lr OB 7 p w fuen p w 0 otherwise and Xy w X w for all w Q Clearly Q lt 2 6 1 and m I 6 Finally from the first order theory of real ordered fields if there is a model using real numbers for a real closed formula then there is a model using only algebraic real numbers 1 since the l
72. xt state along that path AF holds if for all paths starting at s there exists a state in those paths where 6 holds E U 5 if there exists a path leaving s such 35 36 CHAPTER 4 TOWARDS EPCTL that there is a state s along that path where 62 holds and 6 holds in all states between s and s excluding s The other temporal connectives combinations and the temporal symbol G for always in the future are introduced as usual e AXd EX e EFS El 1L U6 e AG EF 5 e EG AF e Ald Ud E d2 U d1 N 2 N EG 62 4 2 Semantics A probabilistic Kripke structure is a tuple M S R D where S is a set of states RC S x S is a total transition relation called the accessibility relation and L is a map from to the set of EPPL models A reader familiar with CTL should notice the similarities between the semantics of both logics The satisfaction relation is defined by structural induction e M sl DB iff L s I C1 e M sl ty lt ta iff L s IH ty lt to e M sl 6 iff M s Ud e M s t 6 gt 5g iff M s If or M s IF e M sl EXO iff M s I 6 with s s R M s I AF iff for all path 7 over R starting in s there exists k N such that M mk LIE M s IH E 6 U62 iff there exists a path 7 over R starting in s and k N such that M mk IH do and M mi l dy for every i lt k Example 4 2 1 Consider the

here - Departamento de Matemática

Contents

Download Pdf Manuals

Related Search

Related Contents

here - Departamento de Matem&aacute;tica

Contents

Download Pdf Manuals

Related Search

Related Contents

here - Departamento de Matemática