a r
X
i
v
:09
4
.
3
4
v
1
[
c
s
.
L
O ]
3
1
M
a
r
2
9
CCS-Based Dynamic Logics for Communicating Concurrent Programs ?Mario R.F.Benevides ?L.Menasch′e Schechter ?{mario,luis }@cos.ufrj.br Abstract This work presents three increasingly expressive Dynamic Logics in which the programs are CCS processes (sCCS-PDL,CCS-PDL and XCCS-PDL).Their goal is to reason about properties of concurrent programs and systems described using CCS.In order to accomplish that,CCS’s opera-tors and constructions are added to a basic modal logic in order to create dynamic logics that are suitable for the description and veri?cation of properties of communicating,concurrent and non-deterministic programs and systems,in a similar way as PDL is used for the sequential case.We provide complete axiomatizations for the three logics.Unlike Peleg’s Con-current PDL with Channels,our logics have a simple Kripke semantics,complete axiomatizations and the ?nite model property.Keywords:Dynamic Logic,Concurrency,Kripke Semantics,Axiomatization,Completeness 1Introduction Propositional Dynamic Logic (PDL)[7]plays an important role in formal speci-?cation and reasoning about sequential programs and systems.PDL is a multi-modal logic with one modality π for each program π.The logic has a set of basic programs and a set of operators (sequential composition,iteration and nondeterministic choice)that are used to inductively build the set of non-basic programs.PDL has been used to describe and verify properties and behaviour of sequential programs and systems.Correctness,termination,fairness,liveness and equivalence of programs are among the properties that one usually wants
to verify.A Kripke semantics can be provided,with a frame F =(W,R π),where W is a non-empty set of possible program states and,for each program π,R πis a binary relation on W such that (s,t )∈R πif and only if there is a computation of πstarting in s and terminating in t .
The Calculus for Communicating Systems (CCS)is a well known process algebra,proposed by Robin Milner [12],for the speci?cation of communicat-ing concurrent systems.It models the concurrency and interaction between
processes through individual acts of communication.A pair of processes can communicate through a common channel and each act of communication con-sists simply of a signal being sent at one end of the channel and immediately being received at the other.A CCS speci?cation is a description(in the form of algebraic equations)of the behaviour expected from a system,based on the communication events that may occur.As in PDL,CCS has a set of operators (action pre?x,parallel composition,nondeterministic choice and restriction on acts of communication)that are used to inductively build process speci?cations from a set of basic actions.Iteration can also be described through the use of recursive equations.
This work presents three increasingly expressive Dynamic Logics in which the programs are CCS processes(sCCS-PDL,CCS-PDL and XCCS-PDL).Their goal is to reason about properties of concurrent programs and systems described using CCS.
There are,in the literature,some logics that make use of CCS or other process algebras.However,they use these process algebras as a language for the description of frames and models,while using standard modal logics for the description of properties(see,for example,[12]and[14]).The logics that we develop in the present work use CCS in a distinct way.Its operators and constructions are added to a basic modal logic in order to create dynamic logics that are suitable for the description and veri?cation of properties of commu-nicating,concurrent and non-deterministic programs and systems,in a similar way as PDL is used for the sequential case.
Thus,it should be emphasized that the contribution of this work is on the ?eld of dynamic logics and not on the?eld of process algebras.From process algebras,we just borrow a set of operators that are suitable for the description of communication and concurrency.We use these operators because they have a well-established theory behind them and we can use many of its concepts and results to help us build our logics.
Our paper falls in the broad category of works that attempt to generalize PDL and build dynamic logics that deal with classes of non-regular programs. As examples of other works in this area,we can mention[10],[9]and[11],that develop decidable dynamic logics for fragments of the class of context-free pro-grams and[16],[15]and[6],that develop dynamic logics for classes of programs with some sort of concurrency.Our logics have a close relation to two logics in this last group:Concurrent PDL with Channels[15]and the logic developed in [6].Both of these logics are expressive enough to represent interesting properties of communicating concurrent systems.However,neither of them has a simple Kripke semantics.The?rst has a semantics based on super-states and super-processes and its satis?ability problem can be proved undecidable(in fact,it is Π11-hard).Also,it does not have a complete axiomatization[15].The second makes a semantic distinction between?nal and non-?nal states,which makes its semantics and its axiomatization rather complex.On the other hand,due to the use of the CCS mechanisms of communication and concurrency,our logics have a simple Kripke semantics,simple and complete axiomatizations and the ?nite model property.
We choose to base our logics in the mechanisms of communication and con-currency of CCS,instead of some other process algebra,for two reasons.First, CCS is built with the philosophy that only those operators that are essential to the description of the basic behaviours of communication and concurrency
2
should be included as primitives in the language,while the operators and be-haviours of greater complexity should be derived from the basic https://www.doczj.com/doc/095589955.html,ing a small language like CCS,where only the more basic constructions are present, we can study in details what are the problems that may arise when we try to use its operators to build a dynamic logic and what operators and constructions we need to add or remove to correct these problems.Second,the development of CCS-based dynamic logics can be used as a natural stepping stone to the devel-opment of dynamic logics based on theπ-Calculus[13],a very powerful process algebra that is able to describe not only non-determinism and concurrency,but also mobility of processes.Theπ-Calculus can also be used to encode some pow-erful programming paradigms,as object-oriented programming and functional programming(λ-Calculus)[13].
The rest of this paper is organized as follows.In section2,we introduce the necessary background concepts:Propositional Dynamic Logic and the Calcu-lus for Communicating Systems.Our?rst logic(sCCS-PDL),together with a complete axiomatic system,is presented in section3.In this logic,we do not use constants or restriction in the CCS processes.In section4,we present our second logic(CCS-PDL),in which we allow the presence of constants in the CCS processes.We also give an axiomatization for this second logic and prove its completeness using a Fischer-Ladner construction.The third logic(XCCS-PDL),together with a complete axiomatization for it,is presented in section 5.In this logic,we extend CCS with some extra operators,which allows us to solve some issues that appear in the previous logics.Finally,in section6,we state our?nal remarks.
In the preliminary version of this work([2]),the contents of section5are completely absent and the concepts and proofs in section4are presented with far less details.Besides that,most of the motivations,discussions and detailed explanations that we present in this paper,trying to show what guided our choices in the construction of these logics,are also absent from[2].
2Background
This section presents two important subjects.First,we make a brief review of the syntax and semantics of PDL.Second,we present the process algebra CCS together with some useful concepts,properties and results from its theory.We do not assume a familiarity with CCS,since process algebras are by no means a universally studied topic among(modal)logicians.We introduce here all that is necessary for our presentation in the next sections,trying to make this work as self-contained as possible.
2.1Propositional Dynamic Logic
In this section,we present the syntax and semantics of PDL.
De?nition1.The PDL language consists of a setΦof countably many proposi-tion symbols,a setΠof countably many basic programs,the boolean connectives ?and∧,the program constructors;,∪and?and a modality π for every programπ.The formulas are de?ned as follows:
?::=p|?|??|?1∧?2| π ?,withπ::=a|π1;π2|π1∪π2|π?,
3
where p ∈Φand a ∈Π.
In all the logics that appear in this paper,we use the standard abbreviations ⊥≡??,?∨φ≡?(??∧?φ),?→φ≡?(?∧?φ)and [π]?≡? π ??.De?nition 2.A frame for PDL is a tuple F =(W,R a ,R π)where
?W is a non-empty set of states;
?R a is a binary relation for each basic program a ;
?R πis a binary relation for each non-basic program π,inductively built using the rules R π1;π2=R π1?R π2,R π1∪π2=R π1∪R π2and R π?=R ?π,where R ?πdenotes the re?exive transitive closure of R π.
De?nition 3.A model for PDL is a pair M =(F ,V ),where F is a PDL frame and V is a valuation function V :Φ→2W .
The semantical notion of satisfaction for PDL is de?ned as follows:
De?nition 4.Let M =(F ,V )be a model.The notion of satisfaction of a formula ?in a model M at a state w ,notation M ,w ?,can be inductively de?ned as follows:
?M ,w p i?w ∈V (p );
?M ,w ?always;
?M ,w ??i?M ,w ?;
?M ,w ?1∧?2i?M ,w ?1and M ,w ?2;
?M ,w π ?i?there is w ′∈W such that wR πw ′and M ,w ′ ?.
2.2Calculus for Communicating Systems
The Calculus for Communicating Systems (CCS)is a well known process alge-bra,proposed by Robin Milner [12],for the speci?cation of communicating con-current systems.It models the concurrency and interaction between processes through individual acts of communication.A CCS speci?cation is a description (in the form of algebraic equations)of the behaviour expected from a system,based on the communication events that may occur.For a broad introduction to CCS,[12]can be consulted.
In CCS,a pair of processes can communicate through a common channel and each act of communication consists simply of a signal being sent at one end of the channel and immediately being received at the other.
Let N ={a,b,c,...}be a set of names.Each channel in a CCS speci?cation is labelled by a name.The labels of the channels are also used to describe the communication actions (sending and receiving signals)performed by the processes,as is shown below.Besides these communication actions,CCS has only one other action:the silent action,denoted by τ,used to represent any internal action performed by any of the processes that does not involve an act of communication (e.g.:a memory update).
There are two possible semantics for the τaction in CCS:it can be regarded as being observable,in the same way as the communication actions,or it can
4
be regarded as being invisible.We adopt the ?rst one,since it is more generic.In our logical formalism,we are able to represent the second semantics as a particular case of the ?rst.
De?nition 5.In our presentation of CCS,process speci?cations can be built using the following operations:
P ::=α|α.P |α.A |P 1+P 2|P 1|P 2|P \L,
with
α::=a |
a ,called output action ,denotes
that the process sends a signal through the channel labelled by a .Finally,τdenotes the silent
action.
We write P α→P ′to express that the process P can perform the action α
and after that behave as P ′.We write P α→√to express that the process P successfully ?nishes after performing the action α(a notation borrowed from
ACP).A process only ?nishes when there is not any possible action left for it to perform.For example,β
β→√.When a process ?nishes
inside a
parallel
composition,
we write P instead of P |√.We also write √instead of √\L and
√|√.We de?ne the set L ={
Table1:Transition Relations of CCS
αα→√A def=P A Pα→P′Qβ→Q′
L
Pα→P′Qβ→Q′Pλ→P′,Q
P|Qτ→P′|Q′
In order to motivate the use of CCS,we present a simple example of the use of the language below.Here,we are still using CCS outside of the logical formalisms that are presented in the next sections.
Example1([12,17]).Consider a vending machine where one can put coins of one or two euro and buy a little or a big chocolate bar.After inserting the coins, one must press the little button for a little chocolate or the big button for a big chocolate.The machine is also programmed to shutdown on its own following some internal protocol(represented by aτaction).A CCS term describing the behaviour of this machine is the following:
V=1e.little.collect.A+2e.big.
collect.A+1e.1e.big.collect.A+τ
Let us now suppose that Chuck wants to use this vending machine.We could describe Chuck as
C=little.collect+1e.2e.
Theorem1(Expansion Law(EL)).Let P=P1|P2,where P is unrestricted. Then
P～
P1α→P′1α.(P′1|P2)+
P2β→P′2
β.(P1|P′2)+
R∈Aτ
τ.R,
where Aτ={(P′1|P′2):P1a→P′1and P2
a→P′1and P2a→P′2,for some a∈N}.We denote the right side of this bisimilarity by Exp(P).
2.3Action Sequences and Possible Runs
In this section,we introduce the key concept of?nite possible runs of a process. This concept plays a central role in the semantics of our logics.
De?nition9.We use the notation?→αto denote a potentially in?nite sequence of actionsα1.α2..···.αn(.···)(the empty sequence is denoted by?→ε).The empty sequence follows the rule?→α.?→ε=?→ε.?→α=?→α,for all?→α.We denote the i-th term of the sequence?→αby(?→α)i.
De?nition10.We say that a?nite sequence of actions?→βis a pre?x of?→αif there is a non-empty sequence?→λsuch that?→α=?→β.?→λ.If?→βis a pre?x of?→α, we write?→β??→α.
De?nition11.We write P
?→α?P′to express that the process P may perform the sequence of actions?→αand after that behave as P′.We write P?→α?√to express that the process P may successfully?nish after performing the sequence of actions?→α(this,in particular,implies that?→αis?nite).
De?nition12.We de?ne the set of?nite possible runs of a process P,denoted by?→R f(P),as?→R f(P)={?→α:P?→α?√}.
We want to de?ne semantics for our logics that only take into account the ?nite possible runs of the processes,i.e.,situations in which the processes suc-cessfully?nish.Thus,we present some useful results about?nite possible runs. De?nition13.Let R and S be sets of?nite sequences of actions.We can de?ne the following operations on these sets:
1.R?S={?→α.?→β:?→α∈R and?→β∈S};
2.R∪S={?→α:?→α∈R or?→α∈S};
3.R0={?→ε},R n=R?R n?1(n≥1);
4.R?= n∈N R n.
Lemma1.If P～Q,then P
?→α?√if and only if Q?→α?√.
Proof.We prove this by induction on the length n of?→α.If n=0,then?→α=?→εand neither P nor Q may successfully?nish without executing any action.If n=1,then?→α=α,for some actionα.Then,P?→α?√?Pα→√.By the hypothesis that P～Q,Pα→√?Qα→√.Finally,Qα→√?Q?→α?√.
7
Suppose that the theorem is true for all n Theorem 2.If P ～Q ,then ?→R f (P )=?→R f (Q ). Proof.Suppose that ?→α∈?→R f (P ).Then,P ?→α?√.As P ～Q ,this implies,by lemma 1,that Q ?→α?√,which means that ?→α∈?→R f (Q ).Thus,?→R f (P )??→R f (Q ).The proof that ?→R f (Q )??→R f (P )is entirely analogous.3sCCS-PDL This section presents our ?rst CCS-Based Dynamic Logic.In this logic,all the CCS processes that appear do not use constants or restriction.We call this logic Small CCS-PDL or sCCS-PDL.Our goal here is to introduce a simple logic and discuss some of the issues concerning the axioms and the relational interpretation of the formulas. 3.1Language and Semantics In this section,we present the syntax and semantics of sCCS-PDL. De?nition 14.The sCCS-PDL language consists of a set Φof countably many proposition symbols,a set N of countably many names,the silent action τ,the boolean connectives ?and ∧,the CCS operators .,+and |and a modality P for every process P .The formulas are de?ned as follows: ?::=p |?|??|?1∧?2| P ?,with P ::=α|α.P |P 1+P 2|P 1|P 2,where p ∈Φand α∈N ∪ N ∪{τ}. De?nition 16.A model for sCCS-PDL is a pair M =(F ,V ),where F is a sCCS-PDL frame and V is a valuation function V :Φ→2W . We now de?ne the semantical notion of satisfaction for sCCS-PDL as follows:De?nition 17.Let M =(F ,V )be a model.The notion of satisfaction of a formula ?in a model M at a state w ,notation M ,w ?,can be inductively de?ned as follows: 8 ?M,w p i?w∈V(p); ?M,w ?always; ?M,w ??i?M,w ?; ?M,w ?1∧?2i?M,w ?1and M,w ?2; ?M,w P ?i?there is a?nite path(v0,v1,...,v n),n≥1,such that v0=w,M,v n ?and there is?→α∈?→R f(P)of length n such that (v i?1,v i)∈Rβif and only if(?→α)i=β,for1≤i≤n.We say that such?→αmatches the path(v0,...,v n). If M,w ?for every state w,we say that?is globally satis?ed in the model M,notation M ?.If?is globally satis?ed in all models M of a frame F, we say that?is valid in F,notation F ?.Finally,if?is valid in all frames, we say that?is valid,notation ?.Two formulas?andψare semantically equivalent if ??ψ. As mentioned in the previous section,there are two possible semantics for theτaction in CCS:it can be regarded as being observable or as being invisible. In our logics,we adopt the?rst one,since we are able to represent the second semantics as a particular case of the?rst.In fact,to do that,the only thing that is necessary is to force,in the frames under consideration,Rτto be the relation Rτ={(w,w):w∈W}. Theorem3.?→R f(P)=?→R f(Q)if and only if P p? Q p. Proof.(?)Suppose that?→R f(P)=?→R f(Q),but P p? Q p.Then,we may assume,without loss of generality,that there is a model M and a state v0in this model such that M,v0 P p(*),but M,v0 Q p(**).By de?nition17,(*) implies that there is a path(v0,v1,...,v n),n≥1,in M such that M,v n p (***)and there is?→α∈?→R f(P)that matches this path.But as?→R f(P)=?→R f(Q), then?→α∈?→R f(Q).This and(***)imply,by de?nition17,that M,v0 Q p, contradicting(**). (?)Suppose that P p? Q p(*),but?→R f(P)=?→R f(Q).Then,we may assume,without loss of generality,that there is?→αsuch that?→α∈?→R f(P),but ?→α∈?→R f(Q).Let us build a frame F that consists solely of a path(v0,...,v n), n≥1,such that Rα={(v i?1,v i):1≤i≤n andαis the i-th term of?→α}. Let M=(F,V),such that v n∈V(p)and v i∈V(p),1≤i Corollary1.If P～Q,then P p? Q p. Proof.It follows directly from theorems2and3. We present some equalities between sets of?nite possible runs that are useful to the soundness proof of our axiomatization and to show why the null process 0is problematic. 9 Theorem 4.The following set equalities are true: 1.?→R f (α)={α}; 2.?→R f (α.P )=?→R f (α)??→R f (P ); 3.?→R f (P 1+P 2)=?→R f (P 1)∪?→R f (P 2). Proof.The proof is straightforward from table 1.Theorem 5.The following formulas are valid:1. α.P p ? α P p 2. P 1+P 2 p ? P 1 p ∨ P 2 p Proof.We only provide the proof for the ?rst formula.The proof for the second formula follows by an analogous line of reasoning,using the third equality in theorem 4instead of the second one. (?)Suppose that,for some model M and some state w in this model,M ,w α.P p .Then,by de?nition 17,there is a ?nite path (v 0,v 1,...,v n ),n ≥1,such that v 0=w ,M ,v n p and a sequence ?→α∈?→R f (α.P )that matches this path.Now,by the ?rst and second equalities in theorem 4,there is a sequence ?→β∈?→R f (P )such that ?→α=α.?→β.?→βmatches the path (v 1,...,v n ),which implies that M ,v 1 P p .Besides that,αmatches the path (v 0,v 1),which implies that M ,w α P p .Thus, α.P p → α P p is valid. (?)This proof is entirely analogous to the previous one,using the second equality in theorem 4in the reverse direction. Now it is possible to see why,as stated in the previous section,the use of the null process 0in our logics would be inconvenient.The problems that would appear come from the fact that,as described in [12],in a speci?cation of the form α.0,0is denoting a process that has successfully terminated,while in a speci?cation of the form P +0,0is denoting a deadlocked process.This double role cannot be kept in our logics without sacri?cing a very desirable property in a dynamic logic:the compositional semantics,illustrated in theorem 5. The compositional semantics is a direct consequence of the set equalities in theorem 4.But when we try to keep them in the presence of 0,some problems arise.?→R f (α.0)={α},since 0denotes successful termination in this case (if 0denoted a deadlock,then ?→R f (α.0)would be ?),and ?→R f (P +0)=?→R f (P ),since 0denotes a deadlock in this case (if 0denoted successful termination,then ?→R f (P +0)would be ?→R f (P )∪{?→ε}).To keep the second equality in theorem 4,we must have {α}=?→R f (α.0)=?→R f (α)??→R f (0),which implies that ?→R f (0)={?→ε}(*).On the other hand,to keep the third equality,we must have ?→R f (P )=?→R f (P +0)=?→R f (P )∪?→R f (0),which implies that ?→R f (0)=?(**). In the logical formalism,by theorem 5,(*)would imply that 0 φis se-mantically equivalent to φ,while (**)would imply that 0 φis semantically equivalent to ⊥.The crucial point in this situation is that we would have to either abandon at least one of the equalities in theorem 4,substituting it by a pair of equations,one for the case where P =0and the other for the case where P =0,or to somehow change the semantics so that the meaning of a 10 subformula of the form 0 φwill depend on the context in which it is inserted, being sometimes equivalent toφand sometimes to⊥.Both“solutions”would seriously compromise the compositionality of the semantics. We address this issue of the null process in our third logic,without intro-ducing any of the above problems.There,we rede?ne the process0so that it denotes only a deadlocked process,while de?ning a new way to denote termi-nation. 3.2Axiomatic System We consider the following set of axioms and rules,where p and q are proposition symbols and?andψare formulas. (PL)Enough propositional logic tautologies (K)?[P](p→q)→([P]p→[P]q) (Du)?[P]p?? P ?p (Pr)? α.P p? α P p (NC)? P1+P2 p? P1 p∨ P2 p (PC)If EL can be applied to P,then? P p? Exp(P) p (Sub)If??,then??σ,whereσuniformly substitutes proposition symbols by arbitrary formulas. (MP)If??and??→ψ,then?ψ. (Gen)If??,then?[P]?. It is important to notice that the theorems? P1+P2 p? P2+P1 p and ? P1|P2 p? P2|P1 p,which state the commutativity of the+and|operators, are derivable from the axiomatic system above. The axioms(PL),(K)and(Du)and the rules(Sub),(MP)and(Gen) are standard in the modal logic literature.The soundness of(Pr)and(NC) follows directly from the set equalities in theorem4and from de?nition17,as shown in theorem5.Finally,the soundness of(PC)follows from theorem1 and corollary1. The above axiomatic system is also complete with respect to the class of sCCS-PDL frames and the logic has the?nite model property.We omit the proofs here,because they are analogous to the proofs presented in section4, where constants are added to the language. 4CCS-PDL The logic presented in this section uses the same CCS operators as in the previ-ous section plus constants.This is the CCS-PDL logic.Our goal in this section is to build an axiomatic system for CCS-PDL and prove its completeness. 11 4.1Language and Semantics In this section,we present the syntax and semantics of CCS-PDL. De?nition18.The CCS-PDL language consists of a setΦof countably many proposition symbols,a set N of countably many names,the silent actionτ,the boolean connectives?and∧,the CCS operators.,+and|,a set C of countably many constants,such that each element of C has its unique correspondent de?n-ing equation,and a modality P for every process P.The formulas are de?ned as follows: ?::=p|?|??|?1∧?2| P ?,with P::=α|α.P|α.A|P1+P2|P1|P2, where p∈Φ,α∈N∪ However,due to the possibility of iterative behaviours,some set equalities may present themselves as recursive equations.In these cases,it is possible to obtain an equivalent non-recursive equality.First,the recursive equation can be rewritten,using the set equalities in theorem 4and equation (1),as ?→R f (P )=?→R f (P ′)??→R f (P )∪?→R f (Q ),where ?→R f (Q )is not a function of ?→R f (P ).Now,as all sequences in ?→R f (P ),?→R f (P ′)and ?→R f (Q )are ?nite and ?→ε∈?→R f (P ′),we may use a result known as Arden’s Rule,that states that if X ,A and B are sets of ?nite strings and the empty string is not in A ,then the equation X =A ?X ∪B has as its unique solution X =A ??B [1].Thus,?→R f (P )=?→R f ?(P ′)??→R f (Q ).De?nition 20.We say that a process P is a knot process if P =P A for some constant A with a recursive de?ning equation or if P =P 1|P 2where P 1or P 2is a knot process.Otherwise,we say that P is a non-knot process . De?nition 21.We call a non-empty sequence of actions ?→αa loop of a knot process P if P ?→α?P .We say that ?→αis a proper loop if ?→αis a loop and there is no ?→β??→α,with ?→α=?→β.?→λ,such that ?→βand ?→λare loops of P .The set of loops of P is denoted by Lo (P )and the set of proper loops of P is denoted by P Lo (P ). Theorem 6.?→α∈Lo (P )if and only if ?→α=?→α1.···.?→αn ,n ≥1,where ?→αi ∈P Lo (P ),for all i ∈{1,...,n }. Proof.The proof is straightforward from de?nition 21. De?nition 22.We call a sequence of actions ?→αa breaker of a knot process P if there is no ?→βsuch that ?→α??→βand ?→βis a loop.We say that ?→αis a proper breaker if ?→αis a breaker and there is no ?→β??→α,with ?→α=?→β.?→λ,such that ?→βis a loop and ?→λis a breaker.Finally,we say that ?→αis a minimal proper breaker if ?→αis a proper breaker and there is no ?→β??→αsuch that ?→βis a proper breaker.The set of breakers of P is denoted by Br (P ),the set of proper breakers of P is denoted by P Br (P )and the set of minimal proper breakers of P is denoted by MP Br (P ). Theorem 7.?→α∈P Br (P )if and only if ?→α=?→β.?→λ,where ?→β∈MP Br (P ). Proof.The proof is straightforward from de?nition 22. Using the concepts of loops and breakers,we can split a knot process P into two parts:the looping part ,denoted by L P ,and the tail part ,denoted by T P . L P = {?→α:?→α∈P Lo (P )}. and T P = {?→α.P ′:?→α∈MP Br (P )and P ?→α?P ′} Theorem 8.If P is a knot process,then ?→R f (P )=?→R f ?(L P )??→R f (T P ). Proof.We show that ?→R f (P )=?→R f (L P )??→R f (P )∪?→R f (T P ).The result then follows from Arden’s Rule [1],since ?→ε∈?→R f (L P ). 13 If ?→α∈?→R f (L P )??→R f (P ),then ?→α=?→β.?→λ,where ?→β∈?→R f (L P )and ?→λ∈?→R f (P ).Then,P ?→β?P and P ?→λ?√,which implies that P ?→α?√.Thus,?→α∈?→R f (P ).If ?→α∈?→R f (T P ),then ?→α=?→β.?→λ,where P ?→β?P ′and P ′?→λ?√,which implies that P ?→α?√.Thus,?→α∈?→R f (P ).This proves that ?→R f (L P )??→R f (P )∪?→R f (T P )??→R f (P ).If ?→α∈?→R f (P ),then we have two cases: 1.There is ?→β??→α,with ?→α=?→β.?→λ,such that ?→βis a loop.Then,by theorem 6,?→β=?→β1.?→β2,where ?→β1∈P Lo (P ).This means that ?→β1∈?→R f (L P ).If we make ?→γ=?→β 2.?→λ,then ?→α=?→β1.?→γand P ?→γ?√.Thus,?→γ∈?→R f (P )and ?→α∈?→R f (L P )??→R f (P ). 2.There is no ?→β??→α,with ?→α=?→β.?→λ,such that ?→βis a loop.This implies that,for all ?→β??→α,?→β∈P Br (P ).Then,by theorem 7,?→β=?→β1.?→β2,where ?→β1∈MP Br (P ).If we make ?→γ=?→β2.?→λ,then ?→α=?→β1.?→γ.This means that,if P ?→β1?P ′,then P ′?→γ?√.Thus,?→α∈?→R f (T P ). This proves that ?→R f (P )??→R f (L P )??→R f (P )∪?→R f (T P ).We also de?ne the process L ′P ,that is capable of iterating L P . L ′P = {?→α.Z P :?→α∈P Lo (P )}+L P ,where Z P is a new constant with de?ning equation Z P def =L ′P . The notions of frame,model and satisfaction are de?ned analogously to de?nitions 15,16and 17.It is not di?cult to see that theorem 3and corollary 1remain valid in CCS-PDL.4.2Axiomatic System The axiomatic system is similar to the one presented in section 3.2.We consider the following set of axioms and rules,where p ,q and r are proposition symbols and ?and ψare formulas. ?The axioms (PL),(K)and (Du)and the rules (Sub),(MP)and (Gen).?Axioms for knot processes: (Rec)? P p ? T P p ∨ L P P p (FP)?(r →([T P ]?p ∧[L P ]r ))∧[L ′P ](r →([T P ]?p ∧[L P ]r ))→(r → [P ]?p ) ?Axioms for non-knot processes: (sCCS)The axioms (Pr),(NC)and the rule (PC). (Cons)? α.A p ? α P A p 14 The proof of soundness is analogous to the proof of soundness for sCCS-PDL. The soundness of(Rec)and(FP)follows from theorems8and3.The axiom (FP)may seem strange at?rst,but it is just an adaptation of the so-called induction axiom to our particular situation.The soundness of(Cons)follows from equation(1)and theorem3. Theorem9(Completeness).Every consistent formula is satis?able in a?nite CCS-PDL model. Proof.The proof is presented in the appendix A. 5XCCS-PDL As it was shown in section3,the use of the null process0of CCS in our ?rst two logics would bring a serious inconvenience to their semantics:their compositionality would be compromised.This problem also a?ect our ability to include the restriction operator in these logics.Besides that,in CCS-PDL, we have to de?ne two distinct sets of axioms,depending on whether the process under consideration is a knot process or not. In this section,our goal is to solve these two problems that occur in the previous logics.In order to accomplish this,?rst we extend the language of CCS with new operators and a new type of action and slightly rede?ne its semantics.We call this new process algebra extended CCS or XCCS.Then,we de?ne a dynamic logic in which the programs are XCCS processes(XCCS-PDL). Because of the re?ned de?nition of the null process0in XCCS,we can include it in this logic,as well as the restriction operator.Besides that,one of the new operators of XCCS,the iteration operator,allows us to deal with all sorts of processes with just one set of axioms and to also drop the constants and all its elaborated theory from the language. 5.1XCCS In CCS,we have the set of actions A=N∪ a|τ, where a∈N and L?N. 0is the null process.It is a deadlocked process,since it is incapable of per-forming any running action and of successfully?nishing.END is process that 15 Table 2:Transition Relations of XCCS α.P α→P P ?END →√P ;Q α→P ′;Q P ;Q α→Q ′P +Q α→P ′P +Q β→Q ′P |Q α→P ′|Q P |Q β→P |Q ′λ→Q ′ P α→P ′P α→P ′,α∈L ∪P \L α→P ′\L P ;Q EN D →√P +Q EN D →√P +Q EN D →√ P EN D →√,Q EN D →√P \L EN D →√ z as its last action before termination and may not perform z or a )in P by b ( simpler and more convenient form of sequential composition and a simple form of iteration,as it is done in table2. Now,we need to make slight adjustments to the notion of strong bisimulation and to the Expansion Law. De?nition24.Let P be the set of all possible process speci?cations.A set Z?P×P is a strong bisimulation if(P,Q)∈Z implies,for allα∈A R,?If Pα→P′and P′∈P,then there is Q′∈P such that Qα→Q′and (P′,Q′)∈Z; ?If Qα→Q′and Q′∈P,then there is P′∈P such that Pα→P′and (P′,Q′)∈Z; and ?P END→√if and only if Q END→√. The de?nition of strong bisimilarity is analogous to de?nition7,using the new notion of strong bisimulation stated above. In the presence of the iteration operator,a weaker version of the Expansion Law is now su?cient for our needs. Theorem10(Expansion Law(EL)).Let P=P1|P2,where P is unrestricted and|does not occur in P1and P2.Then P～ P1α→P′1α.(P′1|P2)+ P2β→P′2 β.(P1|P′2)+ R∈Aτ τ.R+E P, where Aτ={(P′1|P′2):P1a→P′1and P2 a→P′1and P2a→P′2,for some a∈N}and E P=END,if P1END→√and P2END →√or E P=0,otherwise.Again,we denote the right side of this bisimilarity by Exp(P). Finally,because of the presence of the action END,we need to slightly adjust the de?nition of the composition R?S of two sets R and S of?nite sequences of actions. De?nition25.Let?(?→α)=?→λ,if?→α=?→λ.END and?(?→α)=?→α,otherwise. Then, R?S={?(?→α).?→β:?→α∈R and?→β∈S} Now,we de?ne some concepts that are useful to the axiomatization of our third logic. De?nition26.We say that a relation～=between processes is a congruence if it is an equivalence relation and it is preserved by all of XCCS operators,that is,if P～=Q,thenα.P～=α.Q,P+R～=Q+R and so on. De?nition27.A syntactic substitution of a restricted name by a fresh name (a name that does not occur in the process speci?cation)in a restriction set L and in every occurrence of the name in the scope of the correspondent restriction \L is called an alpha conversion. 17 De?nition28.Restriction congruence,or r-congruence,denoted by≡r,is a relation between processes de?ned by the following set of axioms and rules,where n(P)denotes the set of names that occur in P as part of both input and output actions. 1.It is a congruence; 2.It is closed under alpha conver- sion; 3.0\L≡r0; 4.END\L≡r END; 5.Ifα∈L∪ L,(α.P)\L≡r0;7.(P;Q)\L≡r(P\L);(Q\L); 8.(P+Q)\L≡r(P\L)+(Q\L); 9.If n(P)∩(L∪ L)=?,P\L≡r P. De?nition29.We say that a process is in r-external form if it has the form P\L,where P is unrestricted. Theorem11.Every process is r-congruent to a process in r-external form and every process with no occurrences of the|operator is r-congruent to an unrestricted process. Proof.The proof follows from de?nition28. Theorem12.If P≡r Q,then P～Q. Proof.The proof follows from table2and de?nition7. 5.2Language and Semantics In this section,we present the syntax and semantics of XCCS-PDL. De?nition30.The XCCS-PDL language consists of a setΦof countably many proposition symbols,a set N of countably many names,the silent actionτ,the ending action END,the boolean connectives?and∧,the XCCS operators.,;, +,|,?and\,a modality α for everyα∈N∪ N∪{τ}and L?N. De?nition31.A frame for XCCS-PDL is a tuple F=(W,{Rα},R END)where ?W is a non-empty set of states; ?Rα,for eachα∈N∪ The notion of model is de?ned analogously to de?nition16.We de?ne the semantical notion of satisfaction for XCCS-PDL as follows: De?nition32.Let M=(F,V)be a model.The notion of satisfaction of a formula?in a model M at a state w,notation M,w ?,can be inductively de?ned as follows: ?M,w p i?w∈V(p); ?M,w ?always; ?M,w ??i?M,w ?; ?M,w ?1∧?2i?M,w ?1and M,w ?2; ?M,w α ?i?there is w′∈W such that wRαw′and M,w′ ?,where α∈N∪ (SC)? P1;P2 p? P1 P2 p (Rec)? P? p?p∨ P P? p (FP)?p∧[P?](p→[P]p)→[P?]p (PCSub)If? P p? Q p,then? P|R p? Q|R p (RSub)If? P p? Q p,then? P\L p? Q\L p (Ard)If? P p? A;P+B p and A END →√,then? P p? A?;B p (Con)If P≡r Q,then? P p? Q p The proof of soundness is analogous to the proof of soundness for sCCS-PDL and CCS-PDL.The axioms(PL),(K)and(Du)and the rules(Sub), (MP)and(Gen)are standard in the modal logic literature.The soundness of (Pr),(NC),(0),(SC),(Rec),(FP),(PCSub),(RSub)and(Ard)follows from the set equalities in theorem13and theorem3.The soundness of(END) also follows from the two previous results with the help of de?nition31.The soundness of(PC)and(Con)follows from theorems10and12with the help of corollary1.The only rule that may require special attention is(PCSub). Theorem14.The rule(PCSub)is sound. Proof.By theorem13,?→R f(P1|P2)= {?→R f(?→α|?→β):?→α∈?→R f(P1)and?→β∈?→R f (P2)}.Now,suppose that P p? Q p,but P|R p? Q|R p.Then, by theorem3,?→R f(P)=?→R f(Q),but?→R f(P|R)=?→R f(Q|R).We may assume, without loss of generality,that there is?→λsuch that?→λ∈?→R f(P|R)(*),but ?→λ∈?→R f (Q|R)(**).(*)implies that there is?→α∈?→R f(P)and?→β∈?→R f(R)such that?→λ∈?→R f(?→α|?→β).But then?→α∈?→R f(Q),which implies that?→λ∈?→R f(Q|R), contradicting(**). De?nition33.We de?ne the following relation between processes:P?Q i?? P p? Q p. Theorem15.?is a congruence. Proof.This relation is clearly an equivalence relation and the axioms(Pr), (SC),(NC),(Rec)and(FP)and the rules(PCSub)and(RSub)enforce the preservation results needed to satisfy de?nition26. De?nition34.Let?k={P1,...,P k}be a set of processes such that P i≡r P j, if i=j.Let E(?k)={E1,...,E k}such that E i=(P i,T i),P i?T i,T i= j A i j;Q i j and,for all(i,j),A i j has no occurrence of|.We say that E(?k)is closed if,for all(i,j),Q i j∈?k. Theorem16.Let P=P1|P2,where P is unrestricted.Then P? P has no occurrence of the|operator. 20 RLC电路的动态和频率特性综合研究 ——电路分析研讨 学院：电子信息工程学院 RLC 电路的动态特性和频率特性综合研究 谐振频率和电压的关系 谐振频率的概念 如图所示，二阶RLC 串联电路，当外加正弦电压源的为某一个频率时， 端口阻抗 呈现为纯电阻性，称电路对外加信号频率谐振。 1:以输入电压为参考相量，写出谐振时各电压的幅度和相位。用仿真软件测量 谐振时各电压有效值。改变电阻值分别为10、20、30时，仿真测量各电压有 效值有什么变化？ 对图1所示的RLC 串联组合，可写出其阻抗为: R j(wL 三)R j(X L X C ) R jX wC 1 谐振的条件是复阻抗的虚部为零，即： X L X C =O , w L = wC ， w 丄 f 1_ 可解得： LC 或 2 LC （1）理论值分析： 我们在此取 V 2CM f 10KHz L 1 1mH C 1 253nF 然后通过改变电阻F 来研究各电压有效值的变化 ①电阻值R=10时, 谐振角频率为0 Z R jwL 1 jwC 1 图1 I V V 2A 1 R jwL 1R v I jwC C j2 fC V L I j2 fL j125.66V V R I R20V ②电阻值R=20时 I V V 1A 1 R jwL 1R V I jwC C j2 fC j125.81V V L I j2 fC j 62.83V V R ②电阻值R=30时 , v V 2 A I A R jwL 1 R 3I V C jwC j2 fC V L I j2 fC j41.89V j 62.91V I R 20V j41.94V R 20V (2)电路仿真如下: ①电阻值R=10时 2?3r*F 1 mH (^^20W1DkHz/0Deg ----------------- Il “羽Al 山西大学 物理电子工程学院实验论文 半导体激光器稳频系统的动态特性研究 学院：物理电子工程学院 专业：光信息科学与技术 导师：王彦华 姓名：杜小娇任思宇 学号：2013274002 20132740 半导体激光器稳频系统的动态特性研究 摘要：本实验在现代社会中自动控制系统技术的启发下，考虑到目前激光技术的发展前景广阔，应用也比较广泛，决定将用类似的方法研究激光器稳频系统的动态特性。在闭环系统中通过不同干扰信号的扰动，观察整个系统的响应，最终得到传递函数，进而分析出该系统的幅频和相频特性。关键字：激光器稳频系统干扰信号传递函数幅频特性相频特性 （一）引言 提高激光器系统稳定性在激光技术、超精密加工、测量设备量子信息等诸多科技前沿领域有着举足轻重的地位。影响激光系统稳定性的因素有很多，例如激光器、气压、震动等。如果激光器系统的稳定性提高到十几个小时乃至更高，那么对于恶劣环境的干扰就可以得以消除，更有利于实验的进行。对于激光器稳定性的研究更显得尤为重要，在激光器输出功率稳定性[1-2]的系统中，都实现了激光器输出功率的长期稳定性。在山西大学[3-6]也有很多实验需要建立在稳定系统来进一步发展。二阶闭环系统稳定的研究过程中针对信号及信号处理[7-8]已经有了较为成熟的一系列体系。因此，结合自动控制理论研究激光器系统及其动态响应，以实验结果为依据，对特定环境下激光器的结构设计的优化以及环路的参数的确定和调试，进行数学建模，从而提供更科学的处理方案，并给出一些的针对性的建议是非常重要的研究工作。 （二）实验原理 2.1半导体激光器（ECDL） 激光器的种类很多，分类的依据也有很多。其中根据其增益介质的不同可分为气体激光器、固体激光器、光纤激光器、染料激光器以及半导体激光器。半导体激光器因其结构紧凑、操作简单、便于集成、价格低廉、功耗低、工作波长范围大等优点而被广泛应用于冷原子物理、量子操控等前沿研究和高分辨率光谱，高精度测量很多技术领域。因此实验中将对半导体激光器稳定性进行了研究与分析。 我们在实验中为了更好控制半导体中发光二极管发出的光经谐振腔不断放大后发射出激光的不同模式，采用了光栅反馈式选模。光栅对激光有色散的作用，进而不同波长的波可以清楚辨别，通过调节光栅的角度，进而可以实现不同频率的激光反馈回激光器中。 IGBT的动态特性与静态特性的研究 IGBT动态参数 IGBT模块动态参数是评估IGBT模块开关性能如开关频率、开关损耗、死区时间、驱动功率等的重要依据，本文重点讨论以下动态参数：模块内部栅极电阻、外部栅极电阻、外部栅极电容、IGBT寄生电容参数、栅极充电电荷、IGBT开关时间参数，结合IGBT模块静态参数可全面评估IGBT芯片的性能。RGint：模块内部栅极电阻: 为了实现模块内部芯片均流，模块内部集成有栅极电阻。该电阻值应该被当成总的栅极电阻的一部分来计算IGBT驱动器的峰值电流能力。 RGext：外部栅极电阻： 外部栅极电阻由用户设置，电阻值会影响IGBT的开关性能。 上图中开关测试条件中的栅极电阻为Rgext的最小推荐值。 用户可通过加装一个退耦合二极管设置不同的Rgon和Rgoff。 已知栅极电阻和驱动电压条件下，IGBT驱动理论峰值电流可由下式计算得到，其中栅极电阻值为内部及外部之和。 实际上，受限于驱动线路杂散电感及实际栅极驱动电路非理想开关特性，计算出的峰值电流无法达到。 如果驱动器的驱动能力不够，IGBT的开关性能将会受到严重的影响。 最小的Rgon由开通di/dt限制，最小的Rgoff由关断dv/dt限制，栅极电阻太小容易导致震荡甚至造成IGBT及二极管的损坏。Cge：外部栅极电容： 高压IGBT一般推荐外置Cge以降低栅极导通速度，开通的di/dt及dv/dt被减小，有利于降低受di/dt影响的开通损耗。 IGBT寄生电容参数： IGBT寄生电容是其芯片的内部结构固有的特性，芯片结构及简单的原理图如下图所示。输入电容Cies及反馈电容Cres是衡量栅极驱动电路的根本要素，输出电容Coss限制开关转换过程的dv/dt，Coss造成的损耗一般可以被忽略。 Nature Communications 10.742，综合：一区，12.124 Nucleic Acid Research 8.808，生物：一区；10.162 Scientific Reports 5.078，综合类：二区，4.259 Methods 3.221，生物，二区，3.802 BMC Systems Biology 2.853，生物：3区，2.003 Journal of Biomedical informatics 2.482，医学：3区；2.753 Journal of Computational Biology 1.670，生物：四区；1.032 Journal of Bioinformatics and Computational Biology 0.931，生物：四区；0.800 Journal of Theoretical Biology1.833 生物、数学与计算生物学三区 Journal of Mathematical Biology 1.786 生物4区数学与计算生物学3区Bioinformatics (IF: 4.328) BMC Bioinformatics (IF: 3.781)，生物：三区；2.448 BMC Biology (IF: 4.734)，生物：一区；6.779 Briefings in Bioinformatics (IF: 4.627)，生物：一区；5.134 Journal of Computational Biology (IF: 1.563)，生物：四区；1.032 PLoS Computational Biology (IF: 5.895)，生物：二区，2.542 Mathematical Biosciences (IF: 1.148)，生物：四区；1.246 Journal of Biomedical Informatics (IF: 1.924)，医学：三区；2.753 Molecular Biosystems ( IF: 4.236)，生物：三区；2.781 Frontiers in Genetics 4.151 生物二区 Microbial Ecology 3.614 生物：二区，微生物3区 9 RC 一阶电路（动态特性 频率响应） 一个电阻和一个电容串联起来的RC 电路看起来是很简单的电路。实际上其中的现象已经相当复杂，这些现象涉及到的概念和分析方法，是电子电路中随处要用到的，务必仔细领悟。 9.1 零输入响应 1.电容上电压的过渡过程 先从数学上最简单的情形来看RC 电路的特性。在图9.1 中，描述了问题的物理模型。假定RC 电路接在一个电压值为V 的直流电源上很长的时间了，电容上的电压已与电源相等（关于充电的过程在后面讲解），在某时刻t 0突然将电阻左端S 接地，此后电容上的电压会怎么变化呢？应该是进入了图中表示的放电状态。理论分析时，将时刻t 0取作时间的零点。数学上要解一个满足初值条件的微分方程。 看放电的电路图，设电容上的电压为v C ,则电路中电流 dt dv C i C =， 依据KVL 定律，建立电路方程： 0=+dt dv RC v C C 初值条件是 ()V v C =0 像上面电路方程这样右边等于零的微分方程称为齐次方程。 设其解是一个指数函数： ()t C e t v S K = K 和S 是待定常数。 代入齐次方程得 0=KS +K S S t t e RC e 约去相同部分得 0=S +1RC 于是 RC 1-=S 齐次方程通解 ()RC t C e t v -K = 还有一个待定常数K 要由初值条件来定： ()V K Ke v C ===00 最后得到： () t RC t C Ve Ve t v --== 在上式中，引入记号RC =τ，这是一个由电路元件参数决定的参数，称为时间常数。它有什么物理意义呢？ 在时间t = τ 处， ()V V Ve v 0.368=e ==-1-C τττ 时间常数 τ是电容上电压下降到初始值的1/e ＝36.8% 经历的时间。 当t = 4 τ 时，()V v 0183.0=4C τ，已经很小，一般认为电路进入稳态。 数学上描述上述物理过程可用分段描述的方式，如图9.1 中表示的由V 到0的“阶跃波”的输入信号，取开始突变的时间作为时间的0点，可以描述为： ()()0=S ≤t V t v 对 ；()()00=S ≥t t v 对。 [练习.9.1]在仿真平台上打开本专题电路图，按图中提示作出“零输入响应”的波形图。观察电容、电阻上输出波形与输入波形的关系，由图上读出电路的时间常数值，与用电路元件值计算结果比较。 仿真分析本专题电路 得到波形图如图9.2 所示。 在0到1m 这时间内，电压源值为V ，在时刻1m 时电压源值突然变到0。仿真平台在对电路做瞬态分析之前，对电路作了直流分析，因此图中1m 以前一段波形只是表明电路已经接在电压源值为V “很长时间”后的持续状态。上面理论分析只适用于1m 以后的时间过程。时刻1m 是理论分析的时间“零”点。图上看到，电容上的电压随时间在下降，曲线的样子是指数下降曲线的典型模样。由v C 曲线找到电压值为0.368V 的地方，读出它的时刻值(=2m )，即可求到电路的时间常数是1m (1毫秒)。 图中也画出电阻上电压变化曲线。观察，发现在1m 以前，电阻电压为0，在时刻1m ，电阻电压突变到 -V ，然后逐渐升到0。怎样理解这个过程呢？ 2.电阻上电压的过渡过程 虽然专题电路图中取电阻的电压时是由电阻直接落地的电路得到的，但电路元件参数是相同的，该电阻上的电压应和电容落地电路中的电阻是一样的。按照这种想法，看图9.1 ，注意电阻的电压的参考方向应是由S 点向右，即应是v(S 点)-v C ，在电源电压为V 的时间内，电容已被充电到v C =V ，那么v R = v(S 点)-v C =V -V =0。在理论分析时间0处，电压源的电压值突变到0，即v(S 点)=0，但电容上的电压不能突变（回顾电容的特性：电压有连续性）。为了区分突变时刻的前和后的状态，用0- 表示突变前，0+ 表示突变后。 即是说， v C (0+)= v C (0-)=V 那么， v R (0+)= 0-v C (0+)= -V 在随后的时间内，按KVL 定律， 电阻上的电压应为： ()()τt RC t C R Ve Ve t v t v ---=-=-= 一、为了说明问题更有条理，我先对SCI/EI收录的会议论文进行说明： （1）EI收录主要收录在期刊上发表的国际会议和国际会议论文集。其中会议论文集、专著等。其中IEE/IEEE、SPIE、ASME、ASCE 等学会的国际会议论文集几乎全部收录。 （2）SCI、SSCI主要收录在期刊上发表的国际会议，如国际会议专刊、增刊，并收录在期刊上刊登的国际会议摘要。SCI、SSCI不收录国际会议论文集（图书）。 （3）ISTP、ISSHP主要收录在专著、期刊、报告、增刊及预印本等形式出版的各种一般会议、座谈、研究会和专题讨论会的会议录文献，包括CD-ROM，EI收录的会议ISTP不一定收录。 （4）部分会议会ISTP、ISSHP被同时收录。 二、对近来部分会议声称能被会议出版的说明： 近来有大量的会议声明能够被一些期刊，如AMR《Advanced Materials Research》，等期刊正刊出版，并且能够被EI检索，对此，大家要注意了，这里鱼目混杂，要擦亮眼睛注意： （1）AMR《Advanced Materials Research》，等这些刊物确实能够被EI检索，因为这几个刊物都是专门接受会议投稿的，也就是专门收录会议论文的，不接受作者的单独投稿。只要能被这个刊物收录可以说就一定能被EI检索，除非你的论文有重大的格式错误，但注意检索类型是CA类型（也就是会议论文）。 （2）论文能否进入这几个刊物，关键就是看你参加的会议是否能够属于刊物的会议列表里，最简单的方法是进入https://www.doczj.com/doc/095589955.html,/网站，输入你要查询的会议名称，如果该会议能够在此网站上查的到，才证明你的论文能够被该刊物收录，也就说明你的论文能够被Ei检索。 （3）这几个刊物都是属于瑞士TTP出版公司旗下的刊物，其旗下的刊物还有如下刊物，这些刊物上发表的文章都能被EI检索：MSF>Materials Science Forum KEM>Key Engineering Materials SSP>Solid State Phenomena DDF>Defect and Diffusion Forum AMM>Applied Mechanics and Materials AMR>Advanced Materials Research AST>Advances in Science and Technology JNanoR>Journal of Nano Research JBBTE>Journal of Biomimetics, Biomaterials, and Tissue Engineering JMNM>Journal of Metastable and Nanocrystalline Materials JERA>International Journal of Engineering Research in Africa （4）Key Engineering Materials 《关键工程材料》瑞士 简述系统动态特性及其测定方法 系统的特性可分为静态特性和动态特性。其中动态特性是指检测系统在被测量随时间变化的条件下输入输出关系。一般地，在所考虑的测量范围内，测试系统都可以认为是线性系统，因此就可以用一定常线性系统微分方程来描述测试系统以及和输入x (t)、输出y (t)之间的关系。 1) 微分方程：根据相应的物理定律（如牛顿定律、能量守恒定律、基尔霍夫电 路定律等），用线性常系数微分方程表示系统的输入x 与输出y 关系的数字方程式。 a i 、 b i (i=0,1,…)：系统结构特性参数，常数，系统的阶次由输出量最高微分阶次决定。 2) 通过拉普拉斯变换建立其相应的“传递函数”，该传递函数就能描述测试装 置的固有动态特性，通过傅里叶变换建立其相应的“频率响应函数”，以此来描述测试系统的特性。 定义系统传递函数H(S)为输出量与输入量的拉普拉斯变换之比，即 式中S 为复变量，即ωαj s += 传递函数是一种对系统特性的解析描述。它包含了瞬态、稳态时间响应和频率响应的全部信息。传递函数有一下几个特点： （1）H(s)描述系统本身的动态特性，而与输入量x (t)及系统的初始状态无关。 （2）H(S)是对物理系统特性的一种数学描述，而与系统的具体物理结构无关。H(S)是通过对实际的物理系统抽象成数学模型后，经过拉普拉斯变换后所得出的，所以同一传递函数可以表征具有相同传输特性的不同物理系统。 （3）H(S)中的分母取决于系统的结构，而分子则表示系统同外界之间的联系，如输入点的位置、输入方式、被测量以及测点布置情况等。分母中s 的幂次n 代表系统微分方程的阶数，如当n =1或n =2 时，分别称为一阶系统或二阶系统。 一般测试系统都是稳定系统，其分母中s 的幂次总是高于分子中s 的幂次(n>m)。 2009年8月Power System Technology Aug. 2009 文章编号：1000-3673（2009）16-0058-05 中图分类号：TM761 文献标志码：A 学科代码：470·40 电力系统功率频率动态特性研究 周海锋1，倪腊琴2，徐泰山1 （1．国网电力科学研究院，江苏省南京市 210003；2．华东电力调度中心，上海市黄浦区 200002） Study on Power-Frequency Dynamic Characteristic of Power Grid ZHOU Hai-feng1，NI La-qin2，XU Tai-shan1 （1．State Grid Electric Power Research Institute，Nanjing 210003，Jiangsu Province，China； 2．East China Grid Dispatching Center，Huangpu District，Shanghai 200002，China） ABSTRACT: Power-frequency characteristics of power grid are the base of the research on system operation modes, design of under-frequency load shedding and evaluation on various frequency and voltage regulation measures. Along with the enlargement of power grid scale, the power-frequency characteristics become complicated increasingly. Based on actual data of practical power grids and by use of numerical simulation, the dynamic power-frequency characteristics of power grid are researched, the space-time distribution features of power grid frequency and the factors impacting power-frequency characteristics are analyzed and the main factors that impact initial stage of frequency, dynamic process of frequency and steady-state value of frequency are given respectively. KEY WORDS: power-frequency characteristic；power shortage；spinning reserve；load frequency coefficient；load model 摘要：电力系统功率频率特性是研究系统运行方式、设计低频减载方案以及评价各种调频调压措施等工作的基础。随着电网规模的扩大，电力系统功率频率特性日趋复杂。文中以实际电网数据为基础，采用数值仿真法研究电网的功率频率动态特性，分析了电网的频率时空分布特性以及功率频率特性的影响因素，并分别给出了影响频率初始阶段、频率动态过程以及频率稳态值的主要因素。 关键词：功率频率特性；功率缺额；旋转备用；频率调节效应系数；负荷模型 0 引言 频率是电力系统的重要参数，也是衡量电能质量的主要指标之一[1]。当电力系统受到大机组跳闸、联络线跳线或者大容量负荷投切等扰动时，由于系统有功功率平衡遭到破坏，引起系统频率发生变化继而发生频率动态过程。当系统频率变化较大时，将会给电力系统带来明显的不利影响，甚至导致频率稳定破坏事故的发生。 低频减载[2-5](under-frequency load shedding，UFLS)作为保障电网安全稳定运行3道防线[6]中的最后一道防线，是防止电力系统发生频率崩溃的紧急控制措施。正确认识电力系统功率频率特性是研究系统运行方式、整定低频减载方案和评价各种调频调压措施等工作的基础。尽管互联系统的容量越来越大，发生全局性频率崩溃的概率越来越小，但一旦发生后果将更加严重。因此深入研究电力系统功率频率特性、分析影响系统功率频率特性的因素，对电力系统的规划、运行及控制具有重要的理论和现实意义。 电力系统功率频率特性研究主要采用解析分析[7]和数值仿真[8-9]2种方法。解析分析法主要采用非均匀线性动态等值，侧重对扰动后系统各区频率动态过程的空间分布现象及特点的分析。数值仿真法可以得到系统精确的受扰轨迹，不仅有助于解释多机系统中功率频率特性的一般规律，还能评价系统中负荷电压特性及各种控制措施对频率动态过程的影响，但是数值仿真法对系统模型及参数选择的依赖性较大。 本文将在研究电力系统功率频率特性机理的基础上，采用数值仿真法揭示电网的频率时空分布特性以及影响互联大电网功率频率特性的主要因素。 1 电力系统功率频率特性 1.1 基本概念 电力系统功率频率特性是指系统有功功率不平衡时频率的变化特性，它是负荷频率特性、发电机频率特性以及电压影响的综合结果[10]。通常将其分为功率频率静态特性和功率频率动态特性，分别描述有功功率变化之后频率的状态和变化过程。其 第三章 系统频率特性 系统的时域分析是分析系统的直接方法，比较直观，但离开计算机仿真，分析高阶系统是困难的。系统频域分析是工程广为应用的系统分析和综合的间接方法。频率分析不仅可以了解系统频率特性，如截止频率、谐振频率等，而且可以间接了解系统时域特性，如快速性，稳定性等，为分析和设计系统提供更简便更可靠的方法。 本章首先阐明频率响应的特点，给出计算频率响应的方法，接着介绍Nyquist 图和Bode 图的绘制方法、系统的稳定裕度及系统时域性能指标计算。 3.1 频率响应和频率特性 3.1.1 一般概念 频率响应是指系统对正弦输入的稳态响应。考虑传递函数为G(s)的线性系统，若输入正弦信号 t X t x i i ωsin )(= (3.1-1) 根据微分方程解的理论，系统的稳态输出仍然为与输入信号同频率的正弦信号，只是其幅值和相位发生了变化。输出幅值正比于输入的幅值i X ，而且是输入正弦频率ω的函数。输出的相位与i X 无关，只与输入信号产生一个相位差?，且也是输入信号频率ω的函数。即线性系统的稳态输出为 )](sin[)()(00ω?ωω+=t X t x (3.1-2) 由此可知，输出信号与输入信号的幅值比是ω的函数，称为系统的幅频特性，记为)(ωA 。输出信号与输入信号相位差也是ω的函数，称为系统的相频特性，记为)(ω?。 幅频特性： )()()(0ωωωi X X A = (3.1-3) 相频特性： )()()(0ω?ω?ω?i -= (3.1-4) 频率特性是指系统在正弦信号作用下，稳态输出与输入之比对频率的关系特性，可表示为： )()()(0ωωωj X j X j G i = (3.1-5) 频率特性)(ωj G 是传递函数)(s G 的一种特殊形式。任何线性连续时间系统的频率特性都可由系统传递函数中的s 以ωj 代替而求得。 )(ωj G 有三种表示方法： )()()(ω?ωωj e A j G = (3.1-6) )()()(ωωωjV U j G += (3.1-7) )(sin )()cos()()(ω?ωωωωjA A j G += (3.1-8) 式中，实频特性： )(cos )()(ω?ωωA U = 虚频特性： 第6 章频率特性测试仪 6．1 概述 频域测量是把信号作为频率的函数进行分析，主要讨论线性系统频率特性的测量和信号的频谱分析。 主要仪器：频率特性测试仪；外差式频谱分析仪；失真度测试仪。 6．2 线性系统频率特性的测量 6．2．1 测量方法 1、点频测量法 是一种静态测量方法，比较繁琐。 2、扫频测量法 是一种动态测量方法，较好。 6．2．2频率特性测试仪的工作原理 是根据扫频测量法的原理设计、制造而成的。它是将扫频信号源及示波器的X--Y显示功能结合为一体，用于测量网络的幅频特性。 1、基本工作原理 扫频仪的原理框图如图所示： 扫描电压发生器产生的扫描电压既加至X轴，又加至扫频信号发生器。 2、扫频信号发生器的主要共作特性 3、产生扫频信号的方法 4、频标电路 6．3 频谱分析仪 要求： 重点掌握频谱分析的基本内容、频谱分析仪的分类方法和分类；了解各种信号的付氏变换及信号频谱的特性 6.3.1 频谱分析的基本概念 广义上，信号频谱是指组成信号的全部频率分量的总集，频谱测量就是在频域内测量信号的各频率分量，以获得信号的多种参数。狭义上，在一般的频谱测量中常将随频率变化的幅度谱称为频谱。对信号进行频域分析就是通过研究频谱来研究信号本身的特性。从图形来看，信号的频谱有两种基本类型：①离散频谱，又称线状谱线；②连续频谱。实际的信号频谱往往是上述两种频谱的混合。 1） 信号频谱分析的内容 信号的频谱分析包括对信号本身的频率特性分析，如对幅度谱、相位谱、能量谱、功率谱等进行测量，从而获得信号在不同频率上的幅度、相位、功率等信息；还包括对线性系统非线性失真的测量，如测量噪声、失真度、调制度等。 2） 频谱分析仪的基本原理 频谱分析仪就是使用不同方法在频域内对信号的电压、功率、频率等参数进行测量并显示的仪器。一般有FFT 分析（实时分析）法、非实时分析法两种实现方法。非实时分析方式有扫频式、差频式（或外差式）两种。外差式分析是频谱仪最常采用方法。 3） 频谱分析仪的分类 按照分析处理方法的不同，可分为模拟式频谱仪、数字式频谱仪和模拟/数字混合式频谱仪；按照基本工作原理，可分为扫描式频谱仪和非扫描式频谱仪；按照处理的实时性，可分为实时频谱仪和非实时频谱仪；按照频率轴刻度的不同，可分为恒带宽分析式频谱仪、恒百分比带宽分析式频谱仪；按照输入通道的数目，可分为单通道、多通道频谱仪；按照工作频带的高低，可分为高频、射频、低频等频谱仪……等等。 6.3.2 外差式频谱仪 外差式频谱仪是目前应用最广泛的一种频谱仪，它利用无线电接收机中普遍使用的自动调谐方式，通过改变本地振荡器的频率来捕获欲接收信号的不同频率分量。其频率变换原理与超外差式收音机的变频原理完全相同，只不过把扫频振荡器用作本振而已，所以也被称为扫频外差式频谱仪。在高频段扫频外差式占据优势地位。 1） 外差式频谱仪的组成 原理框图如图所示，主要包括输入通道、混频电路、中频处理电路、检波和视频滤波等部分。 外差式频谱仪 外差式频谱分析仪频率范围宽、灵敏度高、频率分辨率可变，是目前频谱仪中数量最大的一种，尤其在高频段应用更多。但由于本振是连续可调的，被分析的频谱依次被顺序采样，因此外差式频谱分析仪不能实时分析信号的频谱。 2） 输入通道 频谱仪输入通道的作用是控制加到仪器后续部分上的信号电平，并对输入的信号取差频以获得固定中频。输入通道主要由输入衰减、低噪声放大、低通滤波及混频等几部分组成，功能上等同于一台宽频段、窄带宽的外差式自动选频接收机，所以也叫接收部分。 外差式接收机使用混频器将输入信号频率变换到固定的中频上，如下式所示： I X L f f n f m =?±? 其中f L 为本振频率，f X 为被转换的输入信号频率，f I 为中频信号频率，m 、n 表示谐波的次数，可取值1、2、……。如果仅考虑输入信号和本振的基频，即取m = n = 1时，上式简化成 I X L f f f =± 如何查询期刊影响因子 影响因子是一个国际上通行的期刊评价指标，表示期刊影响力大小。近年来，科研工作者越来越重视期刊的影响因子。那么，怎么查询期刊的影响因子呢？ 首先，查询影响因子要知道具体的查询地址，外文期刊和中文期刊的查询地址不同。 1、查询外文期刊影响因子，可使用外文数据库Web of Science中的JCR，其中JCR Science Edition 用于查询自然科学类期刊，JCR Social Sciences Edition 用于查询人文社会科学类期刊。 2、查询中文期刊的影响因子，可使用中国学术期刊（光盘版）电子杂志社和中国科学文献计量评价中心联合推出的《中国学术期刊综合引证报告》（万锦堃主编，科学出版社）。有需要的读者请到图书馆咨询部查询。 其次，查询影响因子必需知道期刊缩写名，这个有很多规则，具体如下： 1.单个词组成的刊名不得缩写 部分刊名由一个实词组成，如Biomaterials，nature，science等不得缩写。 2.刊名中单音节词一般不缩写 英文期刊中有许多单音节词，如FOOD，CHEST，CHILD，这些词不得缩写。如医学期刊hearand lung, 缩写为Heart Lung,仅略去连词and.但少数构成地名的单词，如NEW，SOUTH等，可缩写成相应首字字母。如New England Journal of Medcine,可缩写为N Engl J Med,不应略为New Engl J Med，South African Journal of Surgery可缩写为S Afr J Surg,不可缩写为South Afr J Surg.另外，少于5个字母(含5个字母)的单词一般不缩写，如Acta,Heart,Bone,Joint等均不缩写。 3.刊名中的虚词一律省略 4.6 频率特性与系统的动态性能 4.6 频率特性与系统的动态性能 控制系统的频率特性与系统的动态性能之间有密切的关系。分析控制系统的动态特性，可以利用开环频率特性，也可以利用闭环频率特性。二阶系统的频率特性与动态性能的时域指标之间又确定的关系，而高阶系统则不存在确定的函数关系。 4.6.1 开环频率特性与系统的动态响应 若把系统的开环对数频率特性划分为低频段，中频段和高频段，这三部分对控制系统动态过程的影响是不同的。开环频率特性的低频段主要影响阶跃响应动态过程的最后阶段，而开环频率特性的高频段主要影响阶跃响应动态过程的起始阶段。对动态性能影响最重要的是中频段。所以，常用开环频率的低频段估计系统的稳态性能，而用中频段估计系统的动态响应。 开环频率特性的低频段通常指第一个转折频率前的频段。这一频段的对数幅频特性质取决于系统的积分环节和放大系数。图4.29是开环频率特性低频段的几种情况。 图4.29 开环频率特性的低频段 图 4.29(a)所示的系统低频段是平行于横轴的直线。这说明系统中不含积分环节，是零型系统。这种系统的单位阶跃响应是有误差的，而且可以根据对数幅频特性确定放大系数K,从而计算出系统的稳态误差。 图4.29（b）所示的系统，由于低频段的斜率为-20dB/十倍频程，可以断定系统含有一个积分环节，是Ⅰ型环节。系统的放大系数可在处求得。稳态误差 可按Ⅰ型系统计算。 图4.29(c)所示的系统是Ⅱ型系统，系统的放大系数可按求取或在对数幅 频特性曲线-40dB/十倍频程与轴的交点处求取，此时有。系统的稳态误差按Ⅱ型系统的稳态误差计算。 开环频率特性曲线的中频段是截止频率附近的频段，截止频率就是使 的频率。即幅值曲线穿越零分贝线的频率。这一频段，对数幅频特性的形状直接影响到系统的稳定裕量。从而对系统动态响应过程的主要性能指标产生影响。用开环频率特性中频段评价控制系统的动态性能，常用到的就是截止频率（穿越频率）和相位裕量。和与二阶系统动态时域指标有如下关系 (4.46) (4.47) 对于高阶系统，开环频率特性的与时域指标没有确定的关系。有不少适用于 各种情况的经验公式，可以近似计算出动态性能的时域指标。有兴趣的同学可以查阅其他书籍做更深入地了解。 4.6.2 闭环频率特性与系统的动态性能 控制系统的闭环频率特性可以通过闭环传递函数直接求得。也可以通过开环频率特性得到。 对于单位反馈控制系统，设开环频率特性为，则闭环频率特性为 工程上常用图解法根据开环频率特性绘制闭环频率特性。用计算机绘制闭环频率特性，既精确又快捷，已经获的广泛的应用。 用闭环频率特性分析系统的动态性能，主要依据是闭环幅频特性，图4.30是典型的闭环幅频特性曲线。 序号期刊名称主办单位影响因子 1 浙江社会科学浙江社会科学界联合会0.485 2 求是学刊黑龙江大学0.312 3 社会科学上海社会科学院0.455 4 社会科学辑刊辽宁省社会科学院0.244 5 武汉大学学报(人文科学版) 武汉大学0.194 6 湖南师范大学社会科学学报湖南师范大学0.327 7 福建论坛(人文社会科学版) 福建社会科学院0.240 8 探索中共重庆市委党校0.345 9 敦煌研究敦煌研究院0.167 10 统计研究中国统计学会;国家统计局统计科学研究所0.939 11 中国社会保障劳动和社会保障部社会保险局0.140 12 管理世界中华人民共和国国务院发展研究中心2.899 13 俄罗斯中亚东欧研究罗斯东欧中亚研究所0.388 14 毛泽东思想研究四川省社会科学院;四川省社会科学界联合会;中共四川省委党史研究室0.123 15 现代法学西南政法大学0.958 16 人民检察最高人民检察院0.475 17 人民司法最高人民法院0.389 18 当代财经江西财经大学0.674 19 当代经济科学西安交通大学0.710 20 生态经济云南教育出版社0.416 21 涉外税务中国国际税收研究会;深圳市国际税收研究会0.607 22 新闻战线人民日报社0.201 23 电视研究中国中央电视台0.189 24 中国出版中国出版杂志社0.246 25 出版发行研究中国出版科学研究所0.167 26 课程.教材.教法人民教育出版社;课程教材研究所1.217 27 外语教学与研究北京外国语大学3.510 28 文学评论中国社会科学院文学研究所0.858 29 清明安微省文联0.000 30 时代文学山东省作家协会0.000 31 作家吉林省作家协会0.043 32 花城花城出版社0.000 33 史学月刊河南大学;河南省历史学会0.282 34 华中科技大学学报(自然科学版) 华中科技大学0.362 35 上海交通大学学报上海交通大学0.411 36 中山大学学报(自然科学版) 中山大学0.596 37 哈尔滨工业大学学报哈尔滨工业大学0.437 38 北京师范大学学报(自然科学版) 北京师范大学0.303 39 天津大学学报天津大学0.319 40 东北大学学报(自然科学版) 东北大学0.637 41 同济大学学报(自然科学版) 同济大学0.422 42 北京理工大学学报北京理工大学0.422RLC电路的动态和频率特性综合研究
半导体激光器系统的动态特性研究资料
IGBT的动态特性与静态特性的研究
生物信息学期刊及影响因子汇总
RC一阶电路(动态特性 频率响应)研究
关于某论文设计是否被SCI、Ei、ISTP等检索以及期刊影响因子地解说
简述系统动态特性及其测定方法
电力系统功率频率动态特性研究--期刊
第三章 系统频率特性
频率特性
如何查询期刊影响因子
频率特性与系统的动态性能
影响因子查询表
相关主题
文本预览