{"header":{"message":"WIP","description":null,"timestamp":"2023-06-20T10:50:06.410403997Z","authors":[{}]},"hash":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC","authors":[{"login":"paradyx","key":"6haf2odGMeVaBH1hYPXKBZAYaktbbMcbxkvUdyZKMhVc"}],"deps":{"hashes":[["KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC","WIP"],["AA",null],["QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC","WIP"],["RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC","More stochastic"],["BGMT6NIKIDEGQ74DC4LPVBR7JCUYHHQBOZXHYXMO5F2UVEQ3N47QC","WIP"],["QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC","WIP"],["6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC","WIP"],["KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","WIP"],["EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","WIP"],["B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","WIP"],["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","Initial"],["UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC","WIP"],["MQJMCLGFSBSFJ3JPCIHQSBZS4XZPGJI7NGGRASX5UVGJO6HES25AC","More background, better acronyms"],["JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC","WIP"],["DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC","some more theory"],["X7SPUV4CXRX7D5KKL6UVGHC7JWRWCA4QAJVVQISE64UEU7GXJNRQC","WIP"]],"deps":["QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC"],"known":["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC","JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC","QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC","BGMT6NIKIDEGQ74DC4LPVBR7JCUYHHQBOZXHYXMO5F2UVEQ3N47QC","MQJMCLGFSBSFJ3JPCIHQSBZS4XZPGJI7NGGRASX5UVGJO6HES25AC","DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC","RVA3DOCNBWFBWA2MLC2TVQOEY25AUCYGEJSWMD72QRQ26AFLVZUAC","6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC"]},"hunks":[{"Edit":{"inode":{"change":3,"pos":6845},"path":"main.tex","line":37,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":206}],"down_context":[{"change":16,"pos":223}],"flag":"BLOCK","start":0,"end":23,"inode":{"change":3,"pos":6845}}},"contents":[{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:0"}},{"Add":{"text":"\\usepackage{cleveref}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22"}}]}},{"Edit":{"inode":{"change":3,"pos":6845},"path":"main.tex","line":57,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":6974}],"down_context":[{"change":16,"pos":379}],"flag":"BLOCK","start":24,"end":70,"inode":{"change":3,"pos":6845}}},"contents":[{"Add":{"text":"% algorithms","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:36"}},{"Add":{"text":"\\usepackage[ruled]{algorithm2e}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:68"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:69"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":2,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":7972}],"down_context":[{"change":3,"pos":7972}],"flag":"BLOCK","start":71,"end":1787,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:71"}},{"Add":{"text":"\\gls{koat}s analysis goal is to find tight upper bounds for \\gls{pip} and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:145"}},{"Add":{"text":"possibly non-probabilistic and non-deterministic integer programs that are a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:222"}},{"Add":{"text":"specialization of the first. The analysis techniques used such as","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:288"}},{"Add":{"text":"\\gls{mprf},\\todo{more} have their limits and cannot always find tight bounds for","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:369"}},{"Add":{"text":"every program, which motivates control-flow refinement in order to find an","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:444"}},{"Add":{"text":"equivalent program to the original one, that opens the possibility for the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:519"}},{"Add":{"text":"analysis to to find tighter bounds. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:556"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:557"}},{"Add":{"text":"Recall \\ref{def:overallcomplexity}; the newly constructed refined program shall","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:637"}},{"Add":{"text":"have they have the same overall runtime complexity as the original program,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:713"}},{"Add":{"text":"which implies that complexity bounds found for the refined program are also","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:789"}},{"Add":{"text":"complexity bounds for the original one. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:830"}},{"Add":{"text":"Naturally the control-flow refinement will add and replace transitions and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:905"}},{"Add":{"text":"locations, hence the runtime and size complexity per each transition won't be","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:983"}},{"Add":{"text":"preserved. However we will show, that each transition in the refined program is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1063"}},{"Add":{"text":"a copy of a transition in the original program, and that complexity of an","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1137"}},{"Add":{"text":"original transition is equal to the sum of its copies.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1192"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1193"}},{"Add":{"text":"The control-flow refinement presented in this thesis adapts the partial","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1265"}},{"Add":{"text":"evaluation presented by \\citeauthor{domenech2019arxiv}\\cite{domenech2019arxiv}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1344"}},{"Add":{"text":"for \\acrlong{pip}. The partial evaluation will be constructed in a similar","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1419"}},{"Add":{"text":"way but explicitly taking probability and general transitions into account. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1496"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1497"}},{"Add":{"text":"The construction is done in three steps. First the single evaluation step","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1571"}},{"Add":{"text":"(unfolding) of transitions in a probabilistic program is presented. Second, a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1649"}},{"Add":{"text":"possibly infinite evaluation tree is constructed that will finally be collapsed","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1729"}},{"Add":{"text":"into a finite evaluation graph by an abstraction layer. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1786"}}]}},{"Replacement":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":31,"ins":{"up_context":[{"change":3,"pos":7973}],"down_context":[{"change":2,"pos":10499}],"flag":"BLOCK","start":1788,"end":2053,"inode":{"change":3,"pos":7949}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7973},"to":{"change":2,"start":10202,"end":10499},"introduced_by":2}],"inode":{"change":3,"pos":7949}},"ins_contents":[{"Add":{"text":"Afterwards we will show that the partial evaluation is sound for probabilistic","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1866"}},{"Add":{"text":"integer programs and prove that the overall expected runtime complexity","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:1938"}},{"Add":{"text":"(\\cref{def:past}) is equally preserved as the overall (worst-case) runtime","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2013"}},{"Add":{"text":"complexity (\\cref{def:runtimebounds}).","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2052"}}],"del_contents":[{"Del":{"text":"\\section{Program equivalence}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10231"}},{"Del":{"text":"\\begin{definition}[Program equivalence]","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10271"}},{"Del":{"text":" Given two PIP $P = (\\V, L, \\GT, l_0)$ and $P' = (\\V, L', \\GT', l_0)$","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10344"}},{"Del":{"text":" are equivalent if and only if the following properties hold:","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10409"}},{"Del":{"text":" \\begin{enumerate}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10431"}},{"Del":{"text":" \\item \\todo{continue}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10461"}},{"Del":{"text":" \\end{enumerate}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10481"}},{"Del":{"text":"\\end{definition}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:10498"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":37,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":783}],"down_context":[{"change":3,"pos":0}],"flag":"BLOCK","start":2054,"end":2055,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2054"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":49,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":758},"to":{"change":3,"start":758,"end":759},"introduced_by":3}],"inode":{"change":3,"pos":7949}}},"contents":[{"Del":{"text":"","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:758"}}]}},{"Replacement":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":52,"ins":{"up_context":[{"change":3,"pos":992}],"down_context":[{"change":3,"pos":1532}],"flag":"BLOCK","start":2056,"end":2333,"inode":{"change":3,"pos":7949}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":992},"to":{"change":3,"start":992,"end":1532},"introduced_by":3}],"inode":{"change":3,"pos":7949}},"ins_contents":[{"Add":{"text":"described by a set of constraints. The resulting graph is called a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2122"}},{"Add":{"text":"\\textit{partial evaluation graph}. It was formalized for \\gls{chc} by","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2192"}},{"Add":{"text":"\\citeauthor{gallagher2019eptcs}. In this thesis the definitions are adapted to","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2271"}},{"Add":{"text":"better fit the algorithm and the formalisms of \\Glspl{pip}. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2332"}}],"del_contents":[{"Del":{"text":"described by a set of constraints (polyhedron).","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1039"}},{"Del":{"text":"This approach is very similar to the computation of invariants, where the set of","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1120"}},{"Del":{"text":"possible assignment each location in a given program is iteratively updated by","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1199"}},{"Del":{"text":"propagating the transition constraints throught the program until a fixpoint is","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1279"}},{"Del":{"text":"found. \\todo{citation} However, during evaluation one starts at a specific","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1354"}},{"Del":{"text":"configuration and \\textit{unfolds} transitions recursively, without influency","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1432"}},{"Del":{"text":"neighboring paths. The result is a (possibly still infinite) tree, representing","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1512"}},{"Del":{"text":"all possible runs.","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1531"}}]}},{"Replacement":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":57,"ins":{"up_context":[{"change":3,"pos":1533}],"down_context":[{"change":3,"pos":1792}],"flag":"BLOCK","start":2334,"end":3923,"inode":{"change":3,"pos":7949}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1533},"to":{"change":3,"start":1533,"end":1614},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1614},"to":{"change":3,"start":22,"end":102},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":102},"to":{"change":3,"start":1694,"end":1792},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1694},"to":{"change":3,"start":1694,"end":1792},"introduced_by":3}],"inode":{"change":3,"pos":7949}},"ins_contents":[{"Add":{"text":"Given \\gls{pip} $P$ with locations $L$, transitions $T$ and general transitions","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2413"}},{"Add":{"text":"$G$. Versions are the vertices of the partial evaluation graph. They contain the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2494"}},{"Add":{"text":"location at each step of the evaluation and a representation of the possible","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2571"}},{"Add":{"text":"assignments at each step of the evaluation. Versions can contain just","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2641"}},{"Add":{"text":"constraints, but in order to guarantee a finite graph later on, they can also","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2719"}},{"Add":{"text":"contain an value from an abstraction space (see \\Sref{sec:abstraction_layer},","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2797"}},{"Add":{"text":"not to be confused with the abstract domains).","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2844"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2845"}},{"Add":{"text":"\\begin{definition}[Version]\\label{def:version}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2892"}},{"Add":{"text":" The set of \\textit{constraint versions} is the set of tuples over the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:2966"}},{"Add":{"text":" locations $L$ from $P$ and constraints $\\C$. The set of \\textit{abstract","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3043"}},{"Add":{"text":" versions} is the set of tuples over the locations $L$ from $P$ and some","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3119"}},{"Add":{"text":" finite abstraction space $A$. Since the set of locations and the abstraction","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3200"}},{"Add":{"text":" space are both finite, so are the abstract versions. The set of versions is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3280"}},{"Add":{"text":" the union of constraint and abstract versions. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3332"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3333"}},{"Add":{"text":" \\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3354"}},{"Add":{"text":" \\vers = (\\Loc \\times \\C) \\union (\\Loc \\times A)","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3410"}},{"Add":{"text":" \\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3429"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3430"}},{"Add":{"text":" For clarity sake, versions will be denoted with angles. The set notation","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3507"}},{"Add":{"text":" with curly braces is used for non-abstracted constraints like so $\\langle l,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3588"}},{"Add":{"text":" \\{\\psi_1, \\dots\\}\\rangle$ and the list notation with brackets is used for","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3666"}},{"Add":{"text":" abstracted values like so $\\langle l, [\\psi_1, \\dots]\\rangle$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3733"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3750"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3751"}},{"Add":{"text":"The edges of the partial evaluation graph are transitions $\\T_{PE}$ analogously","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3831"}},{"Add":{"text":"defined to Definition \\ref{def:pip}, except that they connect versions and not","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3910"}},{"Add":{"text":"locations. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3922"}}],"del_contents":[{"Del":{"text":"This tree was formalized as an evaluation tree for \\gls{chc} by \\todo{citation}.","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1613"}},{"Del":{"text":"In this thesis the evaluation tree is defined for \\Gls{pip} instead, giving the","pos":"BGMT6NIKIDEGQ74DC4LPVBR7JCUYHHQBOZXHYXMO5F2UVEQ3N47QC:101"}},{"Del":{"text":"opportunity to explicitly handle costs, and probability and staying closer to","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1771"}},{"Del":{"text":"KoAT's formalisms. ","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1791"}}]}},{"Replacement":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":87,"ins":{"up_context":[{"change":3,"pos":1793}],"down_context":[{"change":3,"pos":1829}],"flag":"BLOCK","start":3924,"end":6784,"inode":{"change":3,"pos":7949}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1793},"to":{"change":3,"start":1793,"end":1829},"introduced_by":3}],"inode":{"change":3,"pos":7949}},"ins_contents":[{"Add":{"text":"\\begin{definition}[Partial Evaluation]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:3962"}},{"Add":{"text":" A graph $G = (\\vers, \\T_{PE})$ is a \\textit{partial evaluation} of a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4035"}},{"Add":{"text":" \\gls{pip} $P$ when for every admissible path $c_0c_1\\dots{}c_n \\in \\fpath$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4114"}},{"Add":{"text":" of P with $c_i = (l_i, s_i, t_i)$ and $t_i = (l_{i-1}, \\tau_i, \\eta_i, p_i,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4194"}},{"Add":{"text":" l_i)$ for all $i = 1, \\dots, n$, there exists a path $v_0'v_1'\\dots{}v_n'$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4273"}},{"Add":{"text":" in G with the following properties:","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4313"}},{"Add":{"text":" \\begin{enumerate}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4335"}},{"Add":{"text":" \\item $v'_i = (\\langle l_i, \\varphi_i\\rangle, t_i')$ with some $\\varphi_i","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4417"}},{"Add":{"text":" \\in \\C$ and $t_i' \\in E(G)$,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4458"}},{"Add":{"text":" \\item $t'_i = (\\langle l_{i-i}, \\varphi_{i-1}\\rangle, p_i, \\tau_i, \\eta_i, ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4542"}},{"Add":{"text":" \\langle l_i, \\varphi_i\\rangle)$, and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4591"}},{"Add":{"text":" \\item $s_i \\models \\varphi_i$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4629"}},{"Add":{"text":" \\end{enumerate}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4649"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4666"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4667"}},{"Add":{"text":"A \\Gls{pip} $P$ can be lifted to a trivial partial evaluation graph by replacing","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4748"}},{"Add":{"text":"every location $l \\in L$ by the trivial version $\\langle l,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4808"}},{"Add":{"text":"\\textit{true}\\rangle$. Obviously the lift of program is not useful for the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4883"}},{"Add":{"text":"analysis, as it doesn't capture any interesting properties of the program,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:4958"}},{"Add":{"text":"besides what is already known in the original program. In the following we will","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5038"}},{"Add":{"text":"present a construction for a partial evaluation graph using unfolding and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5112"}},{"Add":{"text":"abstraction.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5125"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5126"}},{"Add":{"text":"The partial evaluation is done step-wise. On every step the next version","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5199"}},{"Add":{"text":"$v' = \\langle l', \\phi'\\rangle$ is computed by unfolding a transition $t \\in \\T$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5280"}},{"Add":{"text":"from the original \\gls{pip} that starts in the same location $l \\in \\L$ as the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5359"}},{"Add":{"text":"version $v = \\langle l, \\phi\\rangle$. The resulting constraint $\\phi'$ contains","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5439"}},{"Add":{"text":"all states $s' \\in \\Sigma$ with $s' \\models \\phi'$ reachable via the transition","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5519"}},{"Add":{"text":"from a state in the source version, i.e. $\\prSs((l, s, \\_) \\rightarrow (l',s',t))","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5601"}},{"Add":{"text":"> 0$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5608"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5609"}},{"Add":{"text":"The non-determinism is taken into account by the implicit existential","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5679"}},{"Add":{"text":"quantification of temporary variables in constraints. In contrast, the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5750"}},{"Add":{"text":"probabilistic sampling is over-approximated with an non-probabilistic update","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5827"}},{"Add":{"text":"$\\tilde{\\eta}: \\PV \\rightarrow Z[\\V]$ and a constraint denoted as","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5893"}},{"Add":{"text":"$\\lfloor\\eta\\rceil$. The probabilistic distributions in the probabilistic update","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:5974"}},{"Add":{"text":"$\\eta$ are replaced by fresh temporary variables that are then constraint by","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6051"}},{"Add":{"text":"$\\lfloor\\eta\\rceil$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6072"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6073"}},{"Add":{"text":"\\begin{definition}[Non-probabilistic overapproximation\\label{def:nonprobapprox}]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6154"}},{"Add":{"text":" Let $\\eta: \\PV \\rightarrow \\Z[\\V\\union D]$ be a probabilistic update","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6227"}},{"Add":{"text":" function, with random distributions $D_1,\\dots,D_n$ used within. A","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6299"}},{"Add":{"text":" \\textit{non-probabilistic over-approximation} is a pair $(\\lfloor\\eta\\rceil,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6380"}},{"Add":{"text":" \\tilde{\\eta}) \\in \\C \\times (\\PV \\rightarrow \\Z[\\V])$ where ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6445"}},{"Add":{"text":" \\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6466"}},{"Add":{"text":" \\lfloor\\eta\\rceil = \\LAnd_{x\\in\\PV} (x' = \\eta(x)[D_i\\backslash{}d_i])","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6545"}},{"Add":{"text":" \\land \\LAnd_{i=1,\\dots,n} \\lfloor D_i \\rceil \\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6601"}},{"Add":{"text":" \\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6620"}},{"Add":{"text":" \\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6641"}},{"Add":{"text":" \\tilde{\\eta}(x) = x' \\hspace{1cm} \\text{for all } x\\in\\PV","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6707"}},{"Add":{"text":" \\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6726"}},{"Add":{"text":" for some fresh temporary variables $x', d_i\\in \\TV$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6783"}}],"del_contents":[{"Del":{"text":"\\begin{definition}[Evaluation Tree]","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:1828"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":140,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":1846}],"down_context":[{"change":3,"pos":1846}],"flag":"BLOCK","start":6785,"end":9461,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6785"}},{"Add":{"text":"\\begin{lemma}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6799"}},{"Add":{"text":" For any assignment $s\\in\\Sigma$, non-probabilistic update $\\eta: \\PV","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6872"}},{"Add":{"text":" \\rightarrow \\Z[\\V \\union D]$, and values $k_i \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:6926"}},{"Add":{"text":" \\text{supp}([\\eta(x_i)](s))$, the assignment $s'(x_i)=k_i$ satisfies the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7003"}},{"Add":{"text":" non-probabilistic over-approximation \\todo{todo}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7056"}},{"Add":{"text":"\\end{lemma}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7068"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7069"}},{"Add":{"text":"\\begin{definition}[Unfolding constraints]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7111"}},{"Add":{"text":" Let $\\varphi \\in \\C$ be a constraint and $t = (\\_, \\tau, \\eta, \\_, \\_) \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7190"}},{"Add":{"text":" \\T$. An unfolding of $\\varphi$ via $t$ is defined as follows.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7256"}},{"Add":{"text":" \\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7274"}},{"Add":{"text":" \\unfold(\\varphi, t) = \\begin{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7318"}},{"Add":{"text":" \\eta(\\varphi \\Land \\tau \\Land \\lfloor\\eta\\rceil)|_{\\PV} & \\text{if }","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7399"}},{"Add":{"text":" \\tilde{\\eta}(\\varphi \\Land \\tau \\Land \\lfloor\\eta\\rceil) \\text{ is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7478"}},{"Add":{"text":" SAT}\\\\ ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7498"}},{"Add":{"text":" \\textit{false} & \\text{otherwise}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7544"}},{"Add":{"text":" \\end{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7564"}},{"Add":{"text":" \\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7580"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7597"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7598"}},{"Add":{"text":"The exactness is relaxed in order to work with abstract domains. Instead, the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7676"}},{"Add":{"text":"result of unfolding an abstract value equivalent to $c$ shall contain all values","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7757"}},{"Add":{"text":"of the constraint unfolding but possibly more. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7805"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7806"}},{"Add":{"text":"Given an unfolding one can derive an unfolding operation $\\unfold^*: \\C \\times","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7885"}},{"Add":{"text":"\\T \\rightarrow 2^{\\T_{PE}}$ that constructs a new transition between the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:7958"}},{"Add":{"text":"versions copying the guard $\\tau$, update $\\eta$, and probability $p$ from the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8037"}},{"Add":{"text":"original transition. Since unsatisfiable versions cannot be reached they are","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8114"}},{"Add":{"text":"ignored and no transition is created. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8154"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8155"}},{"Add":{"text":"\\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8169"}},{"Add":{"text":" \\unfold^*(\\varphi, (l, \\tau, \\eta, p, l')) = \\begin{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8232"}},{"Add":{"text":" \\{(\\langle l, \\varphi\\rangle, \\tau, \\eta, p, \\langle l',","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8297"}},{"Add":{"text":" \\unfold(\\varphi, t)\\rangle \\} & \\unfold(\\varphi, t) \\text{ if is SAT} \\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8378"}},{"Add":{"text":" \\{\\} & \\text{ otherwise}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8411"}},{"Add":{"text":" \\end{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8427"}},{"Add":{"text":"\\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8439"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8440"}},{"Add":{"text":"The operation is overloaded with a set function $\\unfold_P^*: \\C \\times \\GT","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8516"}},{"Add":{"text":"\\rightarrow 2^{\\T_{PE}}$ unfolding all transitions in a general transition.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8592"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8593"}},{"Add":{"text":"\\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8607"}},{"Add":{"text":" \\unfold^*(\\varphi, g) = \\Union_{t \\in g}\\unfold^*(\\varphi, t)","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8673"}},{"Add":{"text":"\\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8685"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8686"}},{"Add":{"text":"Again the operation is overloaded with a function $\\unfold^* : \\vers \\rightarrow","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8767"}},{"Add":{"text":"2^{\\T_{PE}}$ unfolding all outgoing general transitions in the \\gls{pip} $P$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8845"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8846"}},{"Add":{"text":"\\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8860"}},{"Add":{"text":" \\unfold^*(\\langle l, \\varphi\\rangle) = \\Union_{g \\in \\GT_{out}(l)} \\unfold^*(\\varphi, t)","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8953"}},{"Add":{"text":"\\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8965"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8966"}},{"Add":{"text":"\\begin{example}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8982"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8983"}},{"Add":{"text":"\\end{example}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8997"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:8998"}},{"Add":{"text":"\\begin{algorithm}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9016"}},{"Add":{"text":" \\caption{$evaluate(P, G, v)$}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9050"}},{"Add":{"text":" \\KwData{","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9063"}},{"Add":{"text":" A PIP $P$, Graph $G$, and source version $\\langle l, \\varphi\\rangle$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9140"}},{"Add":{"text":" }","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9146"}},{"Add":{"text":" \\KwResult{A Graph $G$}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9173"}},{"Add":{"text":" $N = \\unfold^*(v)$\\;","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9198"}},{"Add":{"text":" \\For{$t = (v, \\tau, \\eta, p, v') \\in N $}{","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9245"}},{"Add":{"text":" \\If {$v' \\not\\in G$}{","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9275"}},{"Add":{"text":" $G := G \\union \\{t\\}$\\;","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9311"}},{"Add":{"text":" $G := evaluate(P, G, v')$\\;","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9351"}},{"Add":{"text":" }","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9361"}},{"Add":{"text":" \\Else {","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9377"}},{"Add":{"text":" $G = G \\union \\{t\\}$\\;","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9412"}},{"Add":{"text":" }","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9422"}},{"Add":{"text":" }","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9428"}},{"Add":{"text":" \\Return {G}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9444"}},{"Add":{"text":"\\end{algorithm}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9460"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":452,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":1784}],"down_context":[{"change":3,"pos":9652}],"flag":"BLOCK","start":9462,"end":9493,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9462"}},{"Add":{"text":"\\section{Choosing properties}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9492"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":455,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":9653}],"down_context":[{"change":3,"pos":1784}],"flag":"BLOCK","start":9494,"end":9516,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"\\section{Correctness}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9515"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":467,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":10289}],"down_context":[{"change":3,"pos":1821}],"flag":"BLOCK","start":9517,"end":11376,"inode":{"change":3,"pos":7949}}},"contents":[{"Add":{"text":"\\section{Partial evaluation of \\gls{scc}s}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9559"}},{"Add":{"text":"During \\gls{koat}s analysis the program is split into \\glspl{scc}. Bounds are","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9637"}},{"Add":{"text":"found for every \\gls{scc} separately and then composed into an overall bound at","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9717"}},{"Add":{"text":"the end. Control-flow refinement is only needed for those \\glspl{scc} where the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9797"}},{"Add":{"text":"analysis fails to find tight bounds. In practice, linear bounds are considered","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9876"}},{"Add":{"text":"tight enough, whereas polynomial and exponential complexity bounds warrant","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9951"}},{"Add":{"text":"refinement in hope for tighter bounds.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9990"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:9991"}},{"Add":{"text":"The previously presented control-flow refinement starts at the start locations","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10070"}},{"Add":{"text":"and evaluates the whole program. The size of the refined program is limited by","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10149"}},{"Add":{"text":"the number of locations and transitions as well as the number of properties on","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10228"}},{"Add":{"text":"each abstracted location. The smaller the initial program, the faster the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10302"}},{"Add":{"text":"control-flow, the refined program and subsequent analysis. Instead of evaluating","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10383"}},{"Add":{"text":"the program, one can adapt the partial evaluate to only evaluate a single","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10457"}},{"Add":{"text":"\\gls{scc} of the program. This section presents the partial evaluation of an","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10534"}},{"Add":{"text":"\\gls{scc}.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10545"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10546"}},{"Add":{"text":"The result is again an entire program, where only transitions the \\gls{scc}, and ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10628"}},{"Add":{"text":"incoming and outgoing transitions to this \\gls{scc} are changed. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10694"}},{"Add":{"text":"In a first step the program is copied as a whole, lifted to a trivial evaluation","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10775"}},{"Add":{"text":"graph and the \\gls{scc}, and all incoming and outgoing transitions are removed","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10854"}},{"Add":{"text":"from the copy. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10870"}},{"Add":{"text":"Then the evaluation algorithm is executed from every incoming transition, but","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:10948"}},{"Add":{"text":"with the additional condition to backtrack after unfolding an exiting","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11018"}},{"Add":{"text":"transition. The new transitions are added into the copied evaluation graph and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11097"}},{"Add":{"text":"therefore progress made by earlier evaluations of entry transitions can be","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11172"}},{"Add":{"text":"reused, shortening the evaluation of succeeding incoming transitions. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11243"}},{"Add":{"text":"Finally, the evaluation graph is converted back to a \\gls{pip} and returned as","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11322"}},{"Add":{"text":"result of the partial evaluation of the \\gls{scc}.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11373"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11374"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11375"}}]}},{"Edit":{"inode":{"change":3,"pos":7949},"path":"ch3_theory.tex","line":503,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2003},"to":{"change":3,"start":2003,"end":2033},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":2033},"to":{"change":3,"start":5098,"end":5099},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":5098},"to":{"change":3,"start":5098,"end":5099},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":5099},"to":{"change":3,"start":7998,"end":8020},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7998},"to":{"change":3,"start":7998,"end":8020},"introduced_by":3}],"inode":{"change":3,"pos":7949}}},"contents":[{"Del":{"text":"\\section{Choosing properties}","pos":"DDNESFMD4LGNTDGTCW27FQPCOR5Y5MJWN2TWCSIRNBK6QGBITBRQC:2032"}},{"Del":{"text":"","pos":"QCVDPRXH57UFLU4YV3P2I5RQZGCBUKROYUZHDWOCHL43KDYN7MPAC:5098"}},{"Del":{"text":"\\section{Correctness}","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:8019"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":9,"ins":{"up_context":[{"change":3,"pos":174}],"down_context":[{"change":3,"pos":160}],"flag":"BLOCK","start":11377,"end":11487,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":174},"to":{"change":3,"start":233,"end":292},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\newcommand{\\Lin}{\\mathcal{LC}} % Set of linear constraints","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11436"}},{"Add":{"text":"\\newcommand{\\Loc}{\\mathcal{L}} % Set of locations","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11486"}}],"del_contents":[{"Del":{"text":"\\renewcommand{\\L}{\\mathcal{L}} % Set of linear constraints","pos":"UVN5HOW3H2OVESJ62UFNQNS6VXHI5TRV22HQ44EOYU42453SDD2QC:291"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":19,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":11351}],"down_context":[{"change":3,"pos":315}],"flag":"BLOCK","start":11488,"end":12091,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\RB}[0]{\\mathcal{RB}} % Runtime bound","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11537"}},{"Add":{"text":"\\newcommand{\\SB}[0]{\\mathcal{SB}} % Size bound","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11584"}},{"Add":{"text":"\\newcommand{\\B}[0]{\\mathcal{B}} %Bounds","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11624"}},{"Add":{"text":"\\newcommand{\\Rt}[0]{\\mathcal{R}} %Runtime","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11666"}},{"Add":{"text":"\\newcommand{\\E}[0]{\\mathbb{E}} % Expected ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11709"}},{"Add":{"text":"\\newcommand{\\scheduler}[0]{\\mathfrak{S}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11750"}},{"Add":{"text":"\\newcommand{\\ESs}[0]{\\mathbb{E}_{\\scheduler,s_0}} % Expected ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11812"}},{"Add":{"text":"\\newcommand{\\Prog}[0]{\\mathcal{P}} % A PIP","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11855"}},{"Add":{"text":"\\newcommand{\\GRV}[0]{\\mathcal{GRV}} % General result variables","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11918"}},{"Add":{"text":"\\renewcommand{\\S}[0]{\\mathcal{S}} % grv variable","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:11967"}},{"Add":{"text":"\\newcommand{\\RBe}[0]{\\mathcal{RB}_\\E} % Expected Runtime bound","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12030"}},{"Add":{"text":"\\newcommand{\\SBe}[0]{\\mathcal{SB}_\\E} % Expected Size bound","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12090"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":44,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":11493}],"down_context":[{"change":2,"pos":11493}],"flag":"BLOCK","start":12092,"end":12540,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\unfold}[0]{\\text{unfold}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12130"}},{"Add":{"text":"\\newcommand{\\vers}[0]{\\textbf{\\textsf{Version}}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12179"}},{"Add":{"text":"\\newcommand{\\pr}[0]{\\textit{pr}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12212"}},{"Add":{"text":"\\newcommand{\\prSs}[0]{\\textit{pr}_{\\scheduler, s_0}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12265"}},{"Add":{"text":"\\newcommand{\\PrSs}[0]{\\mathbb{P}_{\\scheduler, s_0}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12317"}},{"Add":{"text":"\\newcommand{\\G}[0]{\\mathcal{G}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12349"}},{"Add":{"text":"\\newcommand{\\Tin}[0]{\\T_\\text{in}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12384"}},{"Add":{"text":"\\newcommand{\\Tout}[0]{\\T_\\text{out}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12421"}},{"Add":{"text":"\\newcommand{\\GTin}[0]{{\\mathcal{G}\\mathcal{T}_\\text{in}}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12479"}},{"Add":{"text":"\\newcommand{\\GTout}[0]{{\\mathcal{G}\\mathcal{T}_\\text{out}}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12539"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":64,"ins":{"up_context":[{"change":3,"pos":10840}],"down_context":[{"change":3,"pos":10914}],"flag":"BLOCK","start":12541,"end":12617,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":10840},"to":{"change":3,"start":10840,"end":10914},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" non-strict inequality constraints} is defined as the set $\\Lin^{\\leq}$:","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12616"}}],"del_contents":[{"Del":{"text":" non-strict inequality constraints} is defined as the set $\\L^{\\leq}$:","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:10913"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":66,"ins":{"up_context":[{"change":3,"pos":10932}],"down_context":[{"change":3,"pos":11004}],"flag":"BLOCK","start":12618,"end":12692,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":10932},"to":{"change":3,"start":10932,"end":11004},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" \\Lin^{\\leq}=\\set{a_0 + \\sum_{i=1}^{n} a_i v_i \\leq 0}{a_i \\in \\R}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12691"}}],"del_contents":[{"Del":{"text":" \\L^{\\leq}=\\set{a_0 + \\sum_{i=1}^{n} a_i v_i \\leq 0}{a_i \\in \\R}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11003"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":69,"ins":{"up_context":[{"change":3,"pos":11097}],"down_context":[{"change":3,"pos":11130}],"flag":"BLOCK","start":12693,"end":12728,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11097},"to":{"change":3,"start":11097,"end":11130},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" defined as the set $\\Lin^{<}$:","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12727"}}],"del_contents":[{"Del":{"text":" defined as the set $\\L^{<}$:","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11129"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":71,"ins":{"up_context":[{"change":3,"pos":11148}],"down_context":[{"change":3,"pos":11215}],"flag":"BLOCK","start":12729,"end":12798,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11148},"to":{"change":3,"start":11148,"end":11215},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" \\Lin^{<}:=\\set{a_0 + \\sum_{i=1}^{n} a_i v_i < 0}{a_i \\in \\R}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12797"}}],"del_contents":[{"Del":{"text":" \\L^{<}:=\\set{a_0 + \\sum_{i=1}^{n} a_i v_i < 0}{a_i \\in \\R}","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11214"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":75,"ins":{"up_context":[{"change":3,"pos":11311}],"down_context":[{"change":3,"pos":956}],"flag":"BLOCK","start":12799,"end":12868,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11311},"to":{"change":2,"start":11739,"end":11802},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"linear constraints denoted as $\\Lin := \\Lin^{\\leq} \\union \\Lin^{<}$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12867"}}],"del_contents":[{"Del":{"text":"linear constraints denoted as $\\L := \\L^{\\leq} \\union \\L^{<}$.","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:11801"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":82,"ins":{"up_context":[{"change":2,"pos":11943}],"down_context":[{"change":2,"pos":12014}],"flag":"BLOCK","start":12869,"end":12942,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":11943},"to":{"change":2,"start":11943,"end":12014},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" <, =)$, a constraint $\\psi \\in \\Lin$ is \\textit{satisfiable} in when","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:12941"}}],"del_contents":[{"Del":{"text":" <, =)$, a constraint $\\psi \\in \\L$ is \\textit{satisfiable} in when","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:12013"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":88,"ins":{"up_context":[{"change":3,"pos":1087}],"down_context":[{"change":2,"pos":12177}],"flag":"BLOCK","start":12943,"end":13025,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1087},"to":{"change":3,"start":11833,"end":11913},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"A set of constraints $C \\subseteq \\Lin$ is satisfiable, when their conjunction is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13024"}}],"del_contents":[{"Del":{"text":"A set of constraints $C \\subseteq \\L$ is satisfiable, when their conjunction is","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:11912"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":312,"ins":{"up_context":[{"change":3,"pos":14477}],"down_context":[{"change":3,"pos":14632}],"flag":"BLOCK","start":13026,"end":13185,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":14477},"to":{"change":3,"start":14477,"end":14632},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"constraint $\\psi \\in \\Lin^{\\leq}$ describes an closed affine half-space and every","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13107"}},{"Add":{"text":"linear strict inequality constraint $\\psi \\in \\Lin^{\\leq}$ describes an open","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13184"}}],"del_contents":[{"Del":{"text":"constraint $\\psi \\in \\L^{\\leq}$ describes an closed affine half-space and every","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14556"}},{"Del":{"text":"linear strict inequality constraint $\\psi \\in \\L^{\\leq}$ describes an open","pos":"6PTHERE26NXSC3ZXSI5UYKWTMPYZD4WMYFBJKZE3MRRTKC7MIU6QC:14631"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":608,"ins":{"up_context":[{"change":2,"pos":22972}],"down_context":[{"change":2,"pos":23011}],"flag":"BLOCK","start":13186,"end":15368,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":22972},"to":{"change":2,"start":22972,"end":23011},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"$\\Z[\\V\\union D]$, is the set of integer polynomials containing variables $\\V$ or","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13266"}},{"Add":{"text":"distributions. They behave exactly like normal polynomials except that the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13341"}},{"Add":{"text":"values of the distributions are sampled probabilistically instead of being given","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13422"}},{"Add":{"text":"as argument. As such we can define a function $[\\cdot]: \\Z[\\V\\union D]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13493"}},{"Add":{"text":"\\rightarrow \\Sigma \\rightarrow \\Z \\rightarrow [0,1]$ that returns the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13563"}},{"Add":{"text":"probability that the polynomial $f \\in \\Z[\\V \\union D]$ with a state $s \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13639"}},{"Add":{"text":"\\Sigma$ evaluates to a value $k\\in\\Z$ with a probability $[f](s)(k)$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13710"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13711"}},{"Add":{"text":"The values of the variables are fixed by a syntactical substitution, where every","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13792"}},{"Add":{"text":"variable $x_i\\in\\V$ is replaced by the value fixed in the assignment $s(x_i)$,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13871"}},{"Add":{"text":"we write $[x_i\\backslash s(x_i)]$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13906"}},{"Add":{"text":"The resulting polynomial $f[x_i\\backslash s(x_i)]$ describes a random variable","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:13985"}},{"Add":{"text":"$[f](s)$ that takes a value at random depending only on the distributions $D_1,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14065"}},{"Add":{"text":"\\dots, D_m$ within. The random variable has the following probability","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14135"}},{"Add":{"text":"distribution: ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14150"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14151"}},{"Add":{"text":"\\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14165"}},{"Add":{"text":" [f](s)(k) &= \\sum_{\\substack{d_i \\in \\Z \\\\ i = 0,\\dots,m}} D_1(d_1)","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14237"}},{"Add":{"text":" \\cdot D_2(d_2) \\cdots D_m(d_m) \\cdot \\begin{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14292"}},{"Add":{"text":" 1, & \\text{if } f[x_i \\backslash s(x_i)][D_i\\backslash d_i] = k \\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14367"}},{"Add":{"text":" 0, & \\text{otherwise}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14397"}},{"Add":{"text":" \\end{cases}\\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14415"}},{"Add":{"text":" & = P([f](s) = k) ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14438"}},{"Add":{"text":"\\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14450"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14451"}},{"Add":{"text":"where $f[D_i\\backslash d_i]$ is a syntactical substitution of every distribution","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14532"}},{"Add":{"text":"$D_i$ by an integer value $d_i \\in \\Z$ for all $i = 1,\\dots,m$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14596"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14597"}},{"Add":{"text":"Under misuse of notation we write $f(s)$ to denote the unique value $v$ with","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14674"}},{"Add":{"text":"$f(s)(v) = 1$, when it exists. \\todo{check if actually used}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14735"}},{"Add":{"text":"The support of polynomial $f$ with an assignment $s$ is the set of values that","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14814"}},{"Add":{"text":"can be achieved with the polynomial by sampling the random distributions.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14888"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14889"}},{"Add":{"text":"\\begin{example}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14905"}},{"Add":{"text":" Consider the polynomial $f = x^2 + \\textsc{Unif}(3,5)$ and the assignment","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:14983"}},{"Add":{"text":" $s(x) = 2$. $[f](s)$ is the random variable described by the polynomial $f[x/2]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15067"}},{"Add":{"text":" =2^2 + \\textsc{Unif}(3,5)$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15099"}},{"Add":{"text":" It can take three different values with the following probability","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15169"}},{"Add":{"text":" \\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15190"}},{"Add":{"text":" [f](s)(k) = \\begin{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15224"}},{"Add":{"text":" \\frac{1}{3}, & \\text{if } k \\in \\{7,8,9\\}\\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15280"}},{"Add":{"text":" 0, & \\text{otherwise}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15314"}},{"Add":{"text":" \\end{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15334"}},{"Add":{"text":" \\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15353"}},{"Add":{"text":"\\end{example}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15367"}}],"del_contents":[{"Del":{"text":"\\todo{define support, and constraints}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:23010"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":788,"ins":{"up_context":[{"change":2,"pos":29542}],"down_context":[{"change":3,"pos":11429}],"flag":"BLOCK","start":15369,"end":15535,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":29542},"to":{"change":2,"start":29542,"end":29607},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":29607},"to":{"change":3,"start":38151,"end":38228},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11137},"to":{"change":3,"start":38151,"end":38228},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\begin{definition}[Probabilistic Integer Program\\cite{meyer2021tacas}]\\label{def:pip}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15454"}},{"Add":{"text":" $(\\PV, \\Loc, \\GT, l_0)$ is a probabilistic integer transition system where ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15534"}}],"del_contents":[{"Del":{"text":"\\begin{definition}[Probabilistic Integer Program]\\label{def:pip}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:29606"}},{"Del":{"text":" $(\\PV, L, \\GT, l_0)$ is a probabilistic integer transition system where ","pos":"JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC:38227"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":792,"ins":{"up_context":[{"change":3,"pos":38286}],"down_context":[{"change":3,"pos":11563}],"flag":"BLOCK","start":15536,"end":15595,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":3,"pos":38286},"to":{"change":3,"start":11507,"end":11563},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11507},"to":{"change":3,"start":11507,"end":11563},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" \\item $\\Loc$ is a finite non-empty set of location","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15594"}}],"del_contents":[{"Del":{"text":" \\item $L$ is a finite non-empty set of location","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:11562"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":794,"ins":{"up_context":[{"change":3,"pos":11640}],"down_context":[{"change":2,"pos":29608}],"flag":"BLOCK","start":15596,"end":15673,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11640},"to":{"change":3,"start":11640,"end":11716},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" transition $g \\in \\GT$ is a finite non-empty set of transitions ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15672"}}],"del_contents":[{"Del":{"text":" transition $g \\in \\GT$ is a finit non-empty set of transitions ","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:11715"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":797,"ins":{"up_context":[{"change":3,"pos":11791}],"down_context":[{"change":2,"pos":29657}],"flag":"BLOCK","start":15674,"end":15742,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11791},"to":{"change":3,"start":11791,"end":11856},"introduced_by":3}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" \\item a source and target location $l,l' \\in \\Loc$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15741"}}],"del_contents":[{"Del":{"text":" \\item a source and target location $l,l' \\in L$.","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:11855"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":803,"ins":{"up_context":[{"change":2,"pos":30010}],"down_context":[{"change":2,"pos":30091}],"flag":"BLOCK","start":15743,"end":15822,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":30010},"to":{"change":2,"start":30010,"end":30091},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" containing variables or distribution functions. All $t \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15821"}}],"del_contents":[{"Del":{"text":" containing variables or a distribution functions. All $t \\in","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30090"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":810,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":12623}],"down_context":[{"change":3,"pos":12623}],"flag":"BLOCK","start":15823,"end":19846,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":" \\end{enumerate}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15842"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15859"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15860"}},{"Add":{"text":"\\subsection{Probability space of a program\\label{ssec:probabilityspace}}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:15933"}},{"Add":{"text":"Before defining the semantics of a \\gls{pip} a new special location $l_\\bot$ is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16013"}},{"Add":{"text":"introduced that will be used to indicate the termination of a program as well as","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16094"}},{"Add":{"text":"a virtual transition $t_\\bot$ and general transition $g_\\bot = \\{t_\\bot\\}$ with","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16174"}},{"Add":{"text":"the same purpose. Instead of just vaguely \\enquote{terminating} a program takes","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16254"}},{"Add":{"text":"the transition $g_\\bot$ to the location $l_\\bot$ if and only if no other","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16327"}},{"Add":{"text":"transition is walkable. Since no normal transition leaves the location $l_\\bot$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16407"}},{"Add":{"text":"the run loops indefinitely on the location $l_\\bot$ after termination. In","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16481"}},{"Add":{"text":"addition a new transition $t_\\text{in}$ will be used for the start of the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16555"}},{"Add":{"text":"program. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16565"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16566"}},{"Add":{"text":"A state $s$ is a variable assignment for the variables of a program $s: \\V","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16641"}},{"Add":{"text":"\\rightarrow \\Z$. \\Sigma is the set of all states. The set of configuration is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16719"}},{"Add":{"text":"defined as $\\confs = L \\union \\{l_\\bot\\} \\times \\T \\union \\{t_{\\text{in}},","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16794"}},{"Add":{"text":"t_\\bot\\} \\times \\Sigma$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16820"}},{"Add":{"text":"Note that additionally to the location and state, the last transition taken to","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16899"}},{"Add":{"text":"the current location is captured as well. This won't be relevant for the partial","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:16980"}},{"Add":{"text":"evaluation but is important to define the probabilistic properties of a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17052"}},{"Add":{"text":"\\gls{pip}. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17064"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17065"}},{"Add":{"text":"A run of the program is an \\textit{infinite} sequence of configurations, and the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17146"}},{"Add":{"text":"set of all runs is defined as $\\runs = \\confs^\\omega$. In contrast a finite","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17222"}},{"Add":{"text":"prefix is a finite sequence of configurations. The set of all finite prefixes is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17303"}},{"Add":{"text":"defined as $\\fpath = \\confs^*$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17336"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17337"}},{"Add":{"text":"\\begin{rem} ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17350"}},{"Add":{"text":" The set of configurations does not exclude invalid combinations of","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17421"}},{"Add":{"text":" locations and transitions, that is a configuration with a location that is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17500"}},{"Add":{"text":" not the target of the incoming transition, or a state that is impossible to","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17580"}},{"Add":{"text":" reach via the incoming transition. Conversely, the set of runs and finite","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17658"}},{"Add":{"text":" prefixes does not exclude invalid paths, e.g. two consecutive configurations","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17739"}},{"Add":{"text":" that cannot be reached via the given transition, etc. The validity of a path","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17820"}},{"Add":{"text":" will be described by a probability measure where invalid paths have a zero","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17899"}},{"Add":{"text":" probability. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17917"}},{"Add":{"text":"\\end{rem}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17927"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:17928"}},{"Add":{"text":"For a \\gls{pip} one can define a probability space $(\\runs, \\F, \\PrSs)$, where the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18011"}},{"Add":{"text":"outcomes of the probabilistic event are the runs on the program. Every distinct","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18091"}},{"Add":{"text":"run is measurable hence the $\\sigma$-algebra $\\F$ is defined to contain every","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18169"}},{"Add":{"text":"set ${r} \\in \\F$ for $r \\in \\runs$. The probability measure $\\prSs$ describes","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18247"}},{"Add":{"text":"the probability of the given run for a scheduler $\\scheduler$ and the input","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18323"}},{"Add":{"text":"given to the program as the initial state $s_0$. Formally the probability space","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18403"}},{"Add":{"text":"is defined by a cylindrical construction expanding the length of finite prefixes","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18484"}},{"Add":{"text":"up to infinity. For the detailed construction we'll refer to \\cite{meyer20arxiv}.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18566"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18567"}},{"Add":{"text":"On any given configuration a scheduler resolves the non-determinism first. The","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18646"}},{"Add":{"text":"probability measure will use the result of the scheduler instead of the previous","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18727"}},{"Add":{"text":"configuration. The scheduler keeps the values of all program variables from the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18807"}},{"Add":{"text":"previous configuration. It selects a general transition $g$ and a variable","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18882"}},{"Add":{"text":"assignment $\\tilde{s}$ satisfying the guard of the general transition. If no","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:18959"}},{"Add":{"text":"such transition is found of the program is already in the terminating state","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19035"}},{"Add":{"text":"$l_\\bot$ it takes the special transition $g_\\bot$ indicating termination.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19109"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19110"}},{"Add":{"text":"\\begin{definition}[Scheduler]\\label{def:scheduler} \\cite{meyer20arxiv}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19181"}},{"Add":{"text":" A function $\\scheduler : \\confs \\rightarrow (\\GT \\uplus \\{g_\\bot\\})$ is a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19259"}},{"Add":{"text":" scheduler if for every configuration $c = (l,t,s) \\in \\confs$,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19326"}},{"Add":{"text":" $\\scheduler(c) = (g, s')$ implies:","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19365"}},{"Add":{"text":" \\begin{enumerate}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19387"}},{"Add":{"text":" \\item \\label{itm:scheduler1} $s'(x) = s(x)$ for all $x \\in \\PV$ ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19460"}},{"Add":{"text":" \\item $l$ is the start location $l_g$ of the general transition $g$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19537"}},{"Add":{"text":" \\item \\label{itm:scheduler3} $s' \\models \\tau_g$ for the guard $\\tau_g$ of the general","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19632"}},{"Add":{"text":" transition $g$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19661"}},{"Add":{"text":" \\item $g = g_\\bot$ and $s' = s$, if $l=l_bot$, $t=t_\\bot$, or no $g' \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19742"}},{"Add":{"text":" \\GT$ and $s'\\in \\Sigma$ satisfy \\cref{itm:scheduler1} to","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19811"}},{"Add":{"text":" \\cref{itm:scheduler3}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19845"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":881,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":39932}],"down_context":[{"change":2,"pos":30168}],"flag":"BLOCK","start":19847,"end":29399,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"Let $\\scheduler$ be a scheduler and $s_0$ be an initial state. First, the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19920"}},{"Add":{"text":"probability for a program to start at a configuration $c$ is 1 only for the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:19996"}},{"Add":{"text":"configuration that has the initial state $s_0$ at the start location $l_0$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20071"}},{"Add":{"text":"coming from the initial transition $t_\\text{in}$. All other configuration are","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20149"}},{"Add":{"text":"invalid starting configurations and get assigned a zero probability by the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20224"}},{"Add":{"text":"probability measure $\\prSs : \\confs \\rightarrow [0,1]$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20279"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20280"}},{"Add":{"text":"\\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20297"}},{"Add":{"text":" \\prSs(c) = \\begin{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20326"}},{"Add":{"text":" 1 & \\text{ if } c = (l_0, s_0, t_\\text{in}) \\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20381"}},{"Add":{"text":" 0 & \\text{ otherwise}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20411"}},{"Add":{"text":" \\end{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20427"}},{"Add":{"text":"\\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20442"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20443"}},{"Add":{"text":"Lets say the program ran up to a configuration $c=(l,t,s)$. The scheduler","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20517"}},{"Add":{"text":"resolves the non-deterministic sampling and branching to $\\scheduler(c) = (g,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20595"}},{"Add":{"text":"\\tilde{s})$. The probability for the event $c \\rightarrow c'$ that $c'$ follows","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20675"}},{"Add":{"text":"the configuration $c$ with $c' = (l', t', s')$ and $t' = (l, p, \\tau, \\eta, l')","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20755"}},{"Add":{"text":"\\in g$ depends on three things: First the transition $t \\in g$ is taken with the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20836"}},{"Add":{"text":"probability $p$, second the probability that each program variables $x\\in\\PV$ is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20917"}},{"Add":{"text":"updated to the value $s'(x)$ by the probabilistic update - recall definition","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:20994"}},{"Add":{"text":"\\ref{def:polyindeterminates}, third that the temporary variables are sampled by","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21074"}},{"Add":{"text":"the scheduler equal to the target state. The result is the probability measure","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21153"}},{"Add":{"text":"$\\prSs: \\confs^2 \\rightarrow [0,1]$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21191"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21192"}},{"Add":{"text":"\\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21206"}},{"Add":{"text":" \\prSs(c \\rightarrow c') = p \\cdot \\prod_{x\\in\\PV} [\\eta(x)](\\tilde{s})(s'(x))","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21288"}},{"Add":{"text":" \\cdot \\prod_{u\\in\\V\\backslash\\PV} \\delta_{\\tilde{s}(u),s(u)},","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21354"}},{"Add":{"text":"\\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21366"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21367"}},{"Add":{"text":"with any $z_1, z_2 \\in \\Z$: ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21396"}},{"Add":{"text":"\\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21413"}},{"Add":{"text":" \\delta_{z_1,z_2} = \\begin{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21450"}},{"Add":{"text":" 1, & \\text{if } z_1 = z_2 \\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21487"}},{"Add":{"text":" 0, & \\text{if } z_1 \\neq z_2.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21525"}},{"Add":{"text":" \\end{cases}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21541"}},{"Add":{"text":"\\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21556"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21557"}},{"Add":{"text":"Naturally for all other configurations $c'$, such as configuration that are not","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21637"}},{"Add":{"text":"reachable by the given transition, or transitions that were not selected by the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21717"}},{"Add":{"text":"scheduler we define $\\prSs(c \\rightarrow c') = 0$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21769"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21770"}},{"Add":{"text":"\\begin{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21784"}},{"Add":{"text":" \\prSs(f) = \\prSs(c_0) \\cdot \\prod_{i=1}^n \\prSs(c_{i-1} \\rightarrow c_i)","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21861"}},{"Add":{"text":"\\end{align}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21873"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21874"}},{"Add":{"text":"By a cylindrical construction one gets the final probability measure for the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:21951"}},{"Add":{"text":"infinite runs $\\PrSs : \\runs \\rightarrow [0,1]$ and the probability space","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22025"}},{"Add":{"text":"$(\\runs, \\F, \\PrSs)$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22047"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22048"}},{"Add":{"text":"\\begin{definition}[Admissible Run]\\label{def:admissible}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22105"}},{"Add":{"text":" An finite prefix $f \\in \\fpath$ is \\textit{admissible} if and only if","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22179"}},{"Add":{"text":" $\\prSs(f) > 0$. A run $c_0c_1\\dots \\in \\runs$ is \\textit{admissible} if and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22259"}},{"Add":{"text":" only if every finite prefix $c_0\\dots c_n \\in\\fpath$ is admissible.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22331"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22348"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22349"}},{"Add":{"text":"\\begin{rem}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22361"}},{"Add":{"text":" An admissible run can very well have have a zero probability if the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22433"}},{"Add":{"text":" probability of its prefixes approach zero for $n \\rightarrow \\inf$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22505"}},{"Add":{"text":"\\end{rem}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22515"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22516"}},{"Add":{"text":"\\begin{definition}[Terminating Run]\\label{def:termination}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22575"}},{"Add":{"text":" A run is is terminating if it is admissible and it has a finite prefix","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22650"}},{"Add":{"text":" ending in the location $l_\\bot$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22687"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22704"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22705"}},{"Add":{"text":"Because by definition only the terminating transition $t_\\bot$ is admissible","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22782"}},{"Add":{"text":"when the program is in the terminal location $l_\\bot$ and the following","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22854"}},{"Add":{"text":"configuration must again be in the terminal location $l_\\bot$. A terminating run","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:22935"}},{"Add":{"text":"must end with infinitely many repetitions of a terminating configuration","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23008"}},{"Add":{"text":"$c_\\bot=(l_\\bot,t_\\bot,s)$ for some assignment $s\\in\\Sigma$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23069"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23070"}},{"Add":{"text":"\\subsection{Bounds}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23090"}},{"Add":{"text":"The whole goal of \\gls{koat}'s analysis is to find bounds. A bound is an","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23163"}},{"Add":{"text":"expression that describes the upper limit of a property of the program.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23235"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23236"}},{"Add":{"text":"\\begin{definition}[Bounds\\cite{meyer2021tacas}]\\label{def:bounds}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23302"}},{"Add":{"text":" The set of bounds $\\B$ is the smallest set with $\\PV \\union \\R_{\\geq 0}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23378"}},{"Add":{"text":" \\subseteq \\B$, and where $b_1,b_2 \\in \\B$ and $v\\in \\R_{\\geq 1}$ imply $b_1 +","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23460"}},{"Add":{"text":" b_2, b_1 \\cdot b_2 \\in \\B$ and $v^{b_1} \\in \\B$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23513"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23530"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23531"}},{"Add":{"text":"During analysis of classical integer programs, one is especially interested in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23610"}},{"Add":{"text":"runtime and size bounds. A runtime bound is an upper bound on the number of","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23686"}},{"Add":{"text":"visits to a transition in the program over all admissible runs, whereas a size","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23765"}},{"Add":{"text":"bound describes the highest value of a program variable observed at a","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23835"}},{"Add":{"text":"transition over all admissible runs. Because the values observed in a run are","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23913"}},{"Add":{"text":"highly dependent on the decisions made by the scheduler $\\scheduler$, the bounds ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:23995"}},{"Add":{"text":"we take the supremum over all $\\scheduler$. One can also picture the scheduler ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24075"}},{"Add":{"text":"as an adversary that always takes the worst decision possible for runtime and","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24153"}},{"Add":{"text":"size-bounds.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24166"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24167"}},{"Add":{"text":"\\begin{definition}[Runtime and Size Bounds\\cite{meyer2021tacas}\\label{def:runtimebounds}]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24257"}},{"Add":{"text":" $\\RB: \\T \\rightarrow \\B$ is a runtime bound and $\\SB: \\T \\times \\V","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24328"}},{"Add":{"text":" \\rightarrow \\B$ is a size bound if for all transitions $t\\in\\T$, all","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24401"}},{"Add":{"text":" variables $x\\in\\V$, all schedulers $\\scheduler$, and all states $s_0 \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24478"}},{"Add":{"text":" \\Sigma$, we have","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24499"}},{"Add":{"text":" \\begin{align*}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24518"}},{"Add":{"text":" &|s_0|(\\RB(t)) \\geq \\sup \\set{ |\\set{i}{t_i =","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24572"}},{"Add":{"text":" t}|}{f=(\\_,t_0,\\_)\\dots(\\_,t_n,\\_), \\prSs(f) > 0} \\\\","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24633"}},{"Add":{"text":" &|s_0|(\\SB(t, x)) \\geq \\sup \\set{ |s(x)| }{f=\\dots(\\_,t,s), \\prSs(f) >","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24712"}},{"Add":{"text":" 0}.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24724"}},{"Add":{"text":" \\end{align*}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24741"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24758"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24759"}},{"Add":{"text":"In probabilistic programs not only the worst case is of interest, but also the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24838"}},{"Add":{"text":"probable case. For example a program might run indefinitely in the worst case","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24916"}},{"Add":{"text":"but the worst-case has a probability approaching zero. The expected bounds are","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:24995"}},{"Add":{"text":"defined using the expected value of random variables in the probability space","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25073"}},{"Add":{"text":"$(\\runs, \\F, \\PrSs)$ defined in \\Sref{ssec:probabilityspace}. Moreover, recall","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25152"}},{"Add":{"text":"definition \\ref{def:expected_value}.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25189"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25190"}},{"Add":{"text":"\\begin{definition}[Expected Runtime Complexity, \\acrshort{past}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25254"}},{"Add":{"text":" \\cite{meyer2021tacas}\\label{def:past}]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25297"}},{"Add":{"text":" For $g \\in \\GT$ its runtime is the random variable $\\Rt(g)$ where $R: \\GT","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25375"}},{"Add":{"text":" \\rightarrow \\runs \\rightarrow \\overline{\\N}$ with \\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25446"}},{"Add":{"text":" \\Rt(g)((\\_,t_0,\\_)(\\_,t_i,\\_)\\dots) = |\\set{i}{t_i \\in g}|. \\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25525"}},{"Add":{"text":" For a scheduler $\\scheduler$ and starting state $s_0\\in\\Sigma$, the expected","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25606"}},{"Add":{"text":" runtime complexity of $g\\in\\GT$ is $\\E_{\\scheduler,s_0}(\\Rt(g))$ and the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25683"}},{"Add":{"text":" expected runtime complexity of $\\Prog$ is $\\sum_{g\\in\\GT}\\E_{\\scheduler,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25760"}},{"Add":{"text":" s_0}(\\Rt(g)))$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25780"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25781"}},{"Add":{"text":" If $\\Prog$'s expected runtime complexity is finite for every scheduler","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25856"}},{"Add":{"text":" $\\scheduler$ and every initial state $s_0$, then $\\Prog$ is called","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25927"}},{"Add":{"text":" \\acrfull{past}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25946"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25963"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:25964"}},{"Add":{"text":"The expected size bound is defined similarly ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26010"}},{"Add":{"text":"\\begin{definition}[Expected Size","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26043"}},{"Add":{"text":" Complexity\\cite{meyer2021tacas}\\label{def:expectedcomplexity}]","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26110"}},{"Add":{"text":" The set of general result variables is $\\GRV = \\set{(g,l,x)}{g\\in\\GT,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26184"}},{"Add":{"text":" x\\in\\PV, (\\_,\\_,\\_,\\_,l) \\in g}$. The size of $\\alpha = (g,l,x) \\in \\GRV$ is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26265"}},{"Add":{"text":" the random variable $\\S(\\alpha)$ where $\\S : \\GRV \\rightarrow (\\runs","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26338"}},{"Add":{"text":" \\rightarrow \\overline{N})$ with","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26374"}},{"Add":{"text":" \\begin{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26395"}},{"Add":{"text":" \\S(g,l,x)((l_0,t_0,s_0)(l_1,t_1,s_1)\\dots) = \\sup \\set{|s_i(x)|}{l_i =","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26474"}},{"Add":{"text":" l, t_i \\in g}.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26497"}},{"Add":{"text":" \\end{equation}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26516"}},{"Add":{"text":" For a scheduler $\\scheduler$ and starting state $s_0$, the expected size","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26593"}},{"Add":{"text":" complexity of $\\alpha \\in \\GRV$ is $\\E_{\\scheduler,s_0}(\\S(\\alpha))$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26667"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26684"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26685"}},{"Add":{"text":"\\begin{definition}[Expected Runtime and Size","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26730"}},{"Add":{"text":" Bounds\\cite{meyer2021tacas}\\label{def:expectedbounds}]\\phantom{ }","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26800"}},{"Add":{"text":" \\begin{itemize}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26820"}},{"Add":{"text":" \\item $\\RBe : \\GT \\rightarrow \\B$ is an expected runtime bound if for","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26898"}},{"Add":{"text":" all $g\\in\\GT$, all schedulers $\\scheduler$, and all $s_0 \\Sigma$, we","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:26979"}},{"Add":{"text":" have $|s_0|(\\RBe(g)) \\geq \\ESs(\\Rt(g))$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27032"}},{"Add":{"text":" \\item $\\SBe : \\GRV \\rightarrow \\B$ is an expected size bound if for","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27108"}},{"Add":{"text":" all $\\alpha\\in\\GT$, all schedulers $\\scheduler$, and all $s_0 \\Sigma$, we","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27194"}},{"Add":{"text":" have $|s_0|(\\SBe(g)) \\geq \\ESs(\\S(g))$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27246"}},{"Add":{"text":" \\end{itemize}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27264"}},{"Add":{"text":"\\end{definition}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27281"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27282"}},{"Add":{"text":"\\begin{example}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27298"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27299"}},{"Add":{"text":"\\end{example}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27313"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27314"}},{"Add":{"text":"\\subsection{Costs}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27333"}},{"Add":{"text":"It is useful to add the notion of costs to a transition to reflect variable","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27409"}},{"Add":{"text":"complexity of transitions. The accumulative costs of a run are the sum of costs","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27489"}},{"Add":{"text":"for each transition taken. Accumulative costs can simulated by an additional","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27566"}},{"Add":{"text":"program variable $\\mathbf{c} \\in \\PV$ that is updated only by polynomials of the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27647"}},{"Add":{"text":"form $\\eta(\\mathbf{c}) = \\mathbf{c} + c_t$, where $c_t \\in","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27706"}},{"Add":{"text":"\\Z$ is the cost associated with the transition $t\\in\\T$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27763"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27764"}},{"Add":{"text":"For a given size bound $\\SB$ for the \\gls{pip} $\\Prog$ and a starting assignment","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27845"}},{"Add":{"text":"$s_0$, the cost bound is defined as $|s_0|(\\SB(t_\\bot,\\mathbf{c}))$, and given","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27924"}},{"Add":{"text":"an expected size bound $\\SBe$, the expected cost bound is defined as","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:27993"}},{"Add":{"text":"$|s_0|\\SBe(t_\\bot, mathbf{c})$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28025"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28026"}},{"Add":{"text":"\\subsection{Graph operations}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28056"}},{"Add":{"text":"A \\gls{pip} contains a directed graph with vertices $\\L$ and edges $\\T$. We will","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28137"}},{"Add":{"text":"define some graph operations that will become useful during the thesis. The set","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28217"}},{"Add":{"text":"of directed graphs over locations $\\L$ and transitions $\\T$ is denoted by $\\G$. ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28298"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28299"}},{"Add":{"text":"% The graph $G(P)$ denotes the graph contained within a \\gls{pip} $P$ and is","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28376"}},{"Add":{"text":"% defined as $G(P) = (L, \\T)$. The following graph operations will be defined on","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28457"}},{"Add":{"text":"% graphs only, but work equally well for \\glspl{pip} by using the contained graph","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28539"}},{"Add":{"text":"% operation first. However, the result might not be a valid integer program, per-se.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28624"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28625"}},{"Add":{"text":"A set of transitions $T \\subseteq \\T$ induces a sub-graph $G(T)$ in a program $P$,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28708"}},{"Add":{"text":"with $\\G: 2^\\T \\rightarrow \\G$. Similarly a set of locations $L \\subseteq \\Loc$","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28788"}},{"Add":{"text":"induces a sub-graph $G(L)$ in $P$, with $G: 2^\\Loc \\rightarrow \\G$.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28856"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28857"}},{"Add":{"text":"\\begin{rem}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28869"}},{"Add":{"text":" The resulting graphs cannot allways be lifted to a valid \\gls{pip}, since","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:28947"}},{"Add":{"text":" cumulative probability of general transitions are not necessarily preserved.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29028"}},{"Add":{"text":"\\end{rem}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29038"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29039"}},{"Add":{"text":"The operations $\\Tin : \\Loc \\rightarrow 2^\\T$, $\\Tout : \\Loc \\rightarrow 2^\\T$,","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29119"}},{"Add":{"text":"$\\GTin : \\Loc \\rightarrow 2^\\GT$, and $\\GTout: \\Loc \\rightarrow 2^\\GT$ return the","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29201"}},{"Add":{"text":"set of (general) transitions starting or ending in the given location.","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29272"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29273"}},{"Add":{"text":"Adding a transition and possibly new locations therein to graph is denoted by","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29351"}},{"Add":{"text":"the plus operator $+: \\G, \\T \\rightarrow \\G$ ","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29397"}},{"Add":{"text":"","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29398"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":1207,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":30618},"to":{"change":2,"start":30618,"end":34506},"introduced_by":2}],"inode":{"change":3,"pos":8115}}},"contents":[{"Del":{"text":"\\subsection{Semantics}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30640"}},{"Del":{"text":"\\todo{open question regarding temporary variables} ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30692"}},{"Del":{"text":"% the original definition alled states defining variables, but this let's","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30766"}},{"Del":{"text":"% temporary variables carry-over to the next transition. Is this what we","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30839"}},{"Del":{"text":"% want?","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30847"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30848"}},{"Del":{"text":"Before defining the semantics of a \\gls{pip} a new special location $l_\\bot$ is","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:30928"}},{"Del":{"text":"introduced that will be used to indicate the termination of a program as well as","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31009"}},{"Del":{"text":"a virtual transition $t_\\bot$ and general transition $gt_\\bot = \\{t_\\bot\\}$ with","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31090"}},{"Del":{"text":"the same purpose. Instead of just vaguely \\enquote{terminating} a program takes","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31170"}},{"Del":{"text":"the transition $gt_\\bot$ to the location $l_\\bot$ if and only if no other","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31244"}},{"Del":{"text":"transition is walkable. Since no normal transition leaves the location $l_\\bot$","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31324"}},{"Del":{"text":"the run loops indefinitely on the location $l_\\bot$ after termination. In","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31398"}},{"Del":{"text":"addition a new transition $t_\\text{in}$ will be used for the start of the","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31472"}},{"Del":{"text":"program. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31482"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31483"}},{"Del":{"text":"A state $s$ is a variable assignment for the variables of a program $s: \\V","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31558"}},{"Del":{"text":"\\rightarrow \\Z$. \\Sigma is the set of all states. The set of configuration is","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31636"}},{"Del":{"text":"defined as $\\confs = L \\union \\{l_\\bot\\} \\times \\T \\union \\{t_{\\text{in}},","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31711"}},{"Del":{"text":"t_\\bot\\} \\times \\Sigma$. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31737"}},{"Del":{"text":"Note that additionally to the location and state, the last transition taken to","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31816"}},{"Del":{"text":"the current location is captured as well. This won't be relevant for the partial","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31897"}},{"Del":{"text":"evaluation but is important to define the probabilistic properties of a","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31969"}},{"Del":{"text":"\\gls{pip}. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31981"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:31982"}},{"Del":{"text":"A run of the program is an \\textit{infinite} sequence of configurations, and the","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32063"}},{"Del":{"text":"set of all runs is defined as $\\runs = \\confs^\\omega$. In contrast a finite","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32139"}},{"Del":{"text":"prefix is a finite sequence of configurations. The set of all finite prefixes is","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32220"}},{"Del":{"text":"defined as $\\fpath = \\confs^*$. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32253"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32254"}},{"Del":{"text":"\\begin{rem} ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32267"}},{"Del":{"text":" The set of configurations does not exclude invalid combinations of","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32338"}},{"Del":{"text":" locations and transitions, that is a configuration with a location that is","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32417"}},{"Del":{"text":" not the target of the incoming transition, or a state that is impossible to","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32497"}},{"Del":{"text":" reach via the incoming transition. Conversely, the set of runs and finite","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32575"}},{"Del":{"text":" prefixes does not exclude invalid paths, e.g. two consecutive configurations","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32656"}},{"Del":{"text":" that cannot be reached via the given transition, etc. The validity of a path","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32737"}},{"Del":{"text":" will be described by a probability measure where invalid paths have a zero","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32816"}},{"Del":{"text":" probability. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32834"}},{"Del":{"text":"\\end{rem}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32844"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32845"}},{"Del":{"text":"For a \\gls{pip} one can define a $(\\runs, \\F, \\textit{pr})$. The outcomes of","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32922"}},{"Del":{"text":"the probabilistic event in this space are the runs on the program. Every","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:32995"}},{"Del":{"text":"distinct run is measurable hence the $\\sigma$-algebra $\\F$ is defined to contain","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33076"}},{"Del":{"text":"every set ${r} \\in \\F$ for $r \\in \\runs$. The probability measure $pr$ describes","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33157"}},{"Del":{"text":"the probability of the given runs. Formally the probability space is defined by","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33237"}},{"Del":{"text":"a cylindrical construction \\todo{elaborate}. Since the construction is rather","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33315"}},{"Del":{"text":"involved we will only sum up and the properties relevant to this thesis.","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33388"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33389"}},{"Del":{"text":"First the probability of a run is separate from the non-determinism. So for all","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33469"}},{"Del":{"text":"the considerations the non determinism is assumed to be decided by a scheduler","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33548"}},{"Del":{"text":"and the probability measure depends on the scheduler. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33603"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33604"}},{"Del":{"text":"The probability of specific run in the probability space is equal to the","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33677"}},{"Del":{"text":"probability that every transition in the run is taken. Naturally, invalid","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33751"}},{"Del":{"text":"transitions (either because they do not exist in the program, or because the","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33828"}},{"Del":{"text":"guard is not satisfied) have a zero probability. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33878"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33879"}},{"Del":{"text":"The probability space will be used to define the semantics of a \\gls{pip}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33953"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:33954"}},{"Del":{"text":"\\subsection{Notes about the probability measure}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34003"}},{"Del":{"text":"Probability that a variable $x$ takes the value $s(x)$ when taking the","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34074"}},{"Del":{"text":"transition $t$ from an (non-deterministically resolved) assignment $\\tilde{s}$: ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34155"}},{"Del":{"text":"\\todo{redefine with polynomials over indeterminates}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34208"}},{"Del":{"text":"\\begin{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34222"}},{"Del":{"text":" q_{\\tilde{s},t,s(x)}(x)","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34250"}},{"Del":{"text":"\\end{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34262"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34263"}},{"Del":{"text":"(Trivial) probability that the temporary variables got assigned there expected","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34342"}},{"Del":{"text":"values, given a (non-deterministically resolved) assignment $\\tilde{s}$ and the","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34422"}},{"Del":{"text":"resulting assignment $s$","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34447"}},{"Del":{"text":"\\begin{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34461"}},{"Del":{"text":" \\delta_{\\tilde{s}(u),s(u)})","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34493"}},{"Del":{"text":"\\end{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34505"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":1208,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":34507},"to":{"change":2,"start":34507,"end":36270},"introduced_by":2}],"inode":{"change":3,"pos":8115}}},"contents":[{"Del":{"text":"Probability of a transition after a finite prefix: For $F = \\dots (l', t', s') \\in \\fpath$, $(l, t,","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34606"}},{"Del":{"text":"x) \\in \\confs$, $t = (l', p, \\tau, \\eta, l)$.","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34652"}},{"Del":{"text":"\\begin{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34666"}},{"Del":{"text":" pr_{\\mathfrak{S},s_0}((l', t',s') \\rightarrow (l, t, s)) :=","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34730"}},{"Del":{"text":" pr_{\\mathfrak{S},s_0}(f \\rightarrow (l,t,s))= p \\cdot \\prod_{x\\in\\PV}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34805"}},{"Del":{"text":" q_{\\tilde{s},t,s(x)}(x) \\cdot \\prod_{u \\in \\TV} \\delta_{\\tilde{s}(u),s(u)})","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34885"}},{"Del":{"text":"\\end{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34897"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34898"}},{"Del":{"text":"\\begin{rem}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34910"}},{"Del":{"text":" The probability depends on the scheduler $\\mathfrak{S}$ and the starting","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:34987"}},{"Del":{"text":" state $s_0$. ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35005"}},{"Del":{"text":"\\end{rem}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35015"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35016"}},{"Del":{"text":"Probability of a finite prefix. For $f = c_0, \\dots, c_n \\in \\fpath$:","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35086"}},{"Del":{"text":"\\begin{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35100"}},{"Del":{"text":" pr_{\\mathfrak{S},s_0}(f) = pr_{\\mathfrak{S},s_0}(c_0) \\cdot \\prod_{i=1}^n pr_{\\mathfrak{A},s_0}(c_{i-1} \\rightarrow c_i)","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35225"}},{"Del":{"text":"\\end{align}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35237"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35238"}},{"Del":{"text":"Cylindrical construction yields the unique probability measure","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35301"}},{"Del":{"text":"$\\mathbf{P}_{\\mathfrak{S},s_0} : \\F \\rightarrow [0,1]$ for infinite runs","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35374"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35375"}},{"Del":{"text":"\\subsection{Runtime}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35396"}},{"Del":{"text":"\\begin{comment}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35412"}},{"Del":{"text":" for a transition:","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35434"}},{"Del":{"text":" - constant cost","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35454"}},{"Del":{"text":" - most simple case cost = 1 for every transition","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35507"}},{"Del":{"text":" - combining transitions and adding costs","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35552"}},{"Del":{"text":" - costs depending on variables","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35587"}},{"Del":{"text":" for a prefix:","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35605"}},{"Del":{"text":" - finite sequence of configurations","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35645"}},{"Del":{"text":" - runtime = sum of all costs over all steps in the prefix","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35707"}},{"Del":{"text":" - probability = product over all transition probabilities in the prefix","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35783"}},{"Del":{"text":" - legal prefix = non-zero probability","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35825"}},{"Del":{"text":" for a path:","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35841"}},{"Del":{"text":" - infinite sequence of configurations","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35883"}},{"Del":{"text":" - runtime = runtime of the largest non-zero probability prefix","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35950"}},{"Del":{"text":" - pro","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:35960"}},{"Del":{"text":" legal paths = paths with a non-zero ","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36001"}},{"Del":{"text":" for a program:","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36020"}},{"Del":{"text":" - supremum over runtime of all paths","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36061"}},{"Del":{"text":"\\end{comment}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36075"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36076"}},{"Del":{"text":"\\begin{definition}[Runtime of a run]","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36113"}},{"Del":{"text":"\\end{definition}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36130"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36131"}},{"Del":{"text":"\\begin{definition}[Worst-case runtime of a Program]","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36183"}},{"Del":{"text":"\\end{definition}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36200"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36201"}},{"Del":{"text":"\\begin{definition}[Expected runtime of a Program]","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36251"}},{"Del":{"text":"\\end{definition}","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36268"}},{"Del":{"text":"","pos":"QIVGMR6INKBVT5IFCO2UJJQEO4PVW3ZM7IDTCTCOKOX7VKG7UPFAC:36269"}}]}},{"Edit":{"inode":{"change":3,"pos":11899},"path":"acronyms.tex","line":24,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":43267}],"down_context":[],"flag":"BLOCK","start":29400,"end":29460,"inode":{"change":3,"pos":11899}}},"contents":[{"Add":{"text":"\\newacronym{past}{PAST}{probably almost surely terminating}","pos":"KVSF5AFJEIMIYAC264OUAA56SGP5MFAUG3AECKOTUPIXPGULVFQQC:29459"}}]}}],"owner":"paradyx","repo":"ma-tex","token":"fMBwSoSpgfU+uzMUd2CaEsu3Hu7lOP03hOOxDd1mXOI=","login":null}

…

Dependencies

Change contents

Review