Vacuity detection in temporal model checking

The Beginning of Model Checking:A Personal PerspectiveE.Allen Emerson1,21.Department of Computer Sciencesputer Engineering Research CenterThe University of Texas at Austin,Austin TX78712,USAAbstract.Model checking provides an automated method for verify-ing concurrent systems.Correctness specifications are given in tempo-ral logic.The method hinges on an efficient andflexible graph-theoreticreachability algorithm.At the time of its introduction in the early1980’s,the prevailing paradigm for verification was a manual one of proof-theoretic reasoning using formal axioms and inference rules oriented to-wards sequential programs.The need to encompass concurrent programs,the desire to avoid the difficulties with manual deductive proofs,and thesmall model theorem for temporal logic motivated the development ofmodel checking.Keywords:model checking,model-theoretic,synthesis,history,origins1IntroductionIt has long been known that computer software programs,computer hardware designs,and computer systems in general exhibit errors.Working programmers may devote more than half of their time on testing and debugging in order to increase reliability.A great deal of research effort has been and is devoted to developing improved testing methods.Testing successfully identifies many significant errors.Yet,serious errors still afflict many computer systems including systems that are safety critical,mission critical,or economically vital.The US National Institute of Standards and Technology has estimated that programming errors cost the US economy$60B annually[Ni02].Given the incomplete coverage of testing,alternative approaches have been sought.The most promising approach depends on the fact that programs and more generally computer systems may be viewed as mathematical objects with behavior that is in principle well-determined.This makes it possible to specify using mathematical logic what constitutes the intended(correct)behavior.Then one can try to give a formal proof or otherwise establish that the program meets This work was supported in part by National Science Foundation grants CCR-009-8141&CCR-020-5483and funding from Fujitsu Labs of America. email:emerson@ URL:/∼emerson/its specification.This line of study has been active for about four decades now. It is often referred to as formal methods.The verification problem is:Given program M and specification h determine whether or not the behavior of M meets the specification h.Formulated in terms of Turing Machines,the verification problem was considered by Turing[Tu36]. Given a Turing Machine M and the specification h that it should eventually halt (say on blank input tape),one has the halting problem which is algorithmically unsolvable.In a later paper[Tu49]Turing argued for the need to give a(manual) proof of termination using ordinals,thereby presaging work by Floyd[Fl67]and others.The model checking problem is an instance of the verification problem.Model checking provides an automated method for verifying concurrent(nominally)finite state systems that uses an efficient andflexible graph search,to determine whether or not the ongoing behavior described by a temporal property holds of the system’s state graph.The method is algorithmic and often efficient because the system isfinite state,despite reasoning about infinite behavior.If the answer is yes then the system meets its specification.If the answer is no then the system violates its specification;in practice,the model checker can usually produce a counterexample for debugging purposes.At this point it should be emphasized that the verification problem and the model checking problem are mathematical problems.The specification is for-mulated in mathematical logic.The verification problem is distinct from the pleasantness problem[Di89]which concerns having a specification capturing a system that is truly needed and wanted.The pleasantness problem is inherently pre-formal.Nonetheless,it has been found that carefully writing a formal specifi-cation(which may be the conjunction of many sub-specifications)is an excellent way to illuminate the murk associated with the pleasantness problem.At the time of its introduction in the early1980’s,the prevailing paradigm for verification was a manual one of proof-theoretic reasoning using formal axioms and inference rules oriented towards sequential programs.The need to encom-pass concurrent programs,and the desire to avoid the difficulties with manual deductive proofs,motivated the development of model checking.In my experience,constructing proofs was sufficiently difficult that it did seem there ought to be an easier alternative.The alternative was suggested by temporal logic.Temporal logic possessed a nice combination of expressiveness and decidability.It could naturally capture a variety of correctness properties, yet was decidable on account of the“Small”Finite Model Theorem which en-sured that any satisfiable formula was true in somefinite model that was small. It should be stressed that the Small Finite Model Theorem concerns the satisfi-ability problem of propositional temporal logic,i.e.,truth in some state graph. This ultimately lead to model checking,i.e.,truth in a given state graph.The origin and development of model checking will be described below.De-spite being hampered by state explosion,over the past25years model checking has had a substantive impact on program verification efforts.Formal verification2has progressed from discussions of how to manually prove programs correct to the routine,algorithmic,model-theoretic verification of many programs.The remainder of the paper is organized as follows.Historical background is discussed in section2largely related to verification in the Floyd-Hoare paradigm; protocol verification is also considered.Section3describes temporal logic.A very general type of temporal logic,the mu-calculus,that defines correctness in terms offixpoint expressions is described in section4.The origin of model checking is described in section5along with some relevant personal influences on me.A discussion of model checking today is given in section6.Some concluding remarks are made in section7.2Background of Model CheckingAt the time of the introduction of model checking in the early1980’s,axiomatic verification was the prevailing verification paradigm.The orientation of this paradigm was manual proofs of correctness for(deterministic)sequential pro-grams,that nominally started with their input and terminated with their out-put.The work of Floyd[Fl67]established basic principles for proving partial correctness,a type of safety property,as well as termination and total correct-ness,forms of liveness properties.Hoare[Ho69]proposed an axiomatic basis for verification of partial correctness using axioms and inference rules in a formal deductive system.An important advantage of Hoare’s approach is that it was compositional so that the proof a program was obtained from the proofs of its constituent subprograms.The Floyd-Hoare framework was a tremendous success intellectually.It en-gendered great interest among researchers.Relevant notions from logic such as soundness and(relative)completeness as well as compositionality were in-vestigated.Proof systems were proposed for new programming languages and constructs.Examples of proofs of correctness were given for small programs.However,this framework turned out to be of limited use in practice.It did not scale up to“industrial strength”programs,despite its merits.Problems start with the approach being one of manual proof construction.These are formal proofs that can involve the manipulations of extremely long logical formulae. This can be inordinately tedious and error-prone work for a human.In practice, it may be wholly infeasible.Even if strict formal reasoning were used throughout, the plethora of technical detail could be overwhelming.By analogy,consider the task of a human adding100,000decimal numbers of1,000digits each.This is rudimentary in principle,but likely impossible in practice for any human to perform reliably.Similarly,the manual verification of100,000or10,000or even 1,000line programs by hand is not feasible.Transcription errors alone would be prohibitive.Furthermore,substantial ingenuity may also be required on the part of the human to devise suitable assertions for loop invariants.One can attempt to partially automate the process of proof construction using an interactive theorem prover.This can relieve much of the clerical burden.3However,human ingenuity is still required for invariants and various lemmas. Theorem provers may also require an expert operator to be used effectively.Moreover,the proof-theoretic framework is one-sided.It focuses on providing a way to(syntactically)prove correct programs that are genuinely(semantically) correct.If one falters or fails in the laborious process of constructing a proof of a program,what then?Perhaps the program is really correct but one has not been clever enough to prove it so.On the other hand,if the program is really incorrect,the proof systems do not cater for proving incorrectness.Since in practice programs contain bugs in the overwhelming majority of the cases,the inability to identify errors is a serious drawback of the proof-theoretic approach.It seemed there ought to be a better way.It would be suggested by temporal logic as discussed below.Remark.We mention that the term verification is sometimes used in a specific sense meaning to establish correctness,while the term refutation(or falsification) is used meaning to detect an error.More generally,verification refers to the two-sided process of determining whether the system is correct or erroneous.Lastly,we should also mention in this section the important and useful area of protocol work protocols are commonlyfinite state.This makes it possible to do simple graph reachability analysis to determine if a bad state is accessible(cf.[vB78],[Su78]).What was lacking here was aflexible and expres-sive means to specify a richer class of properties.3Temporal LogicModal and temporal logics provided key inspiration for model checking.Origi-nally developed by philosophers,modal logic deals with different modalities of truth,distinguishing between P being true in the present circumstances,pos-sibly P holding under some circumstances,and necessarily P holding under all circumstances.When the circumstances are points in time,we have a modal tense logic or temporal logic.Basic temporal modalities include sometimes P and always P.Several writers including Prior[Pr67]and Burstall[Bu74]suggested that temporal logic might be useful in reasoning about computer programs.For in-stance,Prior suggested that it could be used to describe the“workings of a digital computer”.But it was the seminal paper of Pnueli[Pn77]that made the crit-ical suggestion of using temporal logic for reasoning about ongoing concurrent programs which are often characterized as reactive systems.Reactive systems typically exhibit ideally nonterminating behavior so that they do not conform to the Floyd-Hoare paradigm.They are also typically non-deterministic so that their non-repeatable behavior was not amenable to testing. Their semantics can be given as infinite sequences of computation states(paths) or as computation trees.Examples of reactive systems include microprocessors, operating systems,banking networks,communication protocols,on-board avion-ics systems,automotive electronics,and many modern medical devices.4Pnueli used a temporal logic with basic temporal operators F(sometimes) and G(always);augmented with X(next-time)and U(until)this is today known as LTL(Linear Time Logic).Besides the basic temporal operators applied to propositional arguments,LTL permitted formulae to be built up by forming nestings and boolean combinations of subformulae.For example,G¬(C1∧C2) expresses mutual exclusion of critical sections C1and C2;formula G(T1⇒(T1U C1)specifies that if process1is in its trying region it remains there until it eventually enters its critical section.The advantages of such a logic include a high degree of expressiveness permit-ting the ready capture of a wide range of correctness properties of concurrent programs,and a great deal offlexibility.Pnueli focussed on a proof-theoretic approach,giving a proof in a deductive system for temporal logic of a small example program.Pnueli does sketch a decision procedure for truth overfinite state graphs.However,the complexity would be nonelementary,growing faster than anyfixed composition of exponential functions,as it entails a reduction to S1S,the monadic Second order theory of1Successor,(or SOLLO;see be-low).In his second paper[Pn79]on temporal logic the focus is again on the proof-theoretic approach.I would claim that temporal logic has been a crucial factor in the success of model checking.We have one logical framework with a few basic temporal operators permitting the expression of limitless specifications.The connection with natural language is often significant as well.Temporal logic made it possible, by and large,to express the correctness properties that needed to be expressed. Without that ability,there would be no reason to use model checking.Alternative temporal formalisms in some cases may be used as they can be more expressive or succinct than temporal logic.But historically it was temporal logic that was the driving force.These alternative temporal formalisms include:(finite state)automata(on infinite strings)which accept infinite inputs by infinitely often entering a desig-nated set of automaton states[Bu62].An expressively equivalent but less succinct formalism is that ofω-regular expressions;for example,ab cωdenotes strings of the form:one a,0or more b s,and infinitely many copies of c;and a property not expressible in LTL(true P)ωensuring that at every even moment P holds. FOLLO(First Order Language of Linear Order)which allows quantification over individual times,for example,∀i≥0Q(i);and SOLLO(Second Order Language of Linear Order)which also allows quantification over sets of times corresponding to monadic predicates such as∃Q(Q(0)∧∀i≥0(Q(i)⇒Q(i+1)).1These alterna-tives are sometimes used for reasons of familiarity,expressiveness or succinctness. LTL is expressively equivalent to FOLLO,but FOLLO can be nonelementarily more succinct.This succinctness is generally found to offer no significant practi-cal advantage.Moreover,model checking is intractably(nonelementarily)hard for FOLLO.Similarly,SOLLO is expressively equivalent toω−regular expres-sions but nonelementarily more succinct.See[Em90]for further discussion.1Technically,the latter abbreviates∃Q(Q(0)∧∀i,j≥0(i<j∧¬∃k(i<k<j))⇒(Q(i)⇒Q(j)).5Temporal logic comes in two broad styles.A linear time LTL assertion h is interpreted with respect to a single path.When interpreted over a program there is an implicit universal quantifications over all paths of the program.An assertion of a branching time logic is interpreted over computation trees.The universal A (for all futures)and existential E(for some future)path quantifiers are important in this context.We can distinguish between AF P(along all futures,P eventually holds and is thus inevitable))and EF P(along some future,P eventually holds and is thus possible).One widely used branching time logic is CTL(Computation Tree Logic)(cf. [CE81]).Its basic temporal modalities are A(for all futures)or E(for some fu-ture)followed by one of F(sometime),G(always),X(next-time),and U(until); compound formulae are built up from nestings and propositional combinations of CTL subformulae.CTL derives from[EC80].There we defined the precursor branching time logic CTF which has path quantifiers∀fullpath and∃fullpath, and is very similar to CTL.In CTF we could write∀fullpath∃state P as well as ∃fullpath∃state P These would be rendered in CTL as AF P and EF P,respec-tively.The streamlined notation was derived from[BMP81].We also defined a modal mu-calculus FPF,and then showed how to translate CTF into FPF. The heart of the translation was characterizing the temporal modalities such as AF P and EF P asfixpoints.Once we had thefixpoint characterizations of these temporal operators,we were close to having model checking.CTL and LTL are of incomparable expressive power.CTL can assert the existence of behaviors,e.g.,AGEF start asserts that it is always possible to re-initialize a circuit.LTL can assert certain more complex behaviors along a computation,such as GF en⇒F ex relating to fairness.(It turns out this formula is not expressible in CTL,but it is in“FairCTL”[EL87])The branching time logic CTL*[EH86]provides a uniform framework that subsumes both LTL and CTL,but at the higher cost of deciding satisfiability.There has been an ongoing debate as to whether linear time logic or branching time logic is better for program reasoning(cf.[La80],[EH86],[Va01]).Remark.The formal semantics of temporal logic formulae are defined with respect to a(Kripke)structure M=(S,S0,R,L)where S is a set of states,S0 comprises the initial states,R⊆S×S is a total binary relation,and L is a labelling of states with atomic facts(propositions)true there.An LTL formula h such as F P is defined over path x=t0,t1,t2...through M by the rule M,x|= F P iff∃i≥0P∈L(t i).Similarly a CTL formula f such as EGP holds of a state t0,denoted M,t0|=EGP,iffthere exists a path x=t0,t1,t2,...in M such that∀i≥0P∈L(t i).For LTL h,we define M|=h ifffor all paths x starting in S0,M,x|=h.For CTL formula f we define M|=f ifffor each s∈S0,M,s|=f.A structure is also known as a state graph or state transition graph or transition system.See[Em90]for details.64The Mu-calculusThe mu-calculus may be viewed as a particular but very general temporal logic. Some formulations go back to the work of de Bakker and Scott[deBS69];we deal specifically with the(propositional or)modal mu-calculus(cf.[EC80],[Ko83]). The mu-calculus provides operators for defining correctness properties using re-cursive definitions plus leastfixpoint and greatestfixpoint operators.Leastfix-points correspond to well-founded or terminating recursion,and are used to capture liveness or progress properties asserting that something does happen. Greatestfixpoints permit infinite recursion.They can be used to capture safety or invariance properties.The mu-calculus is very expressive and veryflexible.It has been referred to as a“Theory of Everything”.The formulae of the mu-calculus are built up from atomic proposition con-stants P,Q,...,atomic proposition variables Y,Z,...,propositional connectives ∨,∧,¬,and the leastfixpoint operator,µas well as the greatestfixpoint opera-tor,ν.Eachfixpoint formula such asµZ.τ(Z)should be syntactically monotone meaning Z occurs under an even number of negations,and similarly forν.The mu-calculus is interpreted with respect to a structure M=(S,R,L). The power set of S,2S,may be viewed as the complete lattice(2S,S,∅,⊆,∪,∩).Intuitively,each(closed)formula may be identified with the set of states of S where it is true.Thus,false which corresponds to the empty set is the bottom element,true which corresponds to S is the top element,and implication (∀s∈S[P(s)⇒Q(s)])which corresponds to simple set-theoretic containment (P⊆Q)provides the partial ordering on the lattice.An open formulaτ(Z) defines a mapping from2S→2S whose value varies as Z varies.A givenτ: 2S→2S is monotone provided that P⊆Q impliesτ(P)⊆τ(Q).Tarski-Knaster Theorem.(cf.[Ta55],[Kn28])Letτ:2S→2S be a monotone functional.Then(a)µY.τ(Y)=∩{Y:τ(Y)=Y}=∩{Y:τ(Y)⊆Y},(b)νY.τ(Y)=∪{Y:τ(Y)=Y}=∪{Y:τ(Y)⊇Y},(c)µY.τ(Y)=∪iτi(false)where i ranges over all ordinals of cardinality at mostthat of the state space S,so that when S isfinite i ranges over[0:|S|],and (d)νY.τ(Y)=∩iτi(true)where i ranges over all ordinals of cardinality at mostthat of the state space S,so that when S isfinite i ranges over[0:|S|].Consider the CTL property AF P.Note that it is afixed point orfixpoint of the functionalτ(Z)=P∨AXZ.That is,as the value of the input Z varies,the value of the outputτ(Z)varies,and we have AF P=τ(AF P)=P∨AXAF P. It can be shown that AF P is the leastfixpoint ofτ(Z),meaning the set of states associated with AF P is a subset of the set of states associated with Z,for any fixpoint Z=τ(Z).This might be denotedµZ.Z=τ(Z).More succinctly,we normally write justµZ.τ(Z).In this case we have AF P=µZ.P∨AXZ.We can get some intuition for the the mu-calculus by noting the following fixpoint characterizations for CTL properties:7EF P=µZ.P∨EXZAGP=νZ.P∧AXZAF P=µZ.P∨AXZEGP=νZ.P∧EXZA(P U Q)=µZ.Q∨(P∧AXZ)E(P U Q)=µZ.Q∨(P∧EXZ)For all these properties,as we see,thefixpoint characterizations are simple and plausible.It is not too difficult to give rigorous proofs of their correctness (cf.[EC80],[EL86]).We emphasize that the mu-calculus is a rich and powerful formalism;its formulae are really representations of alternatingfinite state au-tomata on infinite trees[EJ91].Since even such basic automata as deterministic finite state automata onfinite strings can form quite complex“cans of worms”, we should not be so surprised that it is possible to write down highly inscrutable mu-calculus formulae for which there is no readily apparent intuition regard-ing their intended meaning.The mu-calculus has also been referred to as the “assembly language of program logics”reflecting both its comprehensiveness and potentially intricate syntax.On the other hand,many mu-calculus char-acterizations of correctness properties are elegant due to its simple underlying mathematical organization.In[EL86]we introduced the idea of model checking for the mu-calculus in-stead of testing satisfiability.We catered for efficient model checking in fragments of the the mu-calculus.This provides a basis for practical(symbolic)model checking algorithms.We gave an algorithm essentially of complexity n d,where d is the alternation depth reflecting the number of significantly nested least and greatestfixpoint operators.We showed that common logics such as CTL,LTL, and CTL*were of low alternation depth d=1or d=2.We also provided succinctfixpoint characterizations for various natural fair scheduling criteria.A symbolic fair cycle detection method,known as the“Emerson-Lei”algorithm, is comprised of a simplefixpoint characterization plus the Tarski-Knaster theo-rem.It is widely used in practice even though it has worst case quadratic cost. Empirically,it usually outperforms alternatives.5The Origin of Model CheckingThere were several influences in my personal background that facilitated the de-velopment of model checking.In1975Zohar Manna gave a talk at the University of Texas onfixpoints and the Tarski-Knaster Theorem.I was familiar with Di-jkstra’s book[Di76]extending the Floyd-Hoare framework with wlp the weakest liberal precondition for partial correctness and wp the weakest precondition for to-tal correctness.It turns out that wlp and wp may be viewed as modal operators, for which Dijkstra implicitly gavefixpoint characterizations,although Dijkstra did not favor this viewpoint.Basu and Yeh[BY75]at Texas gavefixpoint char-acterizations of weakest preconditions for while loops.Ed Clarke[Cl79]gave similarfixpoint characterizations for both wp and wlp for a variety of control structures.8I will now describe how model checking originated at Harvard University.In prior work[EC80]we gavefixpoint characterizations for the main modalities of a logic that was essentially CTL.These would ultimately provide thefirst key ingredient of model checking.Incidentally,[EC80]is a paper that could very well not have appeared.Some-how the courier service delivering the hard-copies of the submission to Amster-dam for the program chair at CWI(Dutch for“Center for Mathematics and Computer Science”)sent the package in bill-the-recipient mode.Fortunately, CWI was gracious and accepted the package.All that remained to undo this small misfortune was to get an overseas bank draft to reimburse them.The next work,entitled“Design and Synthesis of Synchronization Skeletons using Branching Time Logic”,was devoted to program synthesis and model checking.I suggested to Ed Clarke that we present the paper,which would be known as[CE81],at the IBM Logics of Programs workshop,since he had an invitation to participate.Both the idea and the term model checking were introduced by Clarke and Emerson in[CE81].Intuitively,this is a method to establish that a given program meets a given specification where:–The program defines afinite state graph M.–M is searched for elaborate patterns to determine if the specification f holds.–Pattern specification isflexible.–The method is efficient in the sizes of M and,ideally,f.–The method is algorithmic.–The method is practical.The conception of model checking was inspired by program synthesis.I was interested in verification,but struck by the difficulties associated with manual proof-theoretic verification as noted above.It seemed that it might be possible to avoid verification altogether and mechanically synthesize a correct program directly from its CTL specification.The idea was to exploit the small model property possessed by certain decidable temporal logics:any satisfiable formula must have a“small”finite model of size that is a function of the formula size. The synthesis method would be sound:if the input specification was satisfiable, it built afinite global state graph that was a model of the specification,from which individual processes could be extracted The synthesis method should also be complete:If the specification was unsatisfiable,it should say so.Initially,it seemed to me technically problematic to develop a sound and complete synthesis method for CTL.However,it could always be ensured that an alleged synthesis method was at least sound.This was clear because given anyfinite model M and CTL specification f one can algorithmically check that M is a genuine model of f by evaluating(verifying)the basic temporal modal-ities over M based on the Tarski-Knaster theorem.This was the second key ingredient of model posite temporal formulae comprised of nested subformulae and boolean combinations of subformulae could be verified by re-cursive descent.Thus,fixpoint characterizations,the Tarski-Knaster theorem, and recursion yielded model checking.9Thus,we obtained the model checking framework.A model checker could be quite useful in practice,given the prevalence offinite state concurrent systems. The temporal logic CTL had theflexibility and expressiveness to capture many important correctness properties.In addition the CTL model checking algorithm was of reasonable efficiency,polynomial in the structure and specification sizes. Incidentally,in later years we sometimes referred to temporal logic model check-ing.The crucial roles of abstraction,synchronization skeletons,andfinite state spaces were discussed in[CE81]:The synchronization skeleton is an abstraction where detail irrelevant to synchronization is suppressed.Most solutions to synchronization prob-lems are in fact given as synchronization skeletons.Because synchronization skeletons are in generalfinite state...proposi-tional temporal logic can be used to specify their properties.Thefinite model property ensures that any program whose synchroniza-tion properties can be expressed in propositional temporal logic can be realized by afinite state machine.Conclusions of[CE81]included the following prognostications,which seem to have been on target:[Program Synthesis]may in the long run be quite practical.Much addi-tional research will be needed,however,to make it feasible in practice....We believe that practical[model checking]tools could be developed in the near future.To sum up,[CE81]made several contributions.It introduced model check-ing,giving an algorithm of quadratic complexity O(|f||M|2).It introduced the logic CTL.It gave an algorithmic method for concurrent program synthesis(that was both sound and complete).It argued that most concurrent systems can be abstracted tofinite state synchronization skeletons.It described a method for efficiently model checking basic fairness using strongly connected components. An NP-hardness result was established for checking certain assertions in a richer logic than CTL.A prototype(and non-robust)model checking tool BMoC was developed,primarily by a Harvard undergraduate,to permit verification of syn-chronization protocols.A later paper[CES86]improved the complexity of CTL model checking to linear O(|f||M|).It showed how to efficiently model check relative to uncondi-tional and weak fairness.The EMC model checking tool was described,and a version of the alternating bit protocol verified.A general framework for efficiently model checking fairness properties was given in[EL87],along with a reduction showing that CTL*model checking could be done as efficiently as LTL model checking.Independently,a similar method was developed in France by Sifakis and his student[QS82].Programs were interpreted over transition systems.A branching10。

注意缺陷多动障碍患儿照顾者照顾负担应对方式对负性情绪的影响李光建 曹静 高婷叶 舒京平 王舟 唐小伟［摘 要］　目的　观察注意缺陷多动障碍（ADHD ）患儿照顾者照顾负担、应对方式对负性情绪的影响因素。

方法　选取2021年6月至2022年12月常州市德安医院心理科确诊的68例ADHD 儿童的照顾者为ADHD 组，选择同期在医院门诊进行常规体检的83例正常儿童的照顾者作为正常对照组，比较两组抑郁-焦虑-压力自评量表（DASS －21）、照顾者负担量表（ZBI ）、简易应对方式问卷（SCSQ ）评估结果。

结果　ADHD 组压力、焦虑、抑郁得分分别为10.0（6.0，16.0）、6.0（2.0，11.5）和5（2.0，11.5）分，照顾者的照顾负担为27.0（20.0，45.0）分，均高于正常对照组，差异均有统计学意义（P <0.05）；ADHD 组照顾者的压力与照顾负担和消极应对方式呈正相关（P <0.05）；ADHD 照顾者的焦虑与照顾负担呈正相关（P <0.05），与积极应对方式呈负相关（P <0.05）；ADHD 照顾者的抑郁与照顾负担和消极应对方式呈正相关（ P <0.05），与积极应对方式呈负相关（P <0.05）；照顾负担、消极应对方式是ADHD 照顾者压力的影响因素（P <0.05），照顾负担、积极应对方式是ADHD 照顾者焦虑的影响因素（P <0.05），照顾负担、积极应对方式、消极应对方式是ADHD 照顾者焦虑的影响因素（P <0.05）。

结论　ADHD 照顾者的负性情绪较多、照顾负担较重，照顾者的照顾负担和应对方式是影响其负性情绪的主要因素。

［关键词］注意缺陷多动障碍；照顾者；照顾负担；负性情绪doi:10.3969/j.issn.1000-0399.2023.10.023Impact of caregiver burden coping styles on negative emotions in children with attention deficit hyperactivity disorder LI Guangjian 1，CAO Jing 2，GAO Tingye 1，SHU Jingping 1，WANG Zhou 1，TANG Xiaowei 31.Department of Psychology,Changzhou De’an Hospital, Changzhou 213003,China 2.Department of Disease,Yucheng District People’s Hospital of Ya ’an, Ya’an 625000,China3.Department of Dsychology,Wutaishan Hospital Affiliated to Medical College of Yangzhou University, Yangzhou 225000,ChinaFunding project:2020 Jiangsu Provincial Health Commission General Project (No.M2020031),Key R&D Plan Project of Changzhou Science and Technology Bureau (No.CE20205049), Key R&D Plan Project of Changzhou Science and Technology Bureau (No.CE20215056)Correspondingauthor:GAOTingye,****************[Abstract ] Objective To observe the influencing factors of caregivers ’ care burden and coping style on negative emotions in childrenwith attention deficit hyperactivity disorder (ADHD). Methods From June 2021 to December 2022, caregivers of 68 ADHD children diag⁃nosed in the Department of Psychology at De ’an Hospital in Changzhou city were selected as the ADHD group, and caregivers of 83 normal children who underwent routine physical examinations at our outpatient department during the same period were selected as the normal control group. The evaluation results of the Depression Anxiety Stress Self Rating Scale (DASS-21), Caregiver Burden Scale (ZBI), and Simple Coping Style Questionnaire (SCSQ) were compared between the two groups. Results The score of stress, anxiety, and depression in the ADHD group was 10.0 (6.0, 16.0), 6.0 (2.0, 11.5)and 5 (2.0, 11.5), respectively. The caregiver ’s care burden was 27.0 (20.0, 45.0), all higher than those of the normal control group, and the differences were statistically significant (P <0.05).The pressure of ADHD caregivers was positively correlated with care burden and negative coping styles (P <0.05). The anxiety of ADHD caregivers was positively correlated with care burden (P<0.05),and negatively correlated with positive coping styles (P <0.05). The depression of ADHD caregivers was positively correlated with care burden and negative coping styles (both P <0.05), and negatively correlated with positive coping styles (P <0.05). The burden of care and negative cop⁃· 卫生服务研究 ·基金项目：2020年度江苏省卫生健康委面上项目（编号：M2020031）；常州市科技局重点研发计划项目（编号：CE20205049）；常州市科技局重点研发计划项目（编号：CE20215056）作者单位：213003 江苏常州 常州市德安医院心理科（李光建，高婷叶，舒京平， 王舟） 625000 四川雅安 雅安市雨城区人民医院病案科（曹静） 225000 江苏扬州 扬州大学医学院附属五台山医院心理科（唐小伟）通信作者：高婷叶,****************本文引用格式：李光建，曹静，高婷叶，等.注意缺陷多动障碍患儿照顾者照顾负担应对方式对负性情绪的影响［J ］.安徽医学，2023，44（10）：1255-1259.DOI ：10.3969/j.issn.1000-0399.2023.10.023ing style were the influencing factors of stress in ADHD caregivers (P<0.05), the burden of care and positive coping style were the influencing factors of anxiety in ADHD caregivers (P<0.05), and the burden of care, positive coping style, and negative coping style were the influencing factors of anxiety in ADHD caregivers (P<0.05). Conclusions　The caregivers of ADHD have more negative emotions and heavy care burden. The care burden and coping style of caregivers are the main factors affecting their negative emotions.［Key words］ Attention deficit hyperactivity disorder；Caregiver；Care burden；Negative emotions注意缺陷多动障碍（attention-deficit/hyperactivitydisorder，ADHD）是一种起病于儿童期的神经发育性疾病［1］。

文献引用格式：12 - 18．YU M，XU X Y，SHI S，et al．Depression Recognition Algorithm Based on Facial Deep Spatio - Temporal Features［J］．中图分类号：基于面部深度空时特征的抑郁症识别算法摘要：提出基于残差注意力网络和金字塔扩大卷积长短时记忆（Convolutional Long Short-Term Memory网络提取人脸图像空时特征的抑郁症识别算法。

首先构建残差注意力网络提取人脸图像不同权值的空间特征，征，显示在两个数据集上，特征10%可见，关键词Abstract:the automatic diagnosis of depression from facial expressions, which extracted spatio-temporal features based on the residual attention network and pyramidal dilated convolutional LSTM network. Firstly, the residual attention network was constructed to extract the spatial features with different weight from facial expressions. Then based on the convLSTM network, a pyramid expansion strategy was added to extract the temporal features with different scales on the resulting spatial features. Finally the spatio-temporal features were input into the DNN network for the regression analysis of depression inventory score. Validation was performed on the AVECthe results were shown on both data sets, the Mae and RMSE values between the predicted and true depression degree of the proposed algorithm are better than those based on manual feature and manual feature + depth feature. In the AVEC2030年，抑郁症将成为全世界导致死亡和残疾的最大因素［2］。

第42卷第3期2021年5月Vol.42No.3May2021中山大学学报（医学科学版）JOURNAL OF SUN YAT⁃SEN UNIVERSITY（MEDICAL SCIENCES）基于化学遗传的慢性应激导致抑郁症小鼠模型的构建邓艺雯，张寅航，徐兴浩，蚁焌哲，张小然，黄玮俊（中山大学中山医学院干细胞与组织工程研究中心，广东广州510080）摘要：【目的】建立基于化学遗传的慢性应激导致抑郁症的小鼠模型，为优化慢性应激诱发抑郁症的动物建模方法提供参考。

【方法】通过化学遗传的方法，对小鼠延髓腹外侧区头端（RVLM）进行持续的刺激，模拟机体对慢性应激的响应，系统观察造模和对照组小鼠的行为学、血压及主要炎症因子的变化情况。

【结果】成功建立了小鼠模型。

经腹腔向小鼠给药CNO1h后，造模组较对照组的舒张压与平均脉压显著上升。

持续给药4周后，造模组较对照组的旷场实验的水平运动总距离、中央区进入总次数、中央区滞留时间和中央区域运动总距离这四项指标均显著下降；蔗糖偏好实验提示造模组存在快感缺失；转棒实验提示造模组运动协调能力显著减弱；同时，造模组心率、血压、炎性因子IFN-γ和抑炎因子IL-10水平等也较对照组显著上调。

【结论】我们的模型在诱发抑郁症经典症状，及血压偏高、炎性因子释放紊乱等抑郁症伴随症状上均表现出较高的成功率和稳定性。

这为优化慢性应激诱发抑郁症的动物建模效率和稳定性提供了有参考价值的科学依据。

关键词：抑郁症；慢性应激；交感神经；化学遗传；延髓腹外侧区头端中图分类号：R338.2+2文献标志码：A文章编号：1672-3554（2021）03-0346-09DOI：10.13471/ki.j.sun.yat-sen.univ（med.sci）.2021.0104Establishment of Chronic Stress Inducing Depressive Disorder Mouse ModelVia Chemical GeneticsDENG Yi-wen，ZHANG Yin-hang，XU Xing-hao，YI Jun-zhe，ZHANG Xiao-ran，HUANG Wei-jun（Center for Stem Cell Biology and Tissue Engineering，Zhongshan School of Medicine，Sun Yat-sen University，Guangzhou510080，China）Correspondence to：HUANG Wei-jun；E-mail：*****************Abstract：【Objective】To establish a chronic stress inducing depressive disorder mouse model via chemical genetics，that helps to optimize the animal modeling method of chronic stress-induced depressive disorder.【Methods】To continuous⁃ly stimulate the rostral ventrolateral medulla（RVLM）of mouse by chemical genetic method to mimic the response to chron⁃ic stress.The changes about behavior，blood pressure and major inflammatory factors of the animal models were corre⁃spondingly observed.【Results】The mouse model was established successfully.One hour after intraperitoneal administra⁃tion of CNO，diastolic blood pressure and mean blood pressure were significantly increased in the model group compared with the control.After four weeks of continuous administration，the total distance of movement，the total entering bouts，the distance and duration of the central area in the model group were significantly decreased compared with the control in the open field experiment.The results of sucrose preference and rotarod experiment suggested anhedonia and weakened mo⁃tor coordination ability in the model group.The heart rate，blood pressure，expressions of IFN-γand IL-10in the model group were higher than those in the control.【Conclusions】Our model developed classic symptoms of depressive disorder ef⁃ficiently and stably，as well as accompanying symptoms such as high blood pressure and mussy release of inflammatory fac⁃tors.It provides a valuable scientific basis for improving the efficiency and stability of animal modeling of chronic stress-induced depressive disorder.Key words：depressive disorder；chronic stress；sympathetic nerve；chemical genetics；RVLM［J SUN Yat⁃sen Univ（Med Sci），2021，42（3）：346-354］收稿日期：2021-03-01基金项目：国家自然科学基金（81970222）；广东省科技计划项目（2016B090918040，2017B020230004）作者简介：邓艺雯，硕士生，研究方向：干细胞与组织工程，E-mail：******************；黄玮俊，通信作者，副教授，博士生导师，E-mail：*****************第3期邓艺雯，等.基于化学遗传的慢性应激导致抑郁症小鼠模型的构建抑郁症（depressive disorder）是一种常见的精神类疾病，核心症状是情感低落（depressed mood）、兴趣减退或快感缺失（anhedonia）。

再论中介模型滥⽤：如何规范地实施因果中介效应分析因果中介效应估计、敏感性分析、⼯具变量模型。

近年来，⼤量的经济学论⽂滥⽤中介效应模型，参考⽂献是⼀遍中⽂⼼理学论⽂，特别以硕⼠论⽂居多，引起严肃经济学者的警觉和批评。

在这个⽅程组中有很多的问题存在：y=a+bx+u (1)m=a1x+u1 (2)y=a2x+b2m+u2 (3）很显然（1）式中⾄少遗漏了中介变量m，则导致严重内⽣性问题，内⽣性导致b的估计是有偏的，b都估计不对，何谈后⾯的因果效应和机制分析的识别？且不说有没有考虑三个⼦⽅程的内⽣性问题了！令⼈悲哀和⽆免，其实只需要基本的初等计量经济学知识！本推⽂将介绍在因果分析框架下中介分析模型。

此外，管理学的调节效应其实就是规范实证经济学⾥⾯的交互项模型，即相关异质性因果效应分析：即将开幕的STATA前沿培训精讲：带异质性处理效应的双向固定效应估计|从精确断点、模糊断点估计的实际操作|弱⼯具变量稳健推断异质性分析、机制分析的内容可选择学习：即将开班 | 结构模型、Stata实证前沿、Python数据挖掘暑假⼯作坊当然，⽐较合理地机制分析是基于理论框架的科学分析，这也可以在以上暑假⼯作坊课程中的结构估计部分学习之，其也提供⽂本分析的内容。

欢迎咨询！Causal mediation analysisRaymond Hicks,Niehaus Center for Globalization and GovernancePrinceton University,Princeton, NJ,rhicks@Dustin Tingley,Department of Government,Harvard UniversityCambridge, MA,dtingley@Abstract. Estimating the mechanisms that connect explanatory variables with the explained variable, also known as “mediation analysis,” is central to a variety of social-science fields, especially psychology, and incre epidemiology.Recent work on the statistical methodology behind mediation analysis points to limitations in earlier methods. We implement in Stata computational approaches based on recent developments in the sta analysis. In particular, we provide functions for the correct calculation of causal mediation effects using several different types of parametric models, as well as the calculation of sensitivity analyses for violations to the required for interpreting mediation results causally.摘要：估计解释变量与被解释变量之间的联系机制，也被称为“中介分析”，是各种社会科学领域的核⼼，尤其是⼼理学，并逐渐成为流⾏病学等领域的核⼼。

predictmodel的例子预测模型是机器学习中常用的一种方法，用于根据已有的数据来预测未知的结果。

预测模型可以应用于各种领域，如金融、医疗、市场营销等。

下面将以一个简单的预测模型为例，介绍预测模型的基本原理和使用方法。

一、预测模型的基本原理预测模型的基本原理是通过对已有的数据进行分析和建模，然后利用模型对未知的数据进行预测。

预测模型可以分为监督学习和无监督学习两种类型。

监督学习是指通过已有的带有标签的数据来训练模型，然后利用模型对未知数据进行预测；无监督学习则是指利用未标记的数据进行训练，通过发现数据的内在规律来进行预测。

二、预测模型的示例以一个简单的线性回归模型为例，假设我们有一组数据，包含了房屋的面积和价格。

我们希望通过这组数据来建立一个模型，可以根据房屋的面积来预测价格。

1. 数据收集和准备我们需要收集一组房屋的面积和价格数据。

这些数据可以通过房地产网站、房产中介或者相关机构获取。

收集到的数据需要进行清洗和预处理，包括去除异常值、处理缺失值等。

2. 数据探索和特征选择在建立模型之前，我们需要对数据进行探索和分析，了解数据的分布、相关性等。

同时，我们还需要选择合适的特征，即房屋的面积作为预测模型的输入特征，价格作为输出特征。

3. 模型训练和评估在完成数据准备和特征选择之后，我们可以利用已有的数据来训练模型。

对于线性回归模型来说，我们可以通过最小二乘法来估计模型的参数。

训练完成后，我们需要对模型进行评估，可以使用均方误差等指标来评判模型的性能。

4. 模型应用和预测当模型训练和评估完成后，我们可以将其应用于未知的数据，根据输入的房屋面积来预测价格。

预测结果可以帮助我们做出决策，如购买房屋时的价格参考。

三、预测模型的应用预测模型在实际应用中有着广泛的应用，下面列举几个常见的应用场景。

1. 股票价格预测通过历史的股票价格数据，建立预测模型来预测未来的股票价格走势，帮助投资者做出投资决策。

2. 疾病预测通过分析病人的病例和生理指标，建立预测模型来预测疾病的发展趋势，帮助医生提前采取干预措施。

Network impacts of a road capacity reduction:Empirical analysisand model predictionsDavid Watling a ,⇑,David Milne a ,Stephen Clark baInstitute for Transport Studies,University of Leeds,Woodhouse Lane,Leeds LS29JT,UK b Leeds City Council,Leonardo Building,2Rossington Street,Leeds LS28HD,UKa r t i c l e i n f o Article history:Received 24May 2010Received in revised form 15July 2011Accepted 7September 2011Keywords:Traffic assignment Network models Equilibrium Route choice Day-to-day variabilitya b s t r a c tIn spite of their widespread use in policy design and evaluation,relatively little evidencehas been reported on how well traffic equilibrium models predict real network impacts.Here we present what we believe to be the first paper that together analyses the explicitimpacts on observed route choice of an actual network intervention and compares thiswith the before-and-after predictions of a network equilibrium model.The analysis isbased on the findings of an empirical study of the travel time and route choice impactsof a road capacity reduction.Time-stamped,partial licence plates were recorded across aseries of locations,over a period of days both with and without the capacity reduction,and the data were ‘matched’between locations using special-purpose statistical methods.Hypothesis tests were used to identify statistically significant changes in travel times androute choice,between the periods of days with and without the capacity reduction.A trafficnetwork equilibrium model was then independently applied to the same scenarios,and itspredictions compared with the empirical findings.From a comparison of route choice pat-terns,a particularly influential spatial effect was revealed of the parameter specifying therelative values of distance and travel time assumed in the generalised cost equations.When this parameter was ‘fitted’to the data without the capacity reduction,the networkmodel broadly predicted the route choice impacts of the capacity reduction,but with othervalues it was seen to perform poorly.The paper concludes by discussing the wider practicaland research implications of the study’s findings.Ó2011Elsevier Ltd.All rights reserved.1.IntroductionIt is well known that altering the localised characteristics of a road network,such as a planned change in road capacity,will tend to have both direct and indirect effects.The direct effects are imparted on the road itself,in terms of how it can deal with a given demand flow entering the link,with an impact on travel times to traverse the link at a given demand flow level.The indirect effects arise due to drivers changing their travel decisions,such as choice of route,in response to the altered travel times.There are many practical circumstances in which it is desirable to forecast these direct and indirect impacts in the context of a systematic change in road capacity.For example,in the case of proposed road widening or junction improvements,there is typically a need to justify econom-ically the required investment in terms of the benefits that will likely accrue.There are also several examples in which it is relevant to examine the impacts of road capacity reduction .For example,if one proposes to reallocate road space between alternative modes,such as increased bus and cycle lane provision or a pedestrianisation scheme,then typically a range of alternative designs exist which may differ in their ability to accommodate efficiently the new traffic and routing patterns.0965-8564/$-see front matter Ó2011Elsevier Ltd.All rights reserved.doi:10.1016/j.tra.2011.09.010⇑Corresponding author.Tel.:+441133436612;fax:+441133435334.E-mail address:d.p.watling@ (D.Watling).168 D.Watling et al./Transportation Research Part A46(2012)167–189Through mathematical modelling,the alternative designs may be tested in a simulated environment and the most efficient selected for implementation.Even after a particular design is selected,mathematical models may be used to adjust signal timings to optimise the use of the transport system.Road capacity may also be affected periodically by maintenance to essential services(e.g.water,electricity)or to the road itself,and often this can lead to restricted access over a period of days and weeks.In such cases,planning authorities may use modelling to devise suitable diversionary advice for drivers,and to plan any temporary changes to traffic signals or priorities.Berdica(2002)and Taylor et al.(2006)suggest more of a pro-ac-tive approach,proposing that models should be used to test networks for potential vulnerability,before any reduction mate-rialises,identifying links which if reduced in capacity over an extended period1would have a substantial impact on system performance.There are therefore practical requirements for a suitable network model of travel time and route choice impacts of capac-ity changes.The dominant method that has emerged for this purpose over the last decades is clearly the network equilibrium approach,as proposed by Beckmann et al.(1956)and developed in several directions since.The basis of using this approach is the proposition of what are believed to be‘rational’models of behaviour and other system components(e.g.link perfor-mance functions),with site-specific data used to tailor such models to particular case studies.Cross-sectional forecasts of network performance at specific road capacity states may then be made,such that at the time of any‘snapshot’forecast, drivers’route choices are in some kind of individually-optimum state.In this state,drivers cannot improve their route selec-tion by a unilateral change of route,at the snapshot travel time levels.The accepted practice is to‘validate’such models on a case-by-case basis,by ensuring that the model—when supplied with a particular set of parameters,input network data and input origin–destination demand data—reproduces current mea-sured mean link trafficflows and mean journey times,on a sample of links,to some degree of accuracy(see for example,the practical guidelines in TMIP(1997)and Highways Agency(2002)).This kind of aggregate level,cross-sectional validation to existing conditions persists across a range of network modelling paradigms,ranging from static and dynamic equilibrium (Florian and Nguyen,1976;Leonard and Tough,1979;Stephenson and Teply,1984;Matzoros et al.,1987;Janson et al., 1986;Janson,1991)to micro-simulation approaches(Laird et al.,1999;Ben-Akiva et al.,2000;Keenan,2005).While such an approach is plausible,it leaves many questions unanswered,and we would particularly highlight two: 1.The process of calibration and validation of a network equilibrium model may typically occur in a cycle.That is to say,having initially calibrated a model using the base data sources,if the subsequent validation reveals substantial discrep-ancies in some part of the network,it is then natural to adjust the model parameters(including perhaps even the OD matrix elements)until the model outputs better reflect the validation data.2In this process,then,we allow the adjustment of potentially a large number of network parameters and input data in order to replicate the validation data,yet these data themselves are highly aggregate,existing only at the link level.To be clear here,we are talking about a level of coarseness even greater than that in aggregate choice models,since we cannot even infer from link-level data the aggregate shares on alternative routes or OD movements.The question that arises is then:how many different combinations of parameters and input data values might lead to a similar link-level validation,and even if we knew the answer to this question,how might we choose between these alternative combinations?In practice,this issue is typically neglected,meaning that the‘valida-tion’is a rather weak test of the model.2.Since the data are cross-sectional in time(i.e.the aim is to reproduce current base conditions in equilibrium),then in spiteof the large efforts required in data collection,no empirical evidence is routinely collected regarding the model’s main purpose,namely its ability to predict changes in behaviour and network performance under changes to the network/ demand.This issue is exacerbated by the aggregation concerns in point1:the‘ambiguity’in choosing appropriate param-eter values to satisfy the aggregate,link-level,base validation strengthens the need to independently verify that,with the selected parameter values,the model responds reliably to changes.Although such problems–offitting equilibrium models to cross-sectional data–have long been recognised by practitioners and academics(see,e.g.,Goodwin,1998), the approach described above remains the state-of-practice.Having identified these two problems,how might we go about addressing them?One approach to thefirst problem would be to return to the underlying formulation of the network model,and instead require a model definition that permits analysis by statistical inference techniques(see for example,Nakayama et al.,2009).In this way,we may potentially exploit more information in the variability of the link-level data,with well-defined notions(such as maximum likelihood)allowing a systematic basis for selection between alternative parameter value combinations.However,this approach is still using rather limited data and it is natural not just to question the model but also the data that we use to calibrate and validate it.Yet this is not altogether straightforward to resolve.As Mahmassani and Jou(2000) remarked:‘A major difficulty...is obtaining observations of actual trip-maker behaviour,at the desired level of richness, simultaneously with measurements of prevailing conditions’.For this reason,several authors have turned to simulated gaming environments and/or stated preference techniques to elicit information on drivers’route choice behaviour(e.g. 1Clearly,more sporadic and less predictable reductions in capacity may also occur,such as in the case of breakdowns and accidents,and environmental factors such as severe weather,floods or landslides(see for example,Iida,1999),but the responses to such cases are outside the scope of the present paper. 2Some authors have suggested more systematic,bi-level type optimization processes for thisfitting process(e.g.Xu et al.,2004),but this has no material effect on the essential points above.D.Watling et al./Transportation Research Part A46(2012)167–189169 Mahmassani and Herman,1990;Iida et al.,1992;Khattak et al.,1993;Vaughn et al.,1995;Wardman et al.,1997;Jou,2001; Chen et al.,2001).This provides potentially rich information for calibrating complex behavioural models,but has the obvious limitation that it is based on imagined rather than real route choice situations.Aside from its common focus on hypothetical decision situations,this latter body of work also signifies a subtle change of emphasis in the treatment of the overall network calibration problem.Rather than viewing the network equilibrium calibra-tion process as a whole,the focus is on particular components of the model;in the cases above,the focus is on that compo-nent concerned with how drivers make route decisions.If we are prepared to make such a component-wise analysis,then certainly there exists abundant empirical evidence in the literature,with a history across a number of decades of research into issues such as the factors affecting drivers’route choice(e.g.Wachs,1967;Huchingson et al.,1977;Abu-Eisheh and Mannering,1987;Duffell and Kalombaris,1988;Antonisse et al.,1989;Bekhor et al.,2002;Liu et al.,2004),the nature of travel time variability(e.g.Smeed and Jeffcoate,1971;Montgomery and May,1987;May et al.,1989;McLeod et al., 1993),and the factors affecting trafficflow variability(Bonsall et al.,1984;Huff and Hanson,1986;Ribeiro,1994;Rakha and Van Aerde,1995;Fox et al.,1998).While these works provide useful evidence for the network equilibrium calibration problem,they do not provide a frame-work in which we can judge the overall‘fit’of a particular network model in the light of uncertainty,ambient variation and systematic changes in network attributes,be they related to the OD demand,the route choice process,travel times or the network data.Moreover,such data does nothing to address the second point made above,namely the question of how to validate the model forecasts under systematic changes to its inputs.The studies of Mannering et al.(1994)and Emmerink et al.(1996)are distinctive in this context in that they address some of the empirical concerns expressed in the context of travel information impacts,but their work stops at the stage of the empirical analysis,without a link being made to net-work prediction models.The focus of the present paper therefore is both to present thefindings of an empirical study and to link this empirical evidence to network forecasting models.More recently,Zhu et al.(2010)analysed several sources of data for evidence of the traffic and behavioural impacts of the I-35W bridge collapse in Minneapolis.Most pertinent to the present paper is their location-specific analysis of linkflows at 24locations;by computing the root mean square difference inflows between successive weeks,and comparing the trend for 2006with that for2007(the latter with the bridge collapse),they observed an apparent transient impact of the bridge col-lapse.They also showed there was no statistically-significant evidence of a difference in the pattern offlows in the period September–November2007(a period starting6weeks after the bridge collapse),when compared with the corresponding period in2006.They suggested that this was indicative of the length of a‘re-equilibration process’in a conceptual sense, though did not explicitly compare their empiricalfindings with those of a network equilibrium model.The structure of the remainder of the paper is as follows.In Section2we describe the process of selecting the real-life problem to analyse,together with the details and rationale behind the survey design.Following this,Section3describes the statistical techniques used to extract information on travel times and routing patterns from the survey data.Statistical inference is then considered in Section4,with the aim of detecting statistically significant explanatory factors.In Section5 comparisons are made between the observed network data and those predicted by a network equilibrium model.Finally,in Section6the conclusions of the study are highlighted,and recommendations made for both practice and future research.2.Experimental designThe ultimate objective of the study was to compare actual data with the output of a traffic network equilibrium model, specifically in terms of how well the equilibrium model was able to correctly forecast the impact of a systematic change ap-plied to the network.While a wealth of surveillance data on linkflows and travel times is routinely collected by many local and national agencies,we did not believe that such data would be sufficiently informative for our purposes.The reason is that while such data can often be disaggregated down to small time step resolutions,the data remains aggregate in terms of what it informs about driver response,since it does not provide the opportunity to explicitly trace vehicles(even in aggre-gate form)across more than one location.This has the effect that observed differences in linkflows might be attributed to many potential causes:it is especially difficult to separate out,say,ambient daily variation in the trip demand matrix from systematic changes in route choice,since both may give rise to similar impacts on observed linkflow patterns across re-corded sites.While methods do exist for reconstructing OD and network route patterns from observed link data(e.g.Yang et al.,1994),these are typically based on the premise of a valid network equilibrium model:in this case then,the data would not be able to give independent information on the validity of the network equilibrium approach.For these reasons it was decided to design and implement a purpose-built survey.However,it would not be efficient to extensively monitor a network in order to wait for something to happen,and therefore we required advance notification of some planned intervention.For this reason we chose to study the impact of urban maintenance work affecting the roads,which UK local government authorities organise on an annual basis as part of their‘Local Transport Plan’.The city council of York,a historic city in the north of England,agreed to inform us of their plans and to assist in the subsequent data collection exercise.Based on the interventions planned by York CC,the list of candidate studies was narrowed by considering factors such as its propensity to induce significant re-routing and its impact on the peak periods.Effectively the motivation here was to identify interventions that were likely to have a large impact on delays,since route choice impacts would then likely be more significant and more easily distinguished from ambient variability.This was notably at odds with the objectives of York CC,170 D.Watling et al./Transportation Research Part A46(2012)167–189in that they wished to minimise disruption,and so where possible York CC planned interventions to take place at times of day and of the year where impacts were minimised;therefore our own requirement greatly reduced the candidate set of studies to monitor.A further consideration in study selection was its timing in the year for scheduling before/after surveys so to avoid confounding effects of known significant‘seasonal’demand changes,e.g.the impact of the change between school semesters and holidays.A further consideration was York’s role as a major tourist attraction,which is also known to have a seasonal trend.However,the impact on car traffic is relatively small due to the strong promotion of public trans-port and restrictions on car travel and parking in the historic centre.We felt that we further mitigated such impacts by sub-sequently choosing to survey in the morning peak,at a time before most tourist attractions are open.Aside from the question of which intervention to survey was the issue of what data to collect.Within the resources of the project,we considered several options.We rejected stated preference survey methods as,although they provide a link to personal/socio-economic drivers,we wanted to compare actual behaviour with a network model;if the stated preference data conflicted with the network model,it would not be clear which we should question most.For revealed preference data, options considered included(i)self-completion diaries(Mahmassani and Jou,2000),(ii)automatic tracking through GPS(Jan et al.,2000;Quiroga et al.,2000;Taylor et al.,2000),and(iii)licence plate surveys(Schaefer,1988).Regarding self-comple-tion surveys,from our own interview experiments with self-completion questionnaires it was evident that travellersfind it relatively difficult to recall and describe complex choice options such as a route through an urban network,giving the po-tential for significant errors to be introduced.The automatic tracking option was believed to be the most attractive in this respect,in its potential to accurately map a given individual’s journey,but the negative side would be the potential sample size,as we would need to purchase/hire and distribute the devices;even with a large budget,it is not straightforward to identify in advance the target users,nor to guarantee their cooperation.Licence plate surveys,it was believed,offered the potential for compromise between sample size and data resolution: while we could not track routes to the same resolution as GPS,by judicious location of surveyors we had the opportunity to track vehicles across more than one location,thus providing route-like information.With time-stamped licence plates, the matched data would also provide journey time information.The negative side of this approach is the well-known poten-tial for significant recording errors if large sample rates are required.Our aim was to avoid this by recording only partial licence plates,and employing statistical methods to remove the impact of‘spurious matches’,i.e.where two different vehi-cles with the same partial licence plate occur at different locations.Moreover,extensive simulation experiments(Watling,1994)had previously shown that these latter statistical methods were effective in recovering the underlying movements and travel times,even if only a relatively small part of the licence plate were recorded,in spite of giving a large potential for spurious matching.We believed that such an approach reduced the opportunity for recorder error to such a level to suggest that a100%sample rate of vehicles passing may be feasible.This was tested in a pilot study conducted by the project team,with dictaphones used to record a100%sample of time-stamped, partial licence plates.Independent,duplicate observers were employed at the same location to compare error rates;the same study was also conducted with full licence plates.The study indicated that100%surveys with dictaphones would be feasible in moderate trafficflow,but only if partial licence plate data were used in order to control observation errors; for higherflow rates or to obtain full number plate data,video surveys should be considered.Other important practical les-sons learned from the pilot included the need for clarity in terms of vehicle types to survey(e.g.whether to include motor-cycles and taxis),and of the phonetic alphabet used by surveyors to avoid transcription ambiguities.Based on the twin considerations above of planned interventions and survey approach,several candidate studies were identified.For a candidate study,detailed design issues involved identifying:likely affected movements and alternative routes(using local knowledge of York CC,together with an existing network model of the city),in order to determine the number and location of survey sites;feasible viewpoints,based on site visits;the timing of surveys,e.g.visibility issues in the dark,winter evening peak period;the peak duration from automatic trafficflow data;and specific survey days,in view of public/school holidays.Our budget led us to survey the majority of licence plate sites manually(partial plates by audio-tape or,in lowflows,pen and paper),with video surveys limited to a small number of high-flow sites.From this combination of techniques,100%sampling rate was feasible at each site.Surveys took place in the morning peak due both to visibility considerations and to minimise conflicts with tourist/special event traffic.From automatic traffic count data it was decided to survey the period7:45–9:15as the main morning peak period.This design process led to the identification of two studies:2.1.Lendal Bridge study(Fig.1)Lendal Bridge,a critical part of York’s inner ring road,was scheduled to be closed for maintenance from September2000 for a duration of several weeks.To avoid school holidays,the‘before’surveys were scheduled for June and early September.It was decided to focus on investigating a significant southwest-to-northeast movement of traffic,the river providing a natural barrier which suggested surveying the six river crossing points(C,J,H,K,L,M in Fig.1).In total,13locations were identified for survey,in an attempt to capture traffic on both sides of the river as well as a crossing.2.2.Fishergate study(Fig.2)The partial closure(capacity reduction)of the street known as Fishergate,again part of York’s inner ring road,was scheduled for July2001to allow repairs to a collapsed sewer.Survey locations were chosen in order to intercept clockwiseFig.1.Intervention and survey locations for Lendal Bridge study.around the inner ring road,this being the direction of the partial closure.A particular aim wasFulford Road(site E in Fig.2),the main radial affected,with F and K monitoring local diversion I,J to capture wider-area diversion.studies,the plan was to survey the selected locations in the morning peak over a period of approximately covering the three periods before,during and after the intervention,with the days selected so holidays or special events.Fig.2.Intervention and survey locations for Fishergate study.In the Lendal Bridge study,while the‘before’surveys proceeded as planned,the bridge’s actualfirst day of closure on Sep-tember11th2000also marked the beginning of the UK fuel protests(BBC,2000a;Lyons and Chaterjee,2002).Trafficflows were considerably affected by the scarcity of fuel,with congestion extremely low in thefirst week of closure,to the extent that any changes could not be attributed to the bridge closure;neither had our design anticipated how to survey the impacts of the fuel shortages.We thus re-arranged our surveys to monitor more closely the planned re-opening of the bridge.Unfor-tunately these surveys were hampered by a second unanticipated event,namely the wettest autumn in the UK for270years and the highest level offlooding in York since records began(BBC,2000b).Theflooding closed much of the centre of York to road traffic,including our study area,as the roads were impassable,and therefore we abandoned the planned‘after’surveys. As a result of these events,the useable data we had(not affected by the fuel protests orflooding)consisted offive‘before’days and one‘during’day.In the Fishergate study,fortunately no extreme events occurred,allowing six‘before’and seven‘during’days to be sur-veyed,together with one additional day in the‘during’period when the works were temporarily removed.However,the works over-ran into the long summer school holidays,when it is well-known that there is a substantial seasonal effect of much lowerflows and congestion levels.We did not believe it possible to meaningfully isolate the impact of the link fully re-opening while controlling for such an effect,and so our plans for‘after re-opening’surveys were abandoned.3.Estimation of vehicle movements and travel timesThe data resulting from the surveys described in Section2is in the form of(for each day and each study)a set of time-stamped,partial licence plates,observed at a number of locations across the network.Since the data include only partial plates,they cannot simply be matched across observation points to yield reliable estimates of vehicle movements,since there is ambiguity in whether the same partial plate observed at different locations was truly caused by the same vehicle. Indeed,since the observed system is‘open’—in the sense that not all points of entry,exit,generation and attraction are mon-itored—the question is not just which of several potential matches to accept,but also whether there is any match at all.That is to say,an apparent match between data at two observation points could be caused by two separate vehicles that passed no other observation point.Thefirst stage of analysis therefore applied a series of specially-designed statistical techniques to reconstruct the vehicle movements and point-to-point travel time distributions from the observed data,allowing for all such ambiguities in the data.Although the detailed derivations of each method are not given here,since they may be found in the references provided,it is necessary to understand some of the characteristics of each method in order to interpret the results subsequently provided.Furthermore,since some of the basic techniques required modification relative to the published descriptions,then in order to explain these adaptations it is necessary to understand some of the theoretical basis.3.1.Graphical method for estimating point-to-point travel time distributionsThe preliminary technique applied to each data set was the graphical method described in Watling and Maher(1988).This method is derived for analysing partial registration plate data for unidirectional movement between a pair of observation stations(referred to as an‘origin’and a‘destination’).Thus in the data study here,it must be independently applied to given pairs of observation stations,without regard for the interdependencies between observation station pairs.On the other hand, it makes no assumption that the system is‘closed’;there may be vehicles that pass the origin that do not pass the destina-tion,and vice versa.While limited in considering only two-point surveys,the attraction of the graphical technique is that it is a non-parametric method,with no assumptions made about the arrival time distributions at the observation points(they may be non-uniform in particular),and no assumptions made about the journey time probability density.It is therefore very suitable as afirst means of investigative analysis for such data.The method begins by forming all pairs of possible matches in the data,of which some will be genuine matches(the pair of observations were due to a single vehicle)and the remainder spurious matches.Thus, for example,if there are three origin observations and two destination observations of a particular partial registration num-ber,then six possible matches may be formed,of which clearly no more than two can be genuine(and possibly only one or zero are genuine).A scatter plot may then be drawn for each possible match of the observation time at the origin versus that at the destination.The characteristic pattern of such a plot is as that shown in Fig.4a,with a dense‘line’of points(which will primarily be the genuine matches)superimposed upon a scatter of points over the whole region(which will primarily be the spurious matches).If we were to assume uniform arrival rates at the observation stations,then the spurious matches would be uniformly distributed over this plot;however,we shall avoid making such a restrictive assumption.The method begins by making a coarse estimate of the total number of genuine matches across the whole of this plot.As part of this analysis we then assume knowledge of,for any randomly selected vehicle,the probabilities:h k¼Prðvehicle is of the k th type of partial registration plateÞðk¼1;2;...;mÞwhereX m k¼1h k¼1172 D.Watling et al./Transportation Research Part A46(2012)167–189。

慢性炎性痛模型小鼠腹外侧眶额叶皮质的转录组分析张思博;尹美娴;李婧;柳垂亮【期刊名称】《神经解剖学杂志》【年(卷),期】2024(40)2【摘要】目的:筛选小鼠腹外侧眶额皮质(vlOFC)参与疼痛调节的生物学标记物。

方法:雄性C57BL/6J小鼠于左后足底注射完全弗氏佐剂(CFA)诱导慢性炎性痛。

通过测定缩足阈值(PWT)和缩足潜伏期(PWL)检测痛敏变化。

行为学测试之后取小鼠vlOFC新鲜组织进行转录组测序。

运用生物信息学方法筛选差异表达基因(DEGs),并进行生物学功能和通路富集分析。

结果:与PBS组小鼠相比,CFA组小鼠左后足机械痛阈值和热痛导致的缩爪潜伏期均显著降低(P<0.001)。

两组小鼠vlOFC的DEGs为497个,其中上调143个,下调354个。

基因本体(GO)和京都基因与基因组百科全书(KEGGs)分析显示:慢性炎性痛模型小鼠,vlOFC的DEGs主要表现在有机阳离子转运、神经递质转运、胞质钙离子浓度的调节等生物过程;与G蛋白偶联受体(GPCRs)、神经肽相关以及铵转运等分子功能相关;DEGs主要集中于神经活性配体-受体相互作用、细胞因子-细胞因子受体相互作用、cAMP信号通路。

Reactome功能富集分析显示,参与富集的DEGs数量最多且校正后P值最低的通路为GPCRs配体结合。

结论:vlOFC中的离子转运、神经递质转运与结合、GPCRs相关活动参与了慢性炎性痛的调节。

【总页数】9页(P187-195)【作者】张思博;尹美娴;李婧;柳垂亮【作者单位】广州中医药大学佛山临床医学院;中山大学中山医学院人体解剖学与生理系【正文语种】中文【中图分类】R28【相关文献】1.腹外侧眶皮质在痛觉下行调制中的神经递质与受体机制2.刺激额叶皮层对丘脑腹后外侧核痛放电的影响及其与电针的关系3.大鼠丘脑中央下核GABA纤维终末与腹外侧眶皮质投射神经元的突触联系4.电离辐射激活前额叶皮质NLRP3炎性小体诱导小鼠认知功能障碍5.GluN3A基因缺失影响小鼠抑郁样行为及内侧前额叶皮质与海马mRNA转录组的实验研究因版权原因，仅展示原文概要，查看原文内容请购买。