Model checking probabilistic pushdown automata

Model Checking Probabilistic Pushdown AutomataJavier EsparzaInstitute for Formal Methods in Computer Science,University of Stuttgart,Universit¨a t str.38,70569Stuttgart,Germany.Anton´ın Kuˇc eraFaculty of Informatics,Masaryk University, Botanick´a68a,60200Brno,Czech Republic.czRichard MayrDepartment of Computer Science,Albert-Ludwigs-University FreiburgGeorges-Koehler-Allee51,D-79110Freiburg,Germany.AbstractWe consider the model checking problem for probabilisticpushdown automata(pPDA)and properties expressible invarious probabilistic logics.We start with properties thatcan be formulated as instances of a generalized randomwalk problem.We prove that both qualitative and quantita-tive model checking for this class of properties and pPDA isdecidable.Then we show that model checking for the qual-itative fragment of the logic PCTL and pPDA is also decid-able.Moreover,we develop an error-tolerant model check-ing algorithm for general PCTL and the subclass of state-less pPDA.Finally,we consider the class of properties de-finable by deterministic B¨u chi automata,and show that bothqualitative and quantitative model checking for pPDA is de-cidable.1.IntroductionProbabilistic systems can be used for modeling systemsthat exhibit uncertainty,such as communication protocolsover unreliable channels,randomized distributed systems,or fault-tolerant systems.Finite-state models of such sys-tems often use variants of probabilistic automata whose1This is a standard notation adopted in concurrency theory.The sub-and various probabilistic logics.We start with a class of Figure1.Bernoulli random walk as a pBPAclass of stateless PDA corresponds to a natural subclass of ACP known as Basic Process Algebra[6].erties expressible in PCTL is strictly larger).In Section4.1, we give a model checking algorithm for the qualitative frag-ment of PCTL and pPDA processes.For general PCTL for-mulae and pBPA processes,an error tolerant model check-ing algorithm is developed in Section4.2.The question whether this result can be extended to pPDA is left open.Finally,in Section5we prove that both qualitative and quantitative model checking for the class of properties de-finable by deterministic B¨u chi automata is decidable for pPDA.Again,this is done without computing the probabil-ity explicitly,but rational lower and upper approximations can be computed up to an arbitrarily small given error.Due to the lack of space,some proofs have been omitted. These can be found in a full version of this paper[14]. 2.Preliminary DefinitionsDefinition2.1.A(fully)probabilistic transition system is a triple where is afinite or countably infinite set of states,is a transition relation, and is a function which to each transition of assigns its probability so that for every we have.(The sum above can be if it is empty,i.e.,if does not have any outgoing transitions.)In the rest of this paper we also write instead of.A path in is afinite or infinite se-quence of states such that for every.We also use to denote the state of(by writing we implicitly impose the condition that the length of is at least).A run is a maximal path, i.e.,a path which cannot be prolonged.The sets of allfinite paths and all runs of are denoted and,respec-tively2.Similarly,the sets of allfinite paths and runs that start in a given are denoted and, respectively.Each determines a basic cylinder which consists of all runs that start with.To everywe associate the probabilistic space where is the-field generated by all basic cylinders where starts with,and is the unique probability function such thatwhere and for every(if,we put).We say that setsand are-equivalent iff.The Logic PCTLPCTL,the probabilistic extension of CTL,was defined by Hansson&Jonsson in[17].Let be acountably infinite set of atomic propositions.The syntax of PCTL3is given by the following abstract syntax equation: Here ranges over,,and. Let be a probabilistic transition system. For all,all,and all,letand for alland for allObviously,Let be a valuation.The denotation of a PCTL formula over w.r.t.,denoted,is defined inductively as follows:As usual,we write instead of.The qualitative fragment of PCTL is obtained by restrict-ing the allowed operator/number combinations to‘’and ‘’,which will be also written as‘’and‘’,resp. (Observe that‘’,‘’are definable from‘’,‘’, and negation;for example,.)Probabilistic PDADefinition 2.2.A probabilistic pushdown automaton (pPDA)is a tuple where is afi-nite set of control states,is afinite stack alphabet,is afinite transition relation(we write instead of),and is a func-tion which to each transition assigns its proba-bility so that for all and we have that.A pBPA is a pPDA with just one control state.Formally, a pBPA is understood as a triple where.In the rest of this paper we adopt a more intuitive nota-tion,writing instead of.if for some,then there issuch that;for each we have iff. Moreover,if is regular,then is also reg-ular.For the rest of this section,let be(fixed) simple sets,and let be the sets as-sociated to in the sense of Definition3.1.To simplify our notation,we adopt the following conventions:For each,let.Observe that if is simple,then so is.For all and,we use to ab-breviate,and to abbreviate.The next lemma says how to computefrom thefinite fam-ily of all,probabilities.Lemma3.3.For each wherewe have that equals towherewhere andwith the convention that empty sum equals to and empty product equals to.Now we show that the probabilities,form the least solution of an effectively constructible system of equations.This can be seen as a generalization of a simi-lar result forfinite-state systems[17,11].In thefinite-state case,the equations are linear and can be further modified so that they have a unique solution(which is then computable, e.g.,by Gauss elimination).In the case of pPDA,the equa-tions are not linear and cannot be generally solved by ana-lytical methods.The question whether the equations can be further modified so that they have a unique solution is left open;we just note that the method used forfinite-state sys-tems is insufficient(this is demonstrated by Example3.5). Let be a set of “variables”.Let us consider the system of recursive equa-tions constructed as follows:if,then for each;other-wise,we putif,then;if,then ;otherwise we putFor given,,and we use and to denote the component of which corresponds to the variable and,respectively. The above defined system of equations determines a unique operator where is the tu-ple of values obtained by evaluating the right-hand sides of the equations where all and are substituted with and,respectively.Theorem3.4.The operator has the leastfixed-point. Moreover,for all and we have thatand.Example3.5.Let us consider the pBPA system of Fig.1, and let,.Then we obtain the following system of equations(since has only one control state, we write and instead of and, resp.):As the least solution we obtain the probabilities ,,,, ,.By applying Lemma3.3we further obtain that,e.g.,.In Example3.5,the least solution of the constructed sys-tem of equations could be computed explicitly.This is gen-erally impossible,but certain properties of the least solution are still decidable.For our purposes,it suffices to consider the class of properties defined in the next theorem. Theorem3.6.Letand,where is the set of all rational constants. Let be expressions built over using‘’and ‘’,and let.It is decidable whether. Proof.We show that,due to Theorem3.4,is ef-fectively expressible as a closed formula of. Hence,the theorem follows from the decidability offirst-order arithmetic of reals[25].For all and,let,, ,and befirst order variables,and letand be the vectors of all,,and, variables,respectively.Let us consider the formula constructed as follows:Observe that the conditions andare expressible only using multiplication,summation,and equality.The expressions and are ob-tained from and by substituting all andwith and,respectively.It follows immedi-ately that iff holds.An immediate consequence of Theorem3.6is the fol-lowing:Theorem 3.7.Let,,and.It is decidable whether.Moreover,there effectively exist ratio-nal numbers such thatand.Proof.We can assume w.l.o.g.that for some .Note that iffby Lemma3.3.Hence,we can apply Theorem3.6.The numbers are computable,e.g.,by the algorithm of Fig.2.4.Model Checking PCTL for pPDA Processes 4.1.Qualitative Fragment of PCTLFor the rest of this section wefix a pPDA.Lemma4.1.Let be a simple set.The setsandare effectively regular.Proof.Immediate.Lemma4.2.Let be simple sets.The setis effectively regu-lar.Proof.Let for all ,.For each we define the set inductively as follows:andUsing Lemma3.3,we can easily check that.To see that the set is effectively regular,for each we construct afinite automaton such that.A-automaton recognizing the setcan then be constructed using standard algorithms of au-tomata theory(in particular,note that regular languages are effectively closed under reverse).The states of are all subsets of,is the initial state,is the input alpha-bet,final states are those where for everywe have that(in particular,note that is afinal state),and transition function is given by iff for ev-ery we have that and.Note that for each. The definition of is effective due to Theorem3.6.It is straightforward to check that.Lemma4.3.Let be simple sets.The setis effectively regu-lar.Proof.Let for all ,.For each we define the set inductively as follows:andThe factfollows immediately from Lemma3.3.The set is effectively regular,which can be shown by constructing a finite automaton recognizing the set.This construction and the rest of the argument are very similar to the ones of the proof of Lemma4.2.There-fore,they are not given explicitly.Theorem4.4.Let be a qualitative pCTL formula and a regular valuation.The set is effectively regular.Proof.By induction on the structure of.The cases when and follow immediately.For Boolean connectives we use the fact that regular sets are closed under complement and intersection.The other cases arecovered by Lemma4.1,4.2,and4.3(here we also need Lemma3.2).4.2.Model Checking PCTL for pBPA ProcessesIn this section we provide an error tolerant model check-ing algorithm for PCTL formulae and pBPA processes. Since it is not so obvious what is meant by error tolerance in the context of PCTL model checking,this notion is de-fined formally.Let be a probabilistic transition sys-tem and.For every negation-free PCTL for-mula and valuation we define the denotation of over w.r.t.with error tolerance,denoted,in the same way as.The only exception is whereif,thenif,thenNote that for every negation-free formula we have that.Negations can be“pushed inside”to atomic propositions using dual connectives(note that,e.g., is equivalent to),and for regular val-uations we can further replace every with a fresh propo-sition where is the complement of.Hence,we can assume w.l.o.g.that is negation-free.An error tolerant PCTL model checking algorithm is an algorithm which,for each PCTL formula,valuation, ,and,outputs YES/NO so thatif,then the answer is YES;if the answer is YES,then.For the rest of this section,let usfix a pBPA.Since has just one(or“none”)control state ,we write and instead of and,re-spectively.Lemma4.5.Let be a simple set,,and.The setis effectively regular.Proof.Immediate.The following lemma presents the crucial part of the al-gorithm.This is the place where we need the assumption that is stateless.Lemma4.6.Let be simple sets.For all and there effectively exist-automata and such that for all we have thatif(or),then(or,respectively.)if(or),then(or,respectively.) Theorem 4.7.There is an error-tolerant PCTL model checking algorithm for pBPA processes.Proof.The proof is similar to the one of Theorem4.4,us-ing Lemma4.5and4.6instead of Lemma4.1,4.2,and4.3. Note that Lemma3.2is applicable also to pBPA(the sys-tem constructed in Lemma3.2has the same set of con-trol states as the original system).5.Model Checking Deterministic B¨uchi Au-tomata SpecificationsDefinition5.1.A deterministic B¨u chi automaton is a tuple,where is afinite alphabet,is afinite set of states,is a(total)transition function(we write instead of),is the initial state,and is a set of accepting states.A run of is an infinite sequence of states such that for every there is such that.A run is accepting if for infinitely many indices.For the rest of this section,wefix a pPDA.Definition5.2.Given a configuration of,we call the head and the tail of.The set of all heads of is also denoted by.We consider specifications given by deterministic B¨u chi automata having as their alphabet.It is well known that every LTL formula whose atomic propositions are in-terpreted over simple sets can be encoded into a nondeter-ministic B¨u chi automaton having as alphabet.Deter-ministic B¨u chi automata can encode the fragment of LTL that can also be expressed in the alternation-free modal-calculus[21].Our results can be extended to atomic propo-sitions interpreted over arbitrary regular sets of configura-tions using the same technique as in[15].Definition5.3.The product of and is a probabilistic pushdown automaton where and are determined as follows:iff and are transitions of and,respec-tively.Notice that every(finite or infinite)path in corre-sponds to a unique path in obtained by projecting the control state of every configuration of the path onto itsfirst component,yielding the configuration.Con-versely,for each path in(starting in some)and each there is exactly one path in starting in be-cause is deterministic.Definition5.4.A configuration of is accepting if.A run in is accepting if it visits accepting configurations infinitely often.A run in is accepting if its corresponding run in is accepting.The probability that a configuration of satisfies the specification is defined asis accepting.We solve the following two problems for a given config-uration of:(a)Given and,do we have?(b)Given,compute rationals such thatand.Forfinite-state automata,the problem can be solved as follows(see[11]).Let be afinite-state automaton.Since the product automaton isfinite,it can be transformed into afinite Markov chain by just‘copying’the proba-bilities of the system[11].It is then possible to reduce prob-lems(a),(b)to the problem of computing the probability of hitting a bottom strongly connected component of which contains a state of the form,where is accepting.In our case,the product automaton is again a pPDA, and so its associated probabilistic transition system is infi-nite.The key to our solution for(a)and(b)is the construc-tion of a newfinite Markov chain that plays the rˆo le of in the case offinite automata.5.1.The Markov chainA B¨u chi pPDA is a tuple, where all elements except for are defined as for pPDA and is a set of accepting states.A configuration of is accepting if.A run of is accepting if it visits accepting configurations infinitely often.For all and,the probabil-ity that a run is accepting is denoted by .Obviously,the model checking problems(a),(b)of the previous section can be reduced to the following problems about a given configuration of a B¨u chi pPDA(where ):(A)Given and,do we have?(B)Given,compute rationals such thatand.For the rest of this section,wefix a B¨u chi pPDA.Definition5.5.Let be an infinite run in.For each we define the minimum of,de-noted,inductively as follows:,where is the least number such that for each.,where. Here is the suffix of that starts with. We say thatflashes at if either and is accepting,or and visits an accept-ing configuration between and(where is not included).Sometimes we abuse language and use to de-note not only a configuration,but the particular occurrence of the configuration that corresponds to the minimum. For all and all we define a ran-dom variable over as follows:The possi-ble values of are all pairs of the form,where and is a booleanflag;there is also a special value.For a given,is de-termined as follows:if isfinite then;if conditions(1)–(3)below are satisfied,then;(1)is infinite;(2)the head of is;(3)flashes at.if conditions(1)and(2)above are satisfied and condition (3)is not satisfied,thenNotice that the random variables are well defined,because they assign to each run exactly one value.Lemma5.6.For all,,and, the probability of exists(i.e.,the set of all which satisfy this condition is-measurable).Moreover,for every rational constant there is an effectively constructible formula of which holds if and only if.The following lemma proves the Markov property.In fact,it follows immediatelly from the construction used in the proof of Lemma5.6.Lemma5.7.The conditional probability of on the hypothesis is equal to the probability of conditioned on,assuming that the probability ofis non-zero.For each control state we define aflag,which is equal either to or depending on whether or not,respectively.Another consequence of Lemma5.6is the following:Lemma 5.8.The conditional probability ofon the hypothesisis equal to the conditional probability ofon the hypothesis,assuming that.Now we can define thefinite Markov chain.Definition5.9.Let be afinite-state Markov chain where the set of states isand transition probabilities are defined as follows:,,,.One can readily check that is indeed a Markov chain,i.e.,for every state of we have that the sum of probabilities of all outgoing transitions of is equal to one.A trajectory in is an infinite sequenceof states of where for ev-ery.To every run of we associate its foot-print,which is an infinite sequence of states of de-fined as follows:if isfinite,then for every we have;if is infinite,then for every we have,where is the head of,and iffflashes at.We say that a given is good if the footprint of is a trajectory in.Our next lemma reveals that al-most all runs are good.Lemma5.10.Let.We have thatis good.It follows directly from the definition of that if both and are states of,then they have the “same”outgoing arcs(i.e.,iff,where).In particular,this means that ifor belongs to some strongly connected com-ponent of,then all of the outgoing arcs of and lead to.Hence,the following definition is correct:Definition5.11.We say that a given is recur-rent if there is a bottom strongly connected componentof such that for some.Each recurrent head is either accepting or rejecting,de-pending on whether contains a state of the formor not,respectively.We say that a run of hits a head if there is some such that the head of is. The next lemma says that an infinite run eventually hits a re-current head.Lemma5.12.Let.The conditional probabil-ity that hits a recurrent head on the hypoth-esis that is infinite is equal to one.So,an infinite run eventually hits a recurrent head.Now we prove that if this head is accepting/rejecting,then the run will be accepting/rejecting with probability one. Lemma5.13.Let be an accepting/rejecting head.The conditional probability that is accept-ing/rejecting on the hypothesis that thefirst recurrent head hit by is accepting/rejecting is equal to one.Lemma5.14.(cf.Proposition4.1.5of[11])Let .is equal to the probability that a trajec-tory from in hits a state of the form where is an accepting head(this is equivalent to saying that the trajectory hits a bottom strongly connected component of which contains a state of the form). Theorem5.15.Let be a B¨u chi pPDA.Given a head,,and, we can decide if.Further,for each we can compute rationals such thatand.Proof.Similarly as in Theorem3.6,we compute a closed formula of such that iff holds.Then,the rationals can be computed by a simple binary search similarly as in Fig.2.Due to Lemma5.14we know that,where is the set of all states of,and consists of all states of the form where is an accepting head.This means that there is a system of recur-sive equations such that appears in the tuple of values which form the least solution of the system(we can assume that is,e.g.,thefirst element of this tu-ple).Since isfinite,these equations are linear and by using the results of[17,11]we can even assume that there is a unique solution.The only problem is that numeric co-efficients in this system of equations are the probabilities of transitions in which cannot be precisely computed. This can be overcome as follows:we construct the men-tioned system of linear equations where we replace each co-efficient with a freshfirst-order variable;let be the tupleof all variables which correspond to the coefficients.Now we can effectively construct the formulawhere says that the tuple of variables is a solu-tion of the constructed system of linear equations.Note that is not closed because the variables of(which appear in the subformula)are free.Due to Lemma5.6, for each of these coefficients there effectively exists a for-mula of which says that a given coefficient is equal to the probability of the corresponding transition in (we just“translate”the definition of given in Def-inition5.9into,using the formulae provided by Lemma5.6).Let by a conjunction of all these formu-lae.The formula is constructed as follows:Obviously,iff holds.We conclude this section by trying to explain why our re-sults cannot be directly extended to nondeterministic B¨u chi automata.First of all,notice that we cannot assign proba-bilities to the transitions of in a meaningful way,be-cause a transition of should‘split’into sev-eral transitions of.In the case of afinite automaton, this problem can be solved by working with the product of and,where is the result of applying the deter-minization construction to.Let denote this product. In[11],a definition of recurrence is provided,which char-acterizes the states of that,loosely speaking,re-turn to with probability1in terms of topological prop-erties of the probabilistic transition system.It is then possible to compute the accepting recurrent states.Unfortunately,this construction does not seem to gener-alize to the case of pushdown automata.The problem is that the B¨u chi pPDA has infinitely many states,and so it must be replaced by the chain.However,inwe cannot directly‘observe’the points at which a run hits an accepting state;we can only observe the points at which a run hits a minimum.While we can use to com-pute the recurrent minima,i.e.,the heads to which one can return with probability1at a minimum,at the moment we do not know how to compute the accepting recurrent min-ima,i.e.,the recurrent minima that not only return,but also visit an accepting configuration along the way.More pre-cisely,we know how to decide for a given head if the runs starting at it will almost surely hit some head out of a set and visit some accept-ing configuration along the way.We can also decide if some head will hit with probability one.How-ever,since we do not know whether or not,this in-formation is not sufficient to decide if is an accepting recurrent minimum.6.ConclusionsWe have provided model checking algorithms for pushdown automata against PCTL specifications,and against linear-time specifications represented as determinis-tic B¨u chi automata.Contrary to the case offinite automata, qualitative properties(i.e.,whether a property holds with probability0or1),depend on the exact probabilities of the transitions.There are many possibilities for future work.An obvi-ous question is what is the complexity of the obtained al-gorithms.Since the formulae offirst order arithmetic which are constructed in our algorithms have afixed alternation depth,we can apply a powerful result of Grigoriev[16] which says that the validity of such formulae is decidable in single exponential time.From this we can easily derive the time complexity of some of our algorithms(for example, the qualitative/quantitative random walk problem of Sec-tion3is decidable in exponential time).Since the complex-ity issues were not the main priority of our work,the effi-ciency of our algorithms can be improved even by relatively straightforward optimizations.Moreover,there is a lot of space for advanced numerical algorithms which might be used to compute the required probabilities with enough pre-cision.An obvious question about linear-time specifications is whether our procedure can be improved to deal with nonde-terministic B¨u chi automata.Another possibility is to con-sider LTL specifications and try to generalize the technique of[11],which modifies the probabilistic transition systems step-by-step and at the same time simplifies the formula,un-til it becomes a propositional formula.7.AcknowledgmentsThe authors would like to thank Stefan Schwoon for many helpful insights.References[1]P.A.Abdulla,C.Baier,S.P.Iyer,and B.Jonsson.Reason-ing about probabilistic channel systems.In Proceedings of CONCUR2000,vol.1877of Lecture Notes in Computer Sci-ence,pp.320–330.Springer,2000.[2]P.A.Abdulla and A.Rabinovich.Verification of probabilis-tic systems with faulty communication.In Proceedings of FoSSaCS2003,vol.2620of Lecture Notes in Computer Sci-ence,pp.39–53.Springer,2003.[3] A.Abney,D.McAllester,and F.Pereira.Relating probabilis-tic grammars and automata.In Proceedings of ACP’99,pp.542–549,1999.[4]R.Alur,K.Etessami,and M.Yannakakis.Analysis of re-cursive state machines.In Proceedings of CAV2001,vol.2102of Lecture Notes in Computer Science,pp.207–220.Springer,2001.[5] A.Aziz,V.Singhal, F.Balarin,R.Brayton,andA.Sangiovanni-Vincentelli.It usually works:The tempo-ral logic of stochastic systems.In Proceedings of CAV’95, vol.939of Lecture Notes in Computer Science,pp.155–165.Springer,1995.[6]J.C.M.Baeten and W.P.Weijland.Process Algebra.No.18in Cambridge Tracts in Theoretical Computer Science.Cam-bridge University Press,1990.[7] C.Baier and B.Engelen.Establishing qualitative propertiesfor probabilistic lossy channel systems:an algorithmic ap-proach.In Proceedings of5th International AMAST Work-shop on Real-Time and Probabilistic Systems(ARTS’99), vol.1601of Lecture Notes in Computer Science,pp.34–52.Springer,1999.[8]N.Bertrand and Ph.Schnoebelen.Model checking lossychannel systems is probably decidable.In Proceedings of FoSSaCS2003,vol.2620of Lecture Notes in Computer Sci-ence,pp.120–135.Springer,2003.[9]O.Burkart and B.Steffen.Model checking the full modalmu-calculus for infinite sequential processes.In Proceed-ings of ICALP’97,vol.1256of Lecture Notes in Computer Science,pp.419–429.Springer,1997.[10] C.Courcoubetis and M.Yannakakis.Verifying temporalproperties offinite-state probabilistic programs.In Proceed-ings of29th Annual Symposium on Foundations of Computer Science,pp.338–345.IEEE Computer Society Press,1988.[11] C.Courcoubetis and M.Yannakakis.The complexity ofprobabilistic verification.Journal of the Association for Computing Machinery,42(4):857–907,1995.[12]J.M.Couvreur,N.Saheb,and G.Sutre.An optimal automataapproach to LTL model checking of probabilistic systems.In Proceedings of LPAR2003,vol.2850of Lecture Notes in Computer Science,pp.361–375.Springer,2003.[13]J.Esparza,D.Hansel,P.Rossmanith,and S.Schwoon.Ef-ficient algorithms for model checking pushdown systems.In Proceedings of CAV2000,vol.1855of Lecture Notes in Computer Science,pp.232–247.Springer,2000.[14]J.Esparza,A.Kuˇc era,and R.Mayr.Model checking prob-abilistic pushdown automata.Technical Report FIMU-RS-2004-03,Faculty of Informatics,Masaryk University,2004.[15]J.Esparza,A.Kuˇc era,and S.Schwoon.Model-checkingLTL with regular valuations for pushdown r-mation and Computation,186(2):355–376,2003.[16] plexity of deciding Tarski algebra.Jour-nal of Symbolic Computation,5(1–2):65–108,1988. [17]H.Hansson and B.Jonsson.A logic for reasoning abouttime and reliability.Formal Aspects of Computing,6:512–535,1994.[18]S.Hart and M.Sharir.Probabilistic temporal logic forfiniteand bounded models.In Proceedings of POPL’84,pp.1–13.ACM Press,1984.[19]M.Huth and M.Z.Kwiatkowska.Quantitative analysis andmodel checking.In Proceedings of LICS’97,pp.111–122.IEEE Computer Society Press,1997.[20]S.P.Iyer and M.Narasimha.Probabilistic lossy channel sys-tems.In Proceedings of TAPSOFT’97,vol.1214of Lecture Notes in Computer Science,pp.667–681.Springer,1997.[21]O.Kupferman and M.Y.Vardi.Freedom,weakness,and de-terminism:From linear-time to branching-time.In Proceed-ings of LICS’98,pp.81–92.IEEE Computer Society Press, 1998.[22] D.Lehman and S.Shelah.Reasoning with time and chance.Information and Control,53:165–198,1982.[23]I.Macarie and M.Ogihara.Properties of probabilistic push-down automata.Theoretical Computer Science,207:117–130,1998.[24] A.Rabinovich.Quantitative analysis of probabilistic lossychannel systems.In Proceedings of ICALP2003,vol.2719of Lecture Notes in Computer Science,pp.1008–1021.Springer,2003.[25] A.Tarski.A Decision Method for Elementary Algebra andGeometry.Univ.of California Press,Berkeley,1951. [26]M.Vardi.Automatic verification of probabilistic concurrentfinite-state programs.In Proceedings of26th Annual Sym-posium on Foundations of Computer Science,pp.327–338.IEEE Computer Society Press,1985.[27]I.Walukiewicz.Pushdown processes:Games and model-rmation and Computation,164(2):234–263, 2001.。