Model Checking Probabilistic Pushdown Automata
Javier Esparza
Institute for Formal Methods in Computer Science,
University of Stuttgart,
Universit¨a t str.38,70569Stuttgart,Germany.
Anton′?n Kuˇc era
Faculty of Informatics,Masaryk University, Botanick′a68a,60200Brno,
Czech Republic.
cz
Richard Mayr
Department of Computer Science,
Albert-Ludwigs-University Freiburg
Georges-Koehler-Allee51,
D-79110Freiburg,Germany.
Abstract
We consider the model checking problem for probabilistic
pushdown automata(pPDA)and properties expressible in
various probabilistic logics.We start with properties that
can be formulated as instances of a generalized random
walk problem.We prove that both qualitative and quantita-
tive model checking for this class of properties and pPDA is
decidable.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-
?nable by deterministic B¨u chi automata,and show that both
qualitative and quantitative model checking for pPDA is de-
cidable.
1.Introduction
Probabilistic systems can be used for modeling systems
that exhibit uncertainty,such as communication protocols
over unreliable channels,randomized distributed systems,
or fault-tolerant systems.Finite-state models of such sys-
tems often use variants of probabilistic automata whose
1This 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 pBPA
class 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-?nable 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 De?nitions
De?nition2.1.A(fully)probabilistic transition system is a triple where is a?nite or countably in?nite 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 a?nite or in?nite 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 all?nite paths and all runs of are denoted and,respec-tively2.Similarly,the sets of all?nite 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 every
we associate the probabilistic space where is the-?eld generated by all basic cylinders where starts with,and is the unique probability function such that
where and for every
(if,we put).We say that sets
and are-equivalent iff
.
The Logic PCTL
PCTL,the probabilistic extension of CTL,was de?ned by Hansson&Jonsson in[17].Let be a
countably in?nite 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,let
and for all
and for all
Obviously,
Let be a valuation.The denotation of a PCTL formula over w.r.t.,denoted,is de?ned 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 de?nable from‘’,‘’, and negation;for example,.)
Probabilistic PDA
De?nition 2.2.A probabilistic pushdown automaton (pPDA)is a tuple where is a?-nite set of control states,is a?nite stack alphabet,
is a?nite 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 is
such that;
for each we have iff. Moreover,if is regular,then is also reg-ular.
For the rest of this section,let be(?xed) simple sets,and let be the sets as-sociated to in the sense of De?nition3.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 compute
from the?nite fam-ily of all,probabilities.
Lemma3.3.For each where
we have that equals to
where
where and
with 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 for?nite-state systems[17,11].In the?nite-state case,the equations are linear and can be further modi?ed 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 modi?ed so that they have a unique solution is left open;we just note that the method used for?nite-state sys-tems is insuf?cient(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 put
if,then;if,then ;otherwise we put
For given,,and we use and to denote the component of which corresponds to the variable and,respectively. The above de?ned 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 least?xed-point. Moreover,for all and we have that
and.
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 suf?ces to consider the class of properties de?ned in the next theorem. Theorem3.6.Let
and,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 of?rst-order arithmetic of reals[25].
For all and,let,, ,and be?rst order variables,and let
and be the vectors of all,,and, variables,respectively.Let us consider the formula constructed as follows:
Observe that the conditions and
are expressible only using multiplication,summation,and equality.The expressions and are ob-tained from and by substituting all and
with 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 that
and.
Proof.We can assume w.l.o.g.that for some .Note that iff
by 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 PCTL
For the rest of this section we?x a pPDA
.
Lemma4.1.Let be a simple set.The sets
and
are effectively regular.
Proof.Immediate.Lemma4.2.Let be simple sets.The set
is effectively regu-lar.
Proof.Let for all ,.For each we de?ne the set inductively as follows:
and
Using Lemma3.3,we can easily check that
.To see that the set is effectively regular,for each we construct a?nite automaton such that
.A-automaton recognizing the set
can 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,?nal states are those where for every
we have that(in particular,note that is a?nal state),and transition function is given by iff for ev-ery we have that and
.Note that for each. The de?nition of is effective due to Theorem3.6.It is straightforward to check that
.
Lemma4.3.Let be simple sets.The set
is effectively regu-lar.
Proof.Let for all ,.For each we de?ne the set inductively as follows:
and
The fact
follows immediately from Lemma3.3.The set is effectively regular,which can be shown by constructing a ?nite 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 are
covered by Lemma4.1,4.2,and4.3(here we also need Lemma3.2).
4.2.Model Checking PCTL for pBPA Processes
In 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-?ned formally.
Let be a probabilistic transition sys-tem and.For every negation-free PCTL for-mula and valuation we de?ne the denotation of over w.r.t.with error tolerance,denoted,in the same way as.The only exception is where
if,then
if,then
Note 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 that
if,then the answer is YES;
if the answer is YES,then.
For the rest of this section,let us?x 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 set
is 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 that
if(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 Speci?cations
De?nition5.1.A deterministic B¨u chi automaton is a tuple
,where is a?nite alphabet,is a?nite 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 in?nite sequence of states such that for every there is such that.
A run is accepting if for in?nitely many indices.
For the rest of this section,we?x a pPDA
.
De?nition5.2.Given a con?guration of,we call the head and the tail of.The set of all heads of is also denoted by.
We consider speci?cations 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 con?gura-tions using the same technique as in[15].
De?nition5.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(?nite or in?nite)path in corre-sponds to a unique path in obtained by projecting the control state of every con?guration of the path onto its?rst component,yielding the con?guration.Con-versely,for each path in(starting in some)and each there is exactly one path in starting in be-cause is deterministic.
De?nition5.4.A con?guration of is accepting if.A run in is accepting if it visits accepting con?gurations in?nitely often.A run in is accepting if its corresponding run in is accepting.
The probability that a con?guration of satis?es the speci?cation is de?ned as
is accepting.
We solve the following two problems for a given con?g-uration of:
(a)Given and,do we have
?
(b)Given,compute rationals such that
and.
For?nite-state automata,the problem can be solved as follows(see[11]).Let be a?nite-state automaton.Since the product automaton is?nite,it can be transformed into a?nite 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 in?-nite.The key to our solution for(a)and(b)is the construc-tion of a new?nite Markov chain that plays the r?o le of in the case of?nite automata.
5.1.The Markov chain
A B¨u chi pPDA is a tuple, where all elements except for are de?ned as for pPDA and is a set of accepting states.
A con?guration of is accepting if.A run of is accepting if it visits accepting con?gurations in?nitely 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 con?guration of a B¨u chi pPDA(where ):
(A)Given and,do we have
?
(B)Given,compute rationals such that
and.
For the rest of this section,we?x a B¨u chi pPDA
.
De?nition5.5.Let be an in?nite run in.For each we de?ne the minimum of,de-noted,inductively as follows:
,where is the least number such that for each.
,where. Here is the suf?x of that starts with. We say that?ashes at if either and is accepting,or and visits an accept-ing con?guration between and(where is not included).
Sometimes we abuse language and use to de-note not only a con?guration,but the particular occurrence of the con?guration that corresponds to the minimum. For all and all we de?ne a ran-dom variable over as follows:The possi-ble values of are all pairs of the form,where and is a boolean?ag;there is also a special value.For a given,is de-termined as follows:
if is?nite then;
if conditions(1)–(3)below are satis?ed,then
;
(1)is in?nite;
(2)the head of is;
(3)?ashes at.
if conditions(1)and(2)above are satis?ed and condition (3)is not satis?ed,then
Notice that the random variables are well de?ned,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 of
is non-zero.
For each control state we de?ne a?ag,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 of
on the hypothesis
is equal to the conditional probability of
on the hypothesis,assuming that
.
Now we can de?ne the?nite Markov chain.
De?nition5.9.Let be a?nite-state Markov chain where the set of states is
and transition probabilities are de?ned 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 in?nite sequence
of states of where for ev-ery.
To every run of we associate its foot-print,which is an in?nite sequence of states of de-?ned as follows:
if is?nite,then for every we have;
if is in?nite,then for every we have
,where is the head of,and iff?ashes 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 that
is good.
It follows directly from the de?nition of that if both and are states of,then they have the “same”outgoing arcs(i.e.,iff
,where).In particular,this means that if
or belongs to some strongly connected com-ponent of,then all of the outgoing arcs of and lead to.Hence,the following de?nition is correct:De?nition5.11.We say that a given is recur-rent if there is a bottom strongly connected component
of such that for some.
Each recurrent head is either accepting or rejecting,de-pending on whether contains a state of the form
or 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 in?nite 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 in?nite is equal to one.
So,an in?nite 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 the?rst 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 that
and.
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.,the?rst element of this tu-ple).Since is?nite,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-ef?cients 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-ef?cient with a fresh?rst-order variable;let be the tuple
of all variables which correspond to the coef?cients.Now we can effectively construct the formula
where 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 coef?cients there effectively exists a for-mula of which says that a given coef?cient is equal to the probability of the corresponding transition in (we just“translate”the de?nition 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 a?nite 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 de?nition 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 in?nitely many states,and so it must be replaced by the chain.However,in
we 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 con?guration 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 con?guration 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 suf?cient to decide if is an accepting recurrent minimum.6.Conclusions
We have provided model checking algorithms for pushdown automata against PCTL speci?cations,and against linear-time speci?cations represented as determinis-tic B¨u chi automata.Contrary to the case of?nite 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 of?rst order arithmetic which are constructed in our algorithms have a?xed 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 ef?-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 speci?cations is whether our procedure can be improved to deal with nonde-terministic B¨u chi automata.Another possibility is to con-sider LTL speci?cations and try to generalize the technique of[11],which modi?es the probabilistic transition systems step-by-step and at the same time simpli?es the formula,un-til it becomes a propositional formula.
7.Acknowledgments
The 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.Veri?cation 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,and
A.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.18
in Cambridge Tracts in Theoretical Computer Science.Cam-bridge University Press,1990.
[7] C.Baier and B.Engelen.Establishing qualitative properties
for 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 lossy
channel 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 modal
mu-calculus for in?nite 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 temporal
properties of?nite-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 of
probabilistic veri?cation.Journal of the Association for Computing Machinery,42(4):857–907,1995.
[12]J.M.Couvreur,N.Saheb,and G.Sutre.An optimal automata
approach 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-
?cient 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-checking
LTL with regular valuations for pushdown https://www.doczj.com/doc/226457531.html,r-mation and Computation,186(2):355–376,2003.
[16] https://www.doczj.com/doc/226457531.html,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 about
time and reliability.Formal Aspects of Computing,6:512–535,1994.
[18]S.Hart and M.Sharir.Probabilistic temporal logic for?nite
and bounded models.In Proceedings of POPL’84,pp.1–13.
ACM Press,1984.
[19]M.Huth and M.Z.Kwiatkowska.Quantitative analysis and
model 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 lossy
channel 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 and
Geometry.Univ.of California Press,Berkeley,1951. [26]M.Vardi.Automatic veri?cation of probabilistic concurrent
?nite-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-
https://www.doczj.com/doc/226457531.html,rmation and Computation,164(2):234–263, 2001.
创客空间建设方案 一、建设背景及意义 （一）建设背景 随着李克强总理在达沃斯论坛上提出“大众创业、万众创新”，“创客”这个新名词也被首次写入政府工作报告。2015年3月2日，科技部“发展众创空间推进大众创新创业电视电话会议”中进一步强调，推进大众创新创业是新时期科技工作的重要任务。2015年3月11日，国务院办公厅印发《关于发展众创空间推进大众创新创业的指导意见》，共计提出8项重点任务，其中第一条就是加快构建众创空间。 创客是创新创业重要的助推者之一，我国国内目前创客的规模仍较小，进一步推进国内的创客运动，需要高校培养更多的新型创客人才。着眼于新工业革命的兴起，在当前互联网“+”的时代下，培养具有“创新、创造、创业、分享”精神的新时代大学生是高校发展的必然趋势。打破专业界限，基于多学科、跨专业，“跨界融合、集成创新”的创新型高校创客空间是高等院校适应新工业革命发展的必然要求。 （二）建设意义 高校在开展“创客空间”的建设方面尚没有规律可循，都是在探索阶段。在我院建设高水平院校的形势下，结合我院“培养态度好、知识新、技能强的实用人才”的办学理念，建立具有“我院特色”的“创客空间”。这不仅是认真贯彻落实《国家中长期教育改革和发展规划纲要》和《关于进一步加强高技能人才工作的意见》的精神；也是深化我院教育教学改革，培养学生创新精神和实践能力的重要途径；更是落实以创新带动创业，创业带动就业，促进我院毕业生充分就业创业的重要措施。同时，我院创客空间的建设，将进一步提高学院知名度，为建设全国高水平院校及创新创业实训基地示范院校打下坚实的基础，具有十分显著的现实意义。 二、建设方案 （一）整体方案介绍 本方案基于线上“创新创意”互联网资源分享平台，通过创客教学体验区、创客开发制作区、创客交流区、创客作品展示区，采用STEAM创新教学方法，以线下产品制作与线上理论学习相结合的模式，采用先进的物联网技术、移动互联技术、桌面操作工具等建立一个线上线下互联互通的创客空间。通过该平台的建设大学生“创客”们可以协作、共享，实现从创意到产品的转变，再通过社会资源的对接、孵化实现从“产品”到“商品”的转化。 同时也为创业者和投资人牵线搭桥，为在江北大学城创业孵化中心创业企业、创业小团队搭建完美的金融服务平台，并为无办公地点团队提供办公场所和交流平台，是所有创业追梦人寻找项目和灵感青睐的归属地。 （二）具体方案及主要功能 1、创新创意平台 旨在为有创新创意的学生、众多制造商、天使投资者搭建一座桥梁，让学生提出好的创意，整合学生资源参与创意设计，为好的创意产品找到合适的生产者和投资者，为制造商寻找好的产品和投资机会。通过该平台，能够让有创新创意思想的学生零成本地更快实现创业梦想。
第四章 等效电路模型参数在线辨识 通过第三章函数拟合的方法可以确定钒电池等效电路模型中的参数，但是在实际运行过程中模型参数随着工作环境温度、充放电循环次数、SOC 等因素发生变化，根据离线试验数据计算得到的参数值估算电池SOC 可能会造成较大的估计误差。因此，在实际运行时，应对钒电池等效电路模型参数进行在线辨识，做出实时修正，提高基于模型估算SOC 的精度。 4.1 基于遗忘因子的最小二乘算法 参数辨识是根据被测系统的输入输出来，通过一定的算法，获得让模型输出值尽量接近系统实际输出值的模型参数估计值。根据能否实时辨识系统的模型参数，可以将常用的参数辨识方法分为离线和在线两类，离线辨识只能在数据采集完成后进行，不能对系统模型实时地在线调整参数，对于具有非线性特性的电池系统往往不能得到满意的辨识结果；在线辨识方法一般能够根据实时采集到的数据对系统模型进行辨识，在线调整系统模型参数。常用的辨识方法有最小二乘法、极大似然估计法和Kalman 滤波法等。因最小二乘法原理简明、收敛较快、容易理解和掌握、方便编程实现等特点，在进行电池模型参数辨识时采用了效果较好的含遗忘因子的递推最小二乘法。 4.1.1 批处理最小二乘法简介 假设被辨识的系统模型： 12121212()()()1n n n n b z b z b z y z G z u z a z a z a z ------+++==++++L L （4-1） 其相应的差分方程为： 1 1 ()()()n n i i i i y k a y k i b u k i ===--+-∑∑（4-2） 若考虑被辨识系统或观测信息中含有噪声，则被辨识模型式（4-2）可改写为： 1 1 ()()()()n n i i i i z k a y k i b u k i v k ===--+-+∑∑（4-3） 式中， ()z k 为系统输出量的第k 次观测值；()y k 为系统输出量的第k 次真值，()y k i -为系统输出量的第k i -次真值；()u k 为系统的第k 个输入值，()u k i -为 系统的第k i -个输入值；()v k 为均值为0的随机噪声。
众创空间建设运营方案 根据《云南省人民政府关于进一步做好新形势下就业创业工作的实施意见》（云政发〔2015〕53号），云南省人力资源和社会保障厅、云南省财政厅下发的《关于做好2015年度创业园区众创空间校园创业平台申报认定有关工作的通知》(云人社发〔2015〕300号)、楚雄州人力资源和社会保障局《关于做好创业园区、众创空间及校园创业平台申报认定有关工作的通知》等文件，为响应元谋县创新驱动发展战略，推动“大众创业、万众创新”的浪潮，帮助元谋县青年创业者实现创业梦想，xxxx公司在元谋县人力资源和社会保障局的支持和指导下，依托云南元谋现代种业科技园，打造xxx众创空间，形成政府激励创业创新、社会支持创业创新、劳动者勇于创业创新的新局面，结合实际，特制定本实施方案。 一、建设的重要意义 众创空间是向小微创新企业和个人创业者的低成本、便利化、全要素的开放式综合服务平台，为广大创新创业者提供良好的工作空间、网络空间、社交空间和资源共享空间。大力发展众创空间是创新驱动的最佳体现、转型升级的重要 1
抓手、应对开放式创新最好的举措。 近年来，元谋县围绕“高原特色现代农业”，“区域性南繁种业基地建设”发展战略，不断优化我县绿色产业结构，随着绿色产业经济发展步伐迅速加快，经济发展主体的多元化需求不断增加，一批企业家主体（包括企业中层管理、营销、科技人员）、外出务工经商人员、在校大学生和毕业生、农村致富带头人的创业热情不断高涨，设立元谋现代种业科技众创空间的各项要素已经完全具备。但是创业初始阶段普遍存在规模偏小、布局分散、产业层次低、融资难、应对风险能力弱等问题。 为解决创业主体创业中存在的热点难点问题，通过政府引导、市场运作、政策支持等措施，建立元谋现代种业科技众创空间，为广大创业者开辟一片“试验田”，起到积极的示范作用和龙头带动作用，引导广大创业者走合法、优质、高效的创业道路，储备一批成长性中小企业，培育一批规模创新企业，为我县经济发展提供后续动力，对提升县域经济发展水平和促进民营经济快速发展具有重要意义。 二、建设的指导思想、组织架构和工作目标 （一）指导思想和整体思路 指导思想是探索创新创业企业做大做强的新途径。通过 2
浅析电力系统模型参数辨识 （贵哥提供） 一、现状分析 随着我国电力事业的迅猛发展, 超高压输电线路和大容量机组的相继投入, 对电力系统稳定计算、以及其安全性、经济性和电能质量提出了更高的要求。现代控制理论、计算机技术、现代应用数学等新理论、新方法在电力系统的应用，正在促使电力工业这一传统产业迅速走向高科技化。 我国大区域电网的互联使网络结构更复杂，对电力系统安全稳定分析提出了更高的要求，在线、实时、精确的辨识电力系统模型参数变得更加紧迫。由于电力系统模型的基础性、重要性，国外早在上世纪三十年代就开始了这方面的分析研究，[1,2]国内外的电力工作者在模型参数辨识方面做了大量的研究工作。[3]随后IEEE相继公布了有关四大参数的数学模型。1990年全国电网会议上的调查确定了模型参数的地位，促进了模型参数辨识的进一步发展，并提出了研究发电机、励磁、调速系统、负荷等元件的动态特性和理论模型，以及元件在极端运行环境下的动态特性和参数辨识的要求。但传统的测量手段，限制了在线实时辨识方法的实现。 同步相量测量技术的出现和WAMS系统的研究与应用，使实现在线实时的电力系统模型参数辨识成为可能。同步相量是以标准时间信号GPS作为同步的基准，通过对采样数据计算而得的相量。相量测量装置是进行同步相量测量和输出以及动态记录的装置。PMU的核心特征包括基于标准时钟信号的同步相量测量、失去标准时钟信号的授时能力、PMU与主站之间能够实时通信并遵循有关通信协议。 自1988年Virginia Tech研制出首个PMU装置以来，[4]PMU技术取得了长足发展，并在国内外得到了广泛应用。截至2006年底，在我国范围内，已有300多台P MU装置投入运行，并且可预计，在不久的将来PMU装置会遍布电力系统的各个主要电厂和变电站。这为基于PMU的各种应用提供了良好的条件。 二、系统辨识的概念 系统模型是实际系统本质的简化描述。[5]模型可分为物理模型和数学模型两大类。物理模型是根据相似原理构成的一种物理模拟，通过模型试验来研究系统的
众创空间实施方案
众创空间建设 一、人才引进 众创空间设有科技咨询部、信息检索部、创新发展部、财务部、电子商务部及综合办公室等六个部室，现有各方面专兼职人员26名，并积极与省内及全国研究机构、科研院所、知名大学、检测机构、融资机构联系，建立博士专家导师服务工作站，经过引进高端人才，聘请成功创业企业家，建立“联络员、辅导员、博士专家工作站”组成的服务创业导师团队，打造扩展服务范围，重点服务于我州各中小企业及创业大学生，为创新创业提供有力的技术保障。
二、服务支持 1、基础服务、众创空间 向入驻的中小企业及创业者提供生活、办公空间、创业咖啡、学术交流、研究、转化的必要设施和服务，以零收费的方式为初创者提供工作、社交和资源共享空间，为初创者搭建了低成本、便利化、全要素、开放式的新型创业平台。 推动大众创业、万众创新。实现创新与创业相结合、线上与线下相结合、孵化与投资相结合，为创业者提供良好的工作空间、网络空间、社交空间和资源共享空间。 在众创空间内规划了400平米进行众创空间的建设，以零收费的方式为初创者提供工作、社交和资源共享空间，为初创者搭建了低成本（利用现有资源与条件，盘活存量设施和场地，提供低成本创业场所）、便利化（交通便利，创业者集聚，创新创业资源相对汇集地区，创业手续简便）、全要素（能够提供创新创业要素的全方位供给，构建社交化创业平台）、开放式（整合利用全球创新创业资源，为创业者提供开源软硬件、开放式办公空
间）的新型创业平台。提供社交和资源共享空间,同时将定期邀请成功的企业家和科研院所的专家进行创业指导，方便创业者交流，促使其共同创业。 2、信息服务部 根据各创新企业的需要，建设信息化平台、及时发布国家、省市有关政策及企业、人才等信息，为企业提供畅通的信息渠道和网上交流平台而且能为企业做宣传推广，促进信息交流和资源共享。协助各企业做好信息化事务的报批、备案、注册。 3、产业服务部 不断深化专业服务，学习并联系省内致命众创空间，为提供专业服务能力，建设新能源科技公共服务平台，为新能源领域的企业提供公共技术服务。着力打造具有自主知识产权的创新型企业，鼓励企业自主创新并进行成果转化、产业化中试等创业服务。帮助初创企业创新、创业克服发展过程中的一系列问题，提升企业的竞争力与成功率，根据企业发展各阶段的不同特点及不同需求，全面推进企业创办、政策对接、项目申报等完善实用的服务平台。 4、知识产权、项目服务部 协助企业申报、挖掘实用新型专利、创造专利、外观专利；组织企业申报国家、省、市和平度市的各级各类项目计划；组织企业参加各类项目对接，促进企业与高校和科研究所的合作；为企
互联网+众创空间实施方案
目录 一、众创空间总体要求 二、众创空间重点任务 （一）众创空间建设行动 （二）创业主体培育行动 （三）创业企业孵育行动 （四）创业投融资促进行动（五）创业服务提升行动 （六）创业文化营造行动三、众创空间支持政策 （一）降低市场准入门槛 （二）降低创业成本 四、众创空间保障措施 （一）强化统筹协调 （二）开展先行先试 （三）营造良好氛围
一、总体要求 （一）推进思路 为贯彻落实国家、省和市委、市政府的统一部署，大力实施“创业创新”行动，加强顶层设计，统筹协调联动，分工推进落实，集成政策支持，营造良好环境，使各类创业主体各显其能、各展其才，最大限度地激发全民创业潜力、释放创业活力；大力发展新技术、新产品、新业态、新模式，培育新的经济增长点，以创业促创新，以创业促就业，以创业促发展，为深入实施创新驱动发展战略提供新动能。 （二）实施原则 坚持市场导向，转变政府职能。充分发挥市场在资源配置中的决定性作用，以社会力量为主构建市场化的众创空间，以满足个性化、多样化消费需求和开放式、体验式创新为重点，加强协调联动和政策集成，促进创新创意与市场需求和社会资本有效对接。 创新服务模式，促进开放共享。通过市场化机制、专业化服务和资本化途径，有效集成创业服务资源，提供低成本、便利化、全要素的增值服务。充分运用互联网和开源技术构建开放创新创业平台，加强技术转移，整合利用全球创新资源，加强产学研合作，促进科技资源开放共享。 强化科技支撑，激发创业活力。发挥科技创新支撑作用，运用互联网、大数据、云计算等现代信息技术，促进创新创业要素在更大范围内高效组合、优化配置，降低创业成本，整合各类社会资源和科技资源协同支持创新创业，依靠大众创新创业推进转型升级。
基于最小二乘模型的Bayes 参数辨识方法 王晓侃1，冯冬青2 1 郑州大学电气工程学院，郑州（450001） 2 郑州大学信息控制研究所，郑州（450001） E-mail ：wxkbbg@https://www.doczj.com/doc/226457531.html, 摘 要：从辨识定义出发,首先介绍了Bayes 基本原理及其两种常用的方法,接着重点介绍了基于最小二乘模型的Bayes 参数辨识,最后以实例用MATLAB 进行仿真,得出理想的辨识结果。 关键词:辨识定义；Bayes 基本原理；Bayes 参数辨识 中国图书分类号：TP273+.1 文献标识码：A 0 概述 系统辨识是建模的一种方法。不同的学科领域，对应着不同的数学模型，从某种意义上讲，不同学科的发展过程就是建立它的数学模型的过程。建立数学模型有两种方法:即解析法和系统辨识。L. A. Zadehll 于1962年曾对”辨识”给出定义[1]:系统辨识是在对输入和输出观测的基础上，在指定的一类系统中，确定一个与被识别的系统等价的系统。一般系统输出y(n)通常用系统过去输出y(n-m)和现在输入u(n)及过去输入u(n-m)的函数描述 y(n)=f(y(n-1),y(n-2)，...，y(n-m y ), u(n),u(n-1),... ,u(n-m u ))=f(x(n),n) x(n)=[y(n-1),y(n-2),...y(n-m y ), u(n),u(n-1),...,u(n-m u )]’ 这里f(,)为未知函数关系，一般情况为泛函数，可以是线性函数或非线性函数，分别对应于线性或非线性系统，通常这个函数未知，但是局部输入输出数据可以测出，系统辨识的任务就是根据这部分信息寻找确定函数或确定系统来逼近这个未知函数。但实际上我们不可能找到一个与实际系统完全等价的模型。从实用的角度来看，系统辨识就是从一组模型中选择一个模型，按照某种准则，使之能最好地拟合由系统的输入输出观测数据体现出的实际系统的动态或静态特性。接下来本文就以最小二乘法为基础的Bayes 辨识方法为例进行分析介绍并加以仿真[4]。 1 Bayes 基本原理 Bayes 辨识方法的基本思想是把所要估计的参数看做随机变量,然后设法通过观测与该参数有关联的其他变量,以此来推断这个参数。 设μ是描述某一动态系统的模型，θ是模型μ的参数，它会反映在该动态系统的输入输出观测值中。如果系统的输出变量z(k)在参数θ及其历史纪录(1) k D ?条件下的概率密度函 数是已知的，记作p(z(k)｜θ，(1) k D ?)，其中(1) k D ?表示（k-1）时刻以前的输入输出数据集 合，那么根据Bayes 的观点参数θ的估计问题可以看成是把参数θ当作具有某种先验概率密 度p （θ，(1) k D ?）的随机变量，如果输入u(k)是确定的变量，则利用Bayes 公式，把参数θ 的后验概率密度函数表示成[2] p (θ，k D ）= p (θ｜z (k ),u(k ), (1) k D ?)=p (θ｜z (k ),(1) k D ?) = (k-1) (k-1) p(z(k)/,D )p(/D ) (k-1)(k-1)p(z(k)/,D )p(/D )d θθθθθ∞∫?∞ (1) 在式(1)中,参数θ的先验概率密度函数p(θ｜(1) k D ?)及数据的条件概率密度函数p(z(k)｜θ，
ISSN 1000-0054CN 11-2223/N 清华大学学报(自然科学版)J T singh ua Un iv (Sci &Tech ),1999年第39卷第3期 1999,V o l.39,N o.311/34 37～40 负荷建模和参数辨识的遗传进化算法* 朱守真, 沈善德, 郑宇辉, 李 力, 艾 芊, 曲祖义 清华大学电机工程与应用电子技术系,北京100084; 东北电力集团公司,沈阳110006 收稿日期:1998-06-23 第一作者:女,1950年生,副教授 *基金项目:国家攀登计划B(85-35) 文 摘 提出了一种用于电力系统负荷建模和参数辨识的遗传进化算法,该方法与传统的最小二乘法相比具有全局搜索优化特点,适用于非线性、不连续或微分不连续的各种负荷模型。该方法已成功用于工业负荷实测数据辨识及动态和静态负荷建模。在静态负荷建模上,辨识结果略优于传统的最小二乘法,且通用性更好,只需做极小的修改就可以用于各种形式的静态负荷模型。在动态负荷建模上算法不仅给出了更优秀的结果,而且表现出很好的稳健性。结果表明此方法在负荷建模中的优势。 关键词 遗传进化算法;负荷建模;参数辨识分类号 T M 761 电力负荷模型是电力系统分析、规划、运行和计算的基础,尤其在计算中对电力系统动态行为的模拟结果影响很大。不同的计算需要采用不同的负荷模型,常规采用以不同比例的恒定阻抗、恒定电流、恒定功率或考虑不同动静比例负荷模型的方式使计算结果相差很大,甚至会导致完全错误的结论[1,2]。研究表明建立符合实际的负荷模型是十分必要的。负荷特性具有时变、非线形、不确定等多种特点,且实际负荷的用电设备构成差别很大,尤其是当电压或电流变化时,负荷产生突变,这也增加了建模的难度和复杂性。参数辨识是负荷建模的核心,目前常用的有最小二乘法、辅助变量法、分段线性多项式等方法,其中传统的方法不能有效地克服负荷建模中的非线性和不连续性等问题,会产生多值性等误差。近年来ANN 方法在建模方面已取得成功,但该方法更侧重于模拟模型的动态过程,且形成的结果是非参数模型。 遗传进化算法是模拟自然界进化中优胜劣汰的 优化过程,原则上能以较大的概率找到全局的最优解,具有并行、通用、鲁棒性强,全局收敛性好等优 点。研究人员已在发电规划[3],发电调度[4],无功优化[5]中用算例证明了EP 方法比传统的梯度寻优技术更优越。 本文采用遗传进化算法对静态、动态负荷进行了实测建模。 1 电力负荷的数学模型 本文主要描述以负荷特性来分类的静态和动态模型的建模方法。1.1 静态负荷模型 静态负荷模型表示某一时刻负荷所吸收的有功功率和无功功率与同一时刻负荷母线电压和频率之间的函数关系。静态负荷模型一般以幂函数和多项式模型表示。 本文以幂函数模型为例进行计算,幂函数表示的静态负荷特性如下: P =P 0U a 1f a 2, Q =Q 0 U b 1 f b 2 . (1) 定义误差函数 E w = N i =1 [W m (i )-W c (i )] 2 N (2)式中:N 为测量点数,W m (i )分别表示第i 次有功或无功功率测量值,W c (i )表示利用第i 次采样U i ,f i 的值由式(1)得到的有功或无功计算值,X p 、X q 是待辨识参数的向量: X p =[P 0,a 1,a 2], X q =[Q 0,b 1,b 2]. (3) 辨识问题表述为极小值寻优问题,即搜索一组参数使误差E w 达到最小值。1.2 动态负荷的模型 动态负荷模型表示某一时刻负荷所吸收的有功
机器人动力学研究的典型方法和应用 （燕山大学 机械工程学院） 摘 要：本文介绍了动力学分析的基础知识，总结了机器人动力学分析过程中比较常用的动力学分析的方法：牛顿—欧拉法、拉格朗日法、凯恩法、虚功原理法、微分几何原理法、旋量对偶数法、高斯方法等，并且介绍了各个方法的特点。并通过对PTl300型码垛机器人弹簧平衡机构动力学方法研究，详细分析了各个研究方法的优越性和方法的选择。 前 言：机器人动力学的目的是多方面的。机器人动力学主要是研究机器人机构的动力学。机器人机构包括机械结构和驱动装置，它是机器人的本体，也是机器人实现各种功能运动和操作任务的执行机构，同时也是机器人系统中被控制的对象。目前用计算机辅助方法建立和求解机器人机构的动力学模型是研究机器人动力学的主要方法。动力学研究的主要途径是建立和求解机器人的动力学模型。所谓动力学模指的是一组动力学方程（运动微分方程），把这样的模型作为研究力学和模拟运动的有效工具。 报告正文： （1）机器人动力学研究的方法 1）牛顿—欧拉法 应用牛顿—欧拉法来建立机器人机构的动力学方程，是指对质心的运动和转动分别用牛顿方程和欧拉方程。把机器人每个连杆（或称构件）看做一个刚体。如果已知连杆的表征质量分布和质心位置的惯量张量，那么，为了使连杆运动，必须使其加速或减速，这时所需的力和力矩是期望加速度和连杆质量及其分布的函数。牛顿—欧拉方程就表明力、力矩、惯性和加速度之间的相互关系。 若刚体的质量为m ，为使质心得到加速度a 所必须的作用在质心的力为F ，则按牛顿方程有：ma F = 为使刚体得到角速度ω、角加速度εω= 的转动，必须在刚体上作用一力矩M ， 则按欧拉方程有：εωI I M += 式中，F 、a 、M 、ω、ε都是三维矢量；I 为刚体相对于原点通过质心并与刚
众创空间建设方案最新内容 为贯彻落实党的十八届三中、四中全会提出的“大众创业，万众创新”的“众创空间”战略，为更好地加快我市民营经济发展，着力解决我市民营经济发展中的突出问题，促进我市民营经 济持续健康快速发展，激发全民创新创业热情，实现我市十三五“激活存量、扩大增量、调优结构、培养龙头、做精产品、延长 链条、经济指标实现翻番增长”的奋斗目标，按照总体要求，结 合我市实际，特制定建设如下方案，请领导审核。 一、建设众创空间的重要意义 近年来，围绕“三三”发展战略、“六大发展”发展重点，不断进行产业结构调整与升级，随着民营经济发展步伐迅速加 快，经济发展主体的多元化需求不断增加，一批企业家主体（包 括企业中层管理、营销、科技人员）、外出务工经 商人员、在校大学生和毕业生、农村致富带头人的创业热情不断高涨，等等，设立综合创业孵化与实训基地的各项要素已经完全具备。但是创业初始阶段普遍存在规模偏小、布局分散、产业层次低、用地难、融资难、应对风险能力弱等问题。为解决创业主体创业中存在的热点难点问题，通过政府引导、市场运作、政策支持等措施，建立我市综合创业孵化与实训基地，为广大创业者开辟一片“试验田”，起到积极的示范作用和龙头带动作用，引导广大创业者走合法、优质、高效的创业道路，储备一批成长性中小企业，培育一批
规模创新企业，为我市经济发展提供后续动力，对提升我市经济发展水平和促进民营经济快速发展具有重要意义。 二、指导思想、组织机构与工作目标 （一一）指导思想和整体思路 指导思想是探索创新创业企业做大做强的新途径。通过激发民众、大学生和企业高科技人才为主的各类创业者的创业热情、提升创业能力，以市专利转化促进会为依托，建设创业实训众创空间，孵化一批自主创业实体，以点带面推进我市“创业富民、创新强市”的新型战略和创业型城市创建工作以及民营经济的快速发展。 整体思路是以建设创新创业孵化器为突破，夯实科技发展基础；以增强科技孵化能力为重点，打造“大众创业服务、万众创新服务和科技成果转化服务”的“众创空间”服务平台;以市场为导向，采用现代企业和科技管理运营模式，充分利用社会及民间资源，强化与大专院校、科研部门的技术联合，为广大创新创业人员提供良好的工作空间、网络空间、社交空间和资源空间，以创业促进就业，孵化培育一大批创新型小微企业，形成新的产业业态，为建设创新创业型潞城提供科技支撑和新的经济增长点。 （二）组织机构 建议成立由科技X牵头，财政、经信、中小企业X等部门参加的创业众创空间建设工作领导小组，负责统筹开展众
上海交通大学 硕士学位论文 Bouc-Wen滞回模型的参数辨识及其在电梯振动建模中的应用 姓名：周传勇 申请学位级别：硕士 专业：机械设计及理论 指导教师：李鸿光 20080201
Bouc-Wen滞回模型的参数辨识 及其在电梯振动建模中的应用 摘 要 电梯导靴是连接轿箱系统与导轨的装置，它能起到导向和隔振减振的作用。同时，在电梯的运行过程中它又将导轨由于制造或安装所造成的表面不平顺度传递给轿箱系统，从而引起轿箱系统的水平振动。国内外学者在电梯水平振动的建模和分析中，往往把导靴视为线性弹簧-阻尼元件来建模而忽略了非线性因素。事实上导靴与导轨之间存在非线性的迟滞摩擦力，本文通过实验的方法，采用Bouc-Wen 滞回模型来建立导靴-导轨非线性摩擦力模型。 Bouc-Wen滞回模型因其微分形式的非线性表达式而使得其参数辨识存在较大的困难，本文利用模型中部分参数的不敏感性，通过数学变换将非线性参数辨识问题转化为线性参数辨识问题，从而使得问题大大简化，参数辨识的效果也能满足要求。 基于以上导靴-导轨间摩擦力模型，本文进而建立了轿箱-导轨耦合水平振动动力学模型，该模型将轿箱系统等效为2自由度的平面运动刚体，将导靴等效为质量-弹簧-阻尼单元，同时考虑了导靴-导轨间的非线性摩擦力，以及导靴靴衬与导轨间接触的不连续性等。 在建立了轿箱-导轨耦合水平振动动力学模型后，利用Matlab/Simulink，建立了相应的仿真模型，开展了几种典型导轨不
平顺度激励（弯曲、失调和台阶）下的仿真分析。研究结果表明，这些分析对于电梯结构优化设计和动力学建模与分析有理论指导意义。 关键词：迟滞，参数辨识，非线性，动力学建模，系统仿真
众创空间建设工作方案 众创空间建设工作方案是怎么样的呢?今天我们一起看看吧! 为贯彻落实省委办公厅、省政府办公厅《关于印发〈发展众创空间推进大众创新创业实施方案(2015-2020 年)〉的通知》(苏办发〔2015 〕34 号)精神，深入实施“创业江苏”行动，大力推进众创空间建设，激发全社会创新创业活力，营造良好创新创业生态环境，特制订本工作方案。 一、工作思路 深入实施“创业江苏”行动，通过上下联动，集成政策支持，建设一批众创空间等新型创业服务平台;通过市场化机制、专业化服务和资本化途径，有效集成创业服务资源，打造众创空间、孵化器、加速器、科技园区，形成点、线、面相结合的创新创业孵化服务链条;探索建设众创集聚区，提升创新创业服务能力。 二、工作目标
通过省地联动，形成推进众创空间建设的协同机制。全省建设一批纳入省级以上科技企业孵化器管理的众创空间、一批省级以上科技创业孵化链条和一批众创集聚区， 孵化培育一批创新型企业，推动人才、技术、资本等创新要素向江苏集聚，加快形成大众创业、万众创新的生动局面。 三、重点任务 （一）加快众创空间建设步伐。充分发挥市场配置资源的决定性作用，鼓励行业领军企业、国有大中型企业、高校、科研机构、投资机构、行业组织等社会力量投资建设或管理运营创客空间、创业咖啡、创新工场等新型孵化载体，鼓励引进国际国内知名创客孵化培育管理模式，打造一批低成本、便利化、全要素、开放式的众创空间。各市、高新区要充分利用老旧厂房、闲置房屋、商业设施等资源进行整合和改造提升，为众创空间提供免费或低租金的场地。现有科技企业孵化器和大学科技园，要利用资源优势和孵化经验，通过新建或改造，发展一批众创空间。推进“互联网+ ”与传统创业载体融合，发展“线上虚拟空间与“线下实体空间”相结合的新型众创平台，通过线上线下相结合，为“创客”群体拓展创业空间。 （二）开展科技创业孵化链条试点。支持有条件的孵化器开
参数辨识 参数辨识的步骤 飞行器气动参数辨识是一个系统工程，包括四部分：①试验设计，使试验能为辨识提供含有足够信息量且信息分布均匀的试验数据；②气动模型结果确定，即从候选模型集中，根据一定的准则和经验，选出最优的气动模型构式；③气动参数辨识，根据辨识准则和数据求取模型中待定参数，这是气动辨识定量研究的核心阶段；④模型检验，确认所得气动模型是否确实反映了飞行器动力学系统中气动力的本质属性。这四个部分环环相扣，缺一不可，要反复进行，直到对所得气动模型满意为止。 参数辨识的方法 参数辨识方法主要有最小二乘算法、极大似然法、集员辨识法、贝叶斯法、岭估计法、超椭球法和鲁棒辨识法等多种辨识方法。虽然目前参数辨识的领域己经发展了多种算法，但是用于气动参数估计的算法主要有：极大似然法(ML)，广义Kalman滤波(EKF)法，模型估计法(EBM )、分割及多分割算法(PIA及MPIA)、最小二乘法，微分动态规划法等。 因为最小二乘法和极大似然法是两种经典的算法，目前己经发展得相当成熟。最小二乘法适于线性模型的参数辨识，可以用于飞行器系统辨识中很多的线性模型，如惯性仪表误差系数的辨识，线性时变离散系统初始状态的辨识及多项式曲线拟合等。目前最小二乘法已经广泛应用于工程实际中。而极大似然算法因其具有渐进一致性、估计的无偏性、良好的收敛特性等特点而被广泛应用于飞行器参数辨识领域。 最小二乘法大约是1975年高斯在其著名的星体运动轨道预报研究工作中提出来的。后来，最小二乘法就成了估计理论的奠基石。由于最小二乘法原理简单，编程容易，所以它颇受人们重视，应用相当广泛。 极大似然估计算法在实践中不断地被加以改进，这种改进主要表现在三个方
基于最小二乘法的系统参数辨识 研究生二队李英杰 082068 摘要：系统辨识是自动控制学科的一个重要分支，由于其特殊作用，已经广泛应用于各种领域，尤其是复杂系统或参数不容易确定的系统的建模。过去，系统辨识主要用于线性系统的建模，经过多年的研究，已经形成成熟的理论。但随着社会、科学的发展，非线性系统越来越受到人们的关注，其控制与模型之间的矛盾越来越明显，因而非线性系统的辨识问题也越来越受到重视，其辨识理论不断发展和完善本。文重点介绍了系统参数辨识中最小二乘法的基本原理，并通过热敏电阻阻值温度关系模型的辨识实例，具体说明了基于最小二乘法参数辨识在Matlab中的实现方法。结果表明基于最小二乘法具有算法简单、精度较高等优点。 1. 引言 所谓辨识就是通过测取研究对象在人为输入作用下的输出响应，或正常运行时的输入输出数据记录，加以必要的数据处理和数学计算，估计出对象的数学模型。这是因为对象的动态特性被认为必然表现在它的变化着的输入输出数据之中，辨识只不过是利用数学的方法从数据序列中提炼出对象的数学模型而已[1]。最小二乘法是系统参数辨识中最基本最常用的方法。最小二乘法因其算法简单、理论成熟和通用性强而广泛应用于系统参数辨识中。本文基于热敏电阻阻值与温度关系数据，介绍了最小二乘法的参数辨识在Matlab中的实现。 2. 系统辨识 一般而言，建立系统的数学模型有两种方法：激励分析法和系统辨识法。前者是按照系统所遵循的物化（或社会、经济等）规律分析推导出模型。后者则是从实际系统运行和实验数据处理获得模型。如图1 所示，系统辨识就是从系统的输入输出数据测算系统数学模型的理论和方法。更进一步的定义是L.A.Zadeh 曾经与1962 年给出的，即“系统辨识是在输入和输出的基础上，从系统的一类系统范围内，确立一个与所实验系统等价的系统”。另外，系统辨识还应该具有3 个基本要素，即模型类、数据和准则[5]。被辨识系统模型根据模型形式可分为参数模型和非参数模型两大类。所谓参数模型是指微分方程、差分方程、状态方程等形式的数学模型；而非参数模型是指频率响应、脉冲响应、传递函数等隐含参数的数学模型。在辨识工程中，模型的确定主要根据经验对实际对象的特性进行一定程度上的假设，如对象的模型是线性的还是非线性的、是参数模型还是非参数模型等。在模型确定之后，就可以根据对象的输入输出数据，按照一定的辨识算法确定模型的参数[4]。 图1 被研究的动态系统 3. 最小二乘法（LS）参数估计方法 对于参数模型辨识结构，系统辨识的任务是参数估计，即利用输入输出数据估计这些参数，建立系统的数学模型。在参数估计中最常用的是最小二乘法(LS)、
众创空间运营方案 一、 运营目标 方正智谷创客空间的运营，主要以达成以下效果为目标： （一） 众创空间由备案状态升级为获认定的众创空间 （二） 提升方正产业园的形象和品牌知名度 （三） 服务园内客户，加强与客户的联系，为客户提供有价值的服务 二、 关键衡量指标 按照《苏州工业园区关于发展众创空间推动大众创新创业的实施意见》的相关规定，一个成熟的众创空间应该具有以下几个因素： （一） 孵化场地，为初创团队免费提供 （二） 孵化基金，可以自己出资设立，也可以与投资机构合作 （三） 创业导师，主要是四类人士：投资机构负责人、高校教授、某一领 域专家、知名公司副总以上或创业成功的企业家 （四） 创业项目，至少3-5个，并且每隔一段时间要有所增长，以我们的备 案时间计算，目前需要10个以上的创业项目 （五） 第三方服务机构，可以为企业提供所需的全方位、一站式服务 （六） 沙龙/培训活动，面向创业者免费提供，常规化举办 三、 三大板块 针对众创空间的三大目标，可以将工作大致分为三大板块：即项目板块、活动版块和服务板块，每一个板块之间既相互独立，又互相融合。其关系如下图所示：
其中，活动版块以活动的策划、组织和宣传为主，对应众创空间的品牌目标，同时也是众创空间为各个客户和项目团队提供的主要服务。活动的举办次数是众创空间绩效考核的重要内容之一。目前举办活动的主要方式是通过与合作服务商联合举办的方式，但效果一般。以后可以多参加其他孵化器的活动，借鉴吸收其经验，将活动效果较好的分享者引进为我们的合作服务商，使我们的活动越来越活跃，越来越有价值。 项目板块是衡量众创空间运营情况的核心指标，目前我们已经对产业园内的5个项目进行了包装，但是目前有些工作还待完善，尚未进入园区路演环节。项目的来源有以下几种途径：1.在产业园内项目进行挖掘和包装，2.从产业园外进行寻找和引进，3.通过产业园内客户介绍。 服务板块包括工商注册、代税代账、融资、政策申报等内容，既是众创空间为企业提供的全方位、一站式服务的内涵，同时也是产业园为客户提供的增值服务的一部分。做好了这一块，将有效提升客户对我们的好感度和好评度。我们要不断扩充相关领域的合作服务商的数量，同时也要积极介入，学习掌握相关知识（比如政策申报的流程、条件等）。 四、具体方案 众创空间每个运营板块既互相独立，又相互融合，具体方案如下： （一）项目板块 项目板块以项目的引进和包装为主线，与服务板块相关联。
文章编号：1006-1576（2008）11-0079-04 基于动力学模型的轮式移动机器人运动控制 张洪宇，张鹏程，刘春明，宋金泽 （国防科技大学机电工程与自动化学院，湖南长沙 410073） 摘要：目前，对不确定非完整动力学系统进行设计的主要方法有自适应控制、预测控制、最优控制、智能控制等。结合WMR动力学建模理论的研究成果，对基于动力学模型的WMR运动控制器的设计和研究进展进行综述，并分析今后的重点研究方向。 关键词：轮式移动机器人；动力学模型；运动控制；非完整系统 中图分类号：TP242.6; TP273 文献标识码：A Move Control of Wheeled Mobile Robot Based on Dynamic Model ZHANG Hong-yu, ZHANG Peng-cheng, LIU Chun-ming, SONG Jin-ze (College of Electromechanical Engineering & Automation, National University of Defense Technology, Changsha 410073, China) Abstract: At present, methods of non-integrity dynamic systems design mainly include adaptive control, predictive control, optimal control, intelligence control and so on. Based on analyzing the recent results in modeling of WMR dynamics, a survey on motion control of WMR based on dynamic models was given. In addition, future research directions on related topics were also discussed. Keywords: Wheeled mobile robot; Dynamic model; Motion control; Non-integrity system 0 引言 随着生产的发展和科学技术的进步，移动机器人系统在工业、建筑、交通等实际领域具有越来越广泛的应用和需求。进入21世纪，随着移动机器人应用需求的扩大，其应用领域已从结构化的室内环境扩展到海洋、空间和极地、火山等环境。较之固定式机械手，移动机器人具有更广阔的运动空间，更强的灵活性。移动机器人的研究必须解决一系列问题，包括环境感知与建模、实时定位、路径规划、运动控制等，而其中运动控制又是移动机器人系统研究中的关键问题。故结合WMR动力学建模理论的研究成果，对基于动力学模型的WMR运动控制器设计理论和方法的研究进展进行研究。 1 WMR动力学建模 有关WMR早期的研究文献通常针对WMR的运动学模型。但对于高性能的WMR运动控制器设计，仅考虑运动学模型是不够的。文献[1]提出了带有动力小脚轮冗余驱动的移动机器人动力学建模方法，以及WMR接触稳定性问题和稳定接触条件。文献[2]提出一种新的WMR运动学建模的方法，这种方法是基于不平的地面，从每个轮子的雅可比矩阵中推出一个简洁的方程，在这新的方程中给出了车结构参数的物理概念，这样更容易写出从车到接触点的转换方程。文献[3]介绍了与机器人动作相关的每个轮子的雅可比矩阵，与旋转运动的等式合并得出每个轮子的运动方程。文献[4]基于LuGre干摩擦模型和轮胎动力学提出一种三维动力学轮胎/道路摩擦模型，不但考虑了轮胎的径向运动，同时也考虑了扰动和阻尼摩擦下动力学模型，模型不但可以应用在轮胎/道路情况下，也可应用在对车体控制中。在样例中校准模型参数和证实了模型，并用于广泛应用的“magic formula”中，这样更容易估计摩擦力。在文献[5]中同时考虑运动学和动力学约束，其中提出新的计算轮胎横向力方法，并证实了这种轮胎估计的方法比线性化的轮胎模型好，用非线性模型来模拟汽车和受力计算，建立差动驱动移动机器人模型，模型本身可以当作运动控制器。 2 WMR运动控制器设计的主要发展趋势 在WMR控制器设计中，文献[6]给出了全面的分析，WMR的反馈控制根据控制目标的不同，可以大致分为3类：轨迹跟踪（Trajectory tracking）、路径跟随（Path following）、点镇定（Point stabilization）。轨迹跟踪问题指在惯性坐标系中，机器人从给定的初始状态出发，到达并跟随给定的参考轨迹。路径跟随问题是指在惯性坐标系中，机器人从给定的初始状态出发，到达并跟随指定的几何 收稿日期：2008-05-19；修回日期：2008-07-16 作者简介：张洪宇（1978-）男，国防科学技术大学在读硕士生，从事模式识别与智能系统研究。 ，
模态参数辨识方法综述 摘要：本文对模态分析和模态参数识别进行了综述，对当前识别方法的原理、识别精度及适用条件进行阐述和比较，提出环境激励下模态参数识别方法需解决的关键问题及模态分析在缺陷检测和结构优化中作用。 关键词：模态分析模态参数识别模态分析与缺陷检测结构工作模态 0引言 模态分析是将线性时不变系统振动微分方程组中的物理坐标变换为模态坐标，使方程组解耦，成为一组以模态坐标及模态参数描述的独立方程，坐标变换的变换矩阵为振型矩阵，其每列即为各阶振型。模态是机械结构的固有振动特性，每一个模态具有特定的固有频率、阻尼比和模态振型。这些模态参数可以由计算或试验分析取得，这样一个计算或试验分析过程称为模态分析。振动模态是弹性结构固有的、整体的特性。如果通过模态分析方法搞清楚了结构物在某一易受影响的频率范围内，各阶主要模态的特性，就可能预知结构在此频段内，在外部或内部各种振源作用下实际振动响应，而且一旦通过模态分析知道模态参数并给予验证，就可以把这些参数用于（重）设计过程，优化系统动态特性，或者研究把该结构连接到其他结构上时所产生的影响。模态分析的最终目标是识别出系统的模态参数，为结构系统的振动分析、振动故障诊断和预报、结构动力特性的优化设计提供依据。 解析模态分析可用有限元计算实现，而实验模态分析则是对结构进行可测可控的动力学激励，由激振力和响应的信号求得系统的频响函数矩阵，再在频域或转到时域采用多种识别方法求出模态参数，得到结构固有的动态特性，这些特性包括固有频率、振型和阻尼比等。有限元法是当前分析机械结构模态的主要方法，很多学者研究了单裂缝和多裂缝缺陷对不同结构动态特性的影响，但这些研究仅局限于出现缺陷结构的当前状态，考虑到缺陷在机械结构使用过程中的扩展，提出了模态分析与缺陷扩展理论相结合的方法分析缺陷的发展趋势，便于机械结构剩余寿命的评估，使已达到设计寿命的结构在失效前仍然发挥其功能，节约了经济成本。 一般模态识别方法是基于实验室条件下的频率响应函数进行的参数识别方法，它要求同时测得结构上的激励和响应信号。但是，在许多工程实际应用中，工作条件和实验室条件相差很大，对一些大型结构无法施加激励或施加激励费用很昂贵，因此要求识别结构在工作条件下的模态参数。工作模态参数识别方法与传统模态参数识别方法相比有如下特点：一、仅
Bouc-Wen模型因数字处理方便简单而得到较为广泛的应用，力可以表示为： 利用遗传算法工具箱（GA）对Bouc-Wen模型进行参数识别。 实验数据来源于对磁流变阻尼器（MR damper）进行性能测试，试验获得的数据包括力F，位移x，采用频率已知，速度和加速度可以由位移求导得出。 参数识别出现程序如下：（文件名：Copy_0_of_BoucWen） function j=myfung(x) y0=[0]; yy=y0; tspan=[]'; s=[]'; v=[]'; Ft=[]'; rr=max(size(s));%计算数据个数 i=1; while (i