• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    帶定性判斷的計(jì)分投票制及其公理刻畫

    2021-09-29 06:54:38趙偉
    邏輯學(xué)研究 2021年3期
    關(guān)鍵詞:趙偉公理計(jì)分

    趙偉

    1 Introduction

    Self-organization is a process where a stable pattern is formed by the cooperative behavior between parts of an initially disordered system without external control or influence.It has been introduced to multi-agent systems as an internal control process or mechanism to solve difficult problems spontaneously,especially if the system is operated in an open environment thereby having no perfect and a priori design to be guaranteed.([8,9,10])When the system is deployed in an open environment,agents can enter or exit the system.It might for example be that certain properties become true and certain properties become false,possibly bringing the system to an undesired state.Because in a self-organizing multi-agent system local rules work as guidance for agents to behave thus leading to specific outcomes,we can see the set of local rules as a mechanism that we implement in the system.A mechanism is a procedure,protocol or game for generating desired outcomes.If we want to know whether we can design a set of local rules to ensure desired outcomes,we then enter the field of mechanism design.([7])In the area of model checking,some work has been done to verify a multi-agent system,where norms are regarded as a mechanism.M.Knobbout et al.assume agents to have some preferences,which might be unknown to the system designers,and use a solution concept of Nash equilibrium for decision-making.([4])A formal framework is developed to verify whether a normative system implements desired outcomes no matter what preferences agents have.N.Bulling and M.Dastani formally analyze and verify whether a specific behavior can be enforced by norms and sanctions if agents follow their subjective preferences and whether a set of norms and sanctions that realize the effect exists at all.([2])In the present paper,agents are supposed to communicate with each other for their internals,which might be unknown to the system designers when the system is operated in an open environment,and thus it is important to know how the system behaves under the change of agents’ internals.Intuitively,we can verify both the original system and the new system afresh.However,as we have proved in [6],the verification is computationally expensive.Therefore,we need to think about how we can properly use the verification result that we get from the original system to better verify the new system.In this paper,we propose a framework to reason about the dynamics of self-organizing multi-agent systems under the change of participating agents.Agents follow their local rules to communicate with each other and perform actions,which results in the structural and semantic independence between agents that are represented by the notion of full contributions to the global system behavior.We prove that the full contribution of a coalition of agents remains the same if the internal function of any agent in the coalition is unchanged.Furthermore,we prove that the properties of a coalition regarding not being semantically independent or structurally independent inherit from the original system to the new system if the internal function of any agent in the coalition is unchanged,which means that we do not need to check their semantic independence and structural independence when verifying the new system.Such results can be used to improve the verification efficiency for the new system.

    The remaining part of this paper is structured as follows:In Section 2,we introduce the framework we use in this paper,setting up the context of self-organizing multi-agent systems;In Section 3,we propose the way how we change participating agents and prove what verification information we can use from the original system to efficiently verify the new system;In Section 4,we provide an example to illustrate our results;In Section 5,we conclude this paper and provide future work.

    2 Framework

    We use the same framework to formalize self-organizing multi-agent systems as what we introduced in[6].The semantic structure of this paper is concurrent game structures (CGSs).It is basically a model where agents can simultaneously choose actions that collectively bring the system from the current state to a successor state.Compared to other kripke models of transaction systems,each transition in a CGS is labeled with collective actions and the agents who perform those actions.Moreover,we treat actions as first-class entities instead of using choices that are identified by their possible outcomes.Formally,

    Definition 1A concurrent game structure is a tupleS(k,Q,π,Π,ACT,d,δ)such that:

    ? A natural numberk ≥1 of agents,and the set of all agents is Σ{1,...,k};we useAto denote a coalition of agentsA ?Σ;

    ? A finite setQof states;

    ? A finite set Π of propositions;

    ? A labeling functionπwhich maps each stateq ∈Qto a subset of propositions which are true atq;thus,for eachq ∈Qwe haveπ(q)?Π;

    ? A finite setACTof actions;

    ? For each agenti ∈Σ and a stateq ∈Q,di(q)?ACTis the non-empty set of actions available to agentiinq;D(q)d1(q)×...×dk(q)is the set of joint actions inq;given a stateq ∈Q,an action vector is a tuple〈α1,...,αk〉such thatαi ∈di(q);

    ? A functionδwhich maps each stateq ∈Qand a joint action〈α1,...,αk〉 ∈D(q) to another state that results from stateqif each agent adopted the action in the action vector,thus for eachq ∈Qand each〈α1,...,αk〉 ∈D(q)we haveδ(q,〈α1,...,αk〉)∈Q,and we use(q,〈α1,...,αk〉,q′)whereq′δ(q,〈α1,...,αk〉)to denote a transition that starts fromqand is labeled with〈α1,...,αk〉.

    Note that the model is deterministic:the same update function adopted in the same state will always result in the same resulting state.A computation overSis an infinite sequenceλq0,q1,q2,...of states such that for all positionsi ≥0,there is a joint action〈α1,...,αk〉 ∈D(qi) such thatδ(qi,〈α1,...,αk〉)qi+1.For a computationλand a positioni ≥0,we useλ[i]to denote theith state ofλ.More elaboration of concurrent game structures can be found in[1].

    The same as what we did in [6],we can define a self-organizing multi-agent system as a concurrent game structure together with a set of local rules for agents to follow.Before defining such a type of local rules,we first define what to communicate,which is given by an internal function.

    Definition 2(Internal Functions) Given a concurrent game structureSand an agenti,the internal function of agentiis a functionmi:Q →Lpropthat maps a stateq ∈Qto a propositional formula.We use a tupleM〈m1,m2,...,mk〉to denote the profile of internal functions for all the participating agents.We also useUito denote the set of possible internal functions for agentiin Σ andUMU1×U2×...Ukto denote the universe of tuples of internal functions.

    The internal function returns the information that is provided by participating agents themselves at a particular state,which is referred to as anagent typein this paper and thus might be different from agent to agent.A local rule is defined based on agents’communication as follows:

    Definition 3(Abstract Local Rules) Given a concurrent game structureS,an abstract local rule for agentais a tuple〈τa,γa〉consisting of a functionτa(q)that maps a stateq ∈Qto a subset of agents,that is,τa(q)?Σ,and a functionγa(M(q))that mapsM(q){mi(q)|i ∈τa(q)}to an action available in stateqto agenta,that is,γa(M(q))∈da(q).We denote the set of all the abstract local rules as Γ and a subset of abstract local rules as ΓAthat are designed for the coalition of agentsA.

    An abstract local rule consists of two parts:the first partτa(q)states the agents with whom agentais supposed to communicate in stateq,and the second partγastates the action that agentais supposed to take given the communication with agents inτa(q)for their internals.We see local rules not only as constraints but also guidance on agents’behavior,namely an agent does not know what to do if he does not communicate with other agents.Therefore,we exclude the case where agents get no constraint from their respective local rules.We useoutto denote a set of computations and notationout(q,M,ΓA)is the set of computations starting from stateqwhere agents in coalitionAfollow their respective local rules in ΓAwith internal functionsM.A computationλq0,q1,q2,...is inout(q0,M,ΓA) if and only if it holds that for all positionsi ≥0 there is a move vector〈α1,...,αk〉 ∈D(λ[i])such thatδ(λ[i],〈α1,...,αk〉)λ[i+1]and for alla ∈Ait is the case thatαaγa(M(λ[i])).Moreover,when we refer to a stateqin a computationλ,which is inout(q0,M,ΓA),we will simply writeq ∈out(q0,M,ΓA)for short in the rest of this paper.Now we are ready to define a self-organizing multi-agent system.Formally,

    Definition 4(Self-organizing Multi-agent Systems) A self-organizing multi-agent system(SOMAS)is a tuple(S,M,Γ),whereSis a concurrent game structure,Mis the set of internal functions and Γ is a set of local rules that agents follow.

    Example 5We will use the example in[3,11]for better understanding the above definitions.Consider a CGS scenario as Figure.1 where there are two trains,each controlled by an agent,going through a tunnel from the opposite side.The tunnel has only room for one train,and the agents can either wait or go.Starting from stateq0,if the agents choose to go simultaneously,the trains will crash,which is stateq4;if one agent goes and the other waits,they can both successfully pass through the tunnel,which isq3.

    Fig.1:A CGS example.

    Local rules〈τ1,γ1〉and〈τ2,γ2〉are prescribed for the agents to follow:both agents communicate with each other for their urgenciesu1andu2in stateq0;the one who is more urgent can go through the tunnel first;otherwise,it has to wait.Given the above local rules,ifa1is more urgent than or as urgent asa2with respect tou1andu2,the desired stateq3is reached along with computationq0,q2,q3...;ifa1is less urgent thana2with respect tou1andu2,the desired stateq3is reached along with computationq0,q1,q3....

    In order to study how a self-organizing multi-agent system behaves under the change of participating agents,we first need to characterize the independence between agents in terms of their contributions to the system behavior.In this paper,it is characterized from two perspectives:a semantic perspective given by the underlying game structure and a structural perspective derived from abstract local rules.Similar to ATL in [1],our language ATL-Γ is interpreted over a concurrent game structureSthat has the same propositions and agents as our language.It is an extension of classical propositional logic with temporal cooperation modalities.A formula of the form〈A〉ψmeans that coalition of agentsAwill bring about the subformulaψby following their respective local rules in ΓA,no matter what agents in ΣAdo,whereψis a temporal formula of the form○φ,□φorφ1Uφ2(whereφ,φ1,φ2are again formulas in our language).Formally,the grammar of our language is defined below,wherep ∈Π andA ?Σ:

    Given a self-organizing multi-agent system(S,M,Γ),whereSis a concurrent game structure and Γ is a set of local rules,and a stateq ∈Q,we define the semantics with respect to the satisfaction relation|inductively as follows:

    ?S,M,Γ,q |piffp ∈π(q);

    ?S,M,Γ,q |?φiffS,M,Γ,q|φ;

    ?S,M,Γ,q |φ1∧φ2iffS,M,Γ,q |φ1andS,M,Γ,q |φ2;

    ?S,M,Γ,q |〈A〉○φiff for allλ ∈out(q,M,ΓA),we haveS,M,Γ,λ[1]|φ;

    ?S,M,Γ,q |〈A〉□φiff for allλ ∈out(q,M,ΓA)and all positionsi ≥0 it holds thatS,M,Γ,λ[i]|φ;

    ?S,M,Γ,q |〈A〉φ1Uφ2iff for allλ ∈out(q,M,ΓA)there exists a positioni ≥0 such that for all positions 0≤j ≤iit holds thatS,M,Γ,λ[j]|φ1andS,M,Γ,λ[i]|φ2.

    Dually,we write〈A〉◇φfor〈A〉?Uφ.We can check a formula in our language to verify whether a coalition of agents will bring about a temporal property through following its local rules,which is regarded as semantic independence in this paper.Moreover,agents in the system follow their respective local rules to communicate with other agents.Based on their communcation,we can see a coalition of agents do not get input information from agents outside the coalition,which is regarded as structural independence in this paper.This gives rise to the notion of independent components.

    Definition 6(Independent Components) Given an SOMAS(S,M,Γ),a coalition of agentsA ?Σ and a stateq,we say that coalitionAis an independent component w.r.t.qif and only if for alla ∈Aand its abstract local rule〈τa,γa〉it is the case thatτa(q)?A;a coalition of agentsAis an independent component w.r.t.a set of computationsoutiff for allλ ∈outandq ∈λ,Ais an independent component with respect to stateq.

    In other words,an independent component might output information to agents in ΣA,but do not get input from agents in ΣA.As we can see,it is a structural property given by the communication between agents in a given state.We then propose the notions ofsemantic independence,structural independence and full contributionto characterize the independence between agents from different perspectives.

    Definition 7(Semantic Independence,Structural Independence and Full Contribution) Given an SOMAS(S,M,Γ),a coalition of agentsAand a stateq,

    ?Ais semantically independent with respect to a temporal formulaψfromqiffS,M,Γ,q |〈A〉ψ;

    ?Ais structurally independent fromqiffAis an independent component w.r.t.the set of computationsout(q,M,ΓA);

    ?Ahas full contribution toψinqiffAis the minimal(w.r.t.set-inclusion)coalition that is both semantically independent with respect toψand structurally independent fromq.

    In other words,coalitionAhas full contribution toψbecause any subset of coalitionAis either semantically dependent with respect toψo(hù)r structurally dependent.Given a self-organizing multi-agent system and a set of temporal formulas,we check with each subset of agents and each temporal formula for their semantic and structural independence in order to find which coalition has full contribution to which property.One can refer to[6]for detailed discussion about the above definitions and examples in this section.

    Example 8We continue to discuss the two-train example.Neither train,namelya1ora2as a coalition,has full contribution to the result of passing through the tunnel without crash.The reasons are listed as follows:any single train cannot ensure the result of passing through the tunnel without crash,which means that any single train is not semantically independent and can be expressed:

    Moreover,both trains follow their local rules to communicate with each other in stateq0,which means that any single train is not an independent component w.r.t.stateq0thus not being structurally independent.

    Two trains have full contribution to the result of passing through the tunnel without crash,because both agents by themselves can bring about the result of passing through the tunnel without crash through following the local rules,which can be expressed:

    Moreover,the coalition of two trains is obviously an independent component w.r.t.out(q0,M,Γ{a1,a2}),which means that it is structurally independent,and the coalition of two trains is obviously the minimal coalition that is both semantically independent w.r.t.the result of passing the tunnel without crash and structurally independent from stateq0.

    3 Changing Participating Agents

    When a self-organizing multi-agent system is deployed in an open environment,different types of agents participate in the system and their internals might be unknown to system designers.Therefore,it is important to verify whether the set of local rules still generates desired outcomes,more generally how the system behaves,under the change of participating agents.Because in this paper an internal functionmirefers to an agent type and might be interpreted as agents’preferences,interests or other internal information over states that can be different from agent to agent,changing participating agents can be done by simply replacing internal functions so that the original internal function and the new internal function return different values in the same state.Here we assume that the number of agents in the system does not change so the indexes of agents in Σ remain the same.We have the following definition:

    Definition 9(Change of Participating Agents) Given an original SOMAS(S,M,Γ),a new SOMAS under the change of participating agents is denoted as(S,M′,Γ),whereM′ ∈UMand there exists an agenta ∈Σ and a stateq ∈Qsuch thatma(q)

    As we can see,what we meant by replacing internal functions is that in the new system there exists at least an agent’s internal function such that given the same state its output is different from the one in the original system.Except the internal functions,the underlying concurrent game structure and the set of local rules remain the same.

    Changing participating agents in the system might cause undesired outcomes.Agents communicate with each other for their internals and make a move based on the communication results.The change of agents’ internal functions might change the actions that agents are allowed to take by their local rules,and consequently the new system runs along a computation that might be different from the original system,making undesired properties hold.Therefore,local rules have to be well designed in order to ensure that desired properties remain unchanged under the change of participating agents.

    Example 10In the two-train example,suppose both trains have the same urgency,denoted asM′,they will choose to wait because neither train is more urgent than the other one,resulting in the undesired stateq0of deadlock.As we can see,the local rules cannot ensure that the system reaches a desired state no matter what kind of agents participate in the system.

    Given a self-organizing multi-agent system(S,M,Γ)and a temporal formula as an indicated property,in order to find out which coalition of agents has full contribution to a temporal formula,we need to do model-checking with each subset of Σ and that formula.Intuitively we can follow the same process to verify the new system (S,M′,Γ) as what we did with the original system.However,as we have proved in[6],checking whether a coalition of agents has full contribution to a temporal formula is computationally expensive,because we have to enumerate all the subsets of the coalition and check for their semantic and structural independence in order to ensure the minimality,making verifying both the original system and the new system afresh inefficient and difficult.Thus,it is important to think about whether we can use the verification result with the original system to better verify the new system.In the area of formal argumentation,Beishui Liao,et al propose a divisionbased method to compute the status of arguments when the argumentation system is updated.([5]) Inspired by that,we can divide the system into two parts:the set of agents whose internal functions remain the same and the set of agents whose internal functions change.For the first part,as was in Definition 9,when a self-organizing multi-agent system switches to another under the change of participating agents,it is not necessary that the internal functions of all agents change,which means that there might exist some agents whose internal functions remain the same.Such agents are called an unchanged set.Formally:

    Definition 11(Unchanged Sets) Given two SOMASs (S,M,Γ) and (S,M′,Γ)under the change of agents’internal functions fromMtoM′,an unchanged set with respect toMandM′is defined asUS(M,M′){a ∈Σ|for allq ∈Q:ma(q)

    An unchanged set is symmetric in terms of the change of agents’internal functions.

    Proposition 12Given two SOMASs (S,M,Γ) and (S,M′,Γ),US(M,M′)US(M′,M).

    ProofWe can easily prove it following Definition 11. □

    A coalition of agents has full contribution to a temporal formula if and only if it is the minimal coalition that is both structurally and semantically independent.We can intuitively imagine that a coalition behaves the same if the internal function of each agent inside the coalition does not change,which means that we can reuse the verification information for the original system when verifying the new system.Thus,one important property of unchanged sets is that the full contributions of agents inside an unchanged set remain the same when the internal functions switch fromMtoM′.

    Proposition 13Given two SOMASs(S,M,Γ)and(S,M′,Γ)under the change of agents’internal functions fromMtoM′,and a stateq,if for anya ∈A,q′ ∈Q,i ∈τa(q′)it is the case thatmi(q′),thenout(q,M,ΓA)out(q,M′,ΓA).

    ProofLetout(q,M,ΓA)[i] be a set of states,each of which is theith state of any computation inout(q,M,ΓA).That is,out(q,M,ΓA)[i]{q′ ∈Q | ?λ ∈out(q,M,ΓA) :q′λ[i]}.Next,we need to inductively prove thatout(q,M′,ΓA)in the new system contains the same computations asout(q,M,ΓA) in the original system.Firstly,computations from bothout(q,M,ΓA)andout(q,M′,ΓA)start from stateq.Secondly,supposeout(q,M,ΓA)[i]out(q,M′,ΓA)[i].If for anya ∈A,q′ ∈Q,i ∈τa(q′)we havemi(q′)m′i(q′),thenM(q′)M′(q′),consequentlyγa(M(q′))γa(M′(q′)),which means thatγa(·)returns the same action for each agent in stateq′in both systems.Hence,out(q,M,ΓA)[i+1]out(q,M′,ΓA)[i+1].So we can conclude thatout(q,M,ΓA)out(q,M′,ΓA). □

    From that,we can see the properties of computation setout(q,M,ΓA)remain the same under the change of agents’internal functions fromMtoM′if the internal functions of agents with which coalitionAneeds to communicate remain the same.This gives rise to one important property of unchanged sets:the full contributions of agents inside an unchanged set remain the same when the internal functions switch fromMtoM′.

    Theorem 14.Given two SOMASs(S,M,Γ)and(S,M′,Γ)under the change of agents’ internal functions from M to M′,for any coalition A ?US(M,M′),A has full contribution to a temporal formula ψ in a state q in(S,M,Γ)iff A has full contribution to ψ in q in(S,M′,Γ).

    ProofWe first prove the forward part.Because coalitionAhas full contribution toψin stateqin SOMAS (S,M,Γ),we haveS,M,Γ,q |〈A〉ψ(semantic independence),andAis an independent component w.r.t.out(q,M,ΓA) (structural independence),and any subset ofAis either semantically dependent with respect toψo(hù)r structurally dependent from stateqin(S,M,Γ).BecauseA ?US(M,M′),the internal function of any agent inAremains the same fromMtoM′.By Proposition 13,out(q,M,ΓA)out(q,M′,ΓA).That implies the properties that hold forout(q,M,ΓA) also hold forout(q,M′,ΓA).Thus,by Definition 7,we haveS,M′,Γ,q |〈A〉ψ(semantic independence),andAis an independent component w.r.t.out(q,M′,ΓA) (structural independence).Next,we need to prove whetherAis also the minimal coalition that is both semantically independent with respect toψand structurally independent fromqin(S,M′,Γ).Suppose there exists a coalitionA′ ?Athat is both semantically independent with respect toψand structurally independent fromqin(S,M′,Γ),which means thatS,M′,Γ,q |〈A′〉ψandA′is an independent component w.r.t.out(q,M′,ΓA′).BecauseA′ ?A ?US(M,M′)US(M′,M),the internal function of any agent inA′remains the same fromM′toM.By Proposition 13,out(q,M,ΓA′)out(q,M′,ΓA′),which implies thatS,M,Γ,q |〈A′〉ψandA′is an independent component w.r.t.out(q,M,ΓA′)and thus contradicts with the premise thatAis the minimal coalition that is both semantically independent and structurally independent.Hence,coalitionAis also the minimal coalition that is semantically independent w.r.t.ψand structurally independent from stateqin the new system.Therefore,coalitionAalso has full contribution toψin stateqin(S,M′,Γ).BecauseA ?US(M,M′)US(M′,M),we can prove the backward part in a similar way. □

    Therefore,given that the internal functions of coalitionAremain the same,if we already know that coalitionAhas full contribution toψin stateqin the original system,it will remain the same in the new system;if we already know that coalitionAdoes not have full contribution toψin stateqin the original system,it will also remain the same in the new system.That means the verification information regarding agents in the unchanged set will remain the same under the change of agents’internal functions,which can be used to simplify the verification of the new system.To find the unchanged set with respect toMandM′,we can simply check the internal functions of all the agents with all the states,which can be done in polynomial time to the number of states and the number of agents.After we obtain the unchanged set,we can copy the information about agents’ full contributions within the unchanged set from the original system to the new system.Moreover,since the full contributions of agents in the unchanged set remain the same,the coalitions that we have to check with for the new system becomeP(Σ)P(US(M,M′))instead ofP(Σ)for the original system.The propositions below will give insights to further simplify the verification of the new system.

    Proposition 15Given an SOMAS(S,M,Γ),a coalition of agentsA,a temporal formulaψand a stateq,if for anyA′ ?Ait is the case thatA′does not have full contribution toψin stateq,thenA′is either semantically dependent w.r.t.ψo(hù)r structurally dependent fromq.

    ProofSuppose there existsA′ ?Asuch that it is both semantically independent w.r.t.ψand structurally independent fromq.IfA′is the minimal one,A′has full contribution toψin stateq;ifA′is not the minimal one,there existsA′′ ?A′such that it is the minimal coalition that is both semantically independent w.r.t.ψand structurally independent fromq.Both cases contradict with the premise that for anyA′ ?Ait is the case thatA′does not have full contribution toψin stateq.Thus,A′is either semantically dependent w.r.t.ψo(hù)r structurally dependent fromq. □

    Theorem 16.Given two SOMASs(S,M,Γ)and(S,M′,Γ)under the change of agents’internal functions from M to M′,a coalition of agents A?US(M,M′),a temporal formula ψ and a state q,A has full contribution to ψ in state q in(S,M′,Γ)iff both of the following statements are satisfied:

    1.for any A′ ?US(M,M′)∩A it is the case that A′ does not have full contribution to ψ in state q in(S,M,Γ);

    2.A is the minimal(w.r.t.set-inclusion)coalition within P(A)P(US(M,M′))that is both semantically independent with respect to ψ and structurally independent from q in(S,M′,Γ).

    ProofSince for anyA′ ?US(M,M′)∩Ait is the case thatA′does not have full contribution toψin stateqin(S,M,Γ),we then have for anyA′ ?US(M,M′)∩Ait is the case thatA′does not have full contribution toψin stateqin(S,M′,Γ).That also impliesA′is either semantically dependent w.r.t.ψo(hù)r structurally dependent from stateqin(S,M′,Γ).Combining with the second statement,we can conclude thatAhas full contribution toψin stateqin(S,M′,Γ). □

    In order to verify whether a coalition of agentsAhas full contribution toψ,normally we have to check the semantic independence and structural independence of any subset ofAin order to ensure the minimality,which is computationally expensive as the size of the coalition increases.While Theorem 14 shows us the case whereA ?US(M,M′),Theorem 16 shows us how we can further utilize the information about agents’full contribution from the original system in the new system whenA?US(M,M′).If we have proved that any subset of the unchanged set does not have full contribution toψin the original system,we do not need to check their semantic independence and structural independence when verifying the new system,because they will not hold as in the original system.With the verification information from the original system,we can decrease the coalitions that we have to check fromP(A)toP(A)P(US(M,M′)∩A).We can use Theorem 16 and Theorem 14 to more efficiently verify whether a coalition of agents has full contribution to a temporal formula in the new system.In the next section,we will use an example to illustrate how we can use the verification result from the original system in the verification of the new system based on Theorems 14 and 16.

    4 Example

    We extend the two-train example to illustrate the above theory.Suppose we have a U-shape traffic system depicted as in Fig.2.The top is the same as the previous example where trainsa1anda2,each controlled by an agent,are going through a tunnel from the opposite side.Agenta2exits the traffic system from Exit1 after passing through the tunnel,while agenta1needs to go down to exit the traffic system from Exit3 after passing through the tunnel.Below the tunnel there is a second tunnel,and on the left hand side another train,controlled by agenta3,is also going through the tunnel to exit the system from Exit3.The whole traffic system has only room for one train to go through,and the agents can either wait or go.Since agenta1needs to go down to exit the traffic system after passing through the first tunnel,it will clash with agenta3by Exit3 if they go simultaneously.The CGS is depicted in Fig.3.

    Fig.2:A traffic system consisting of three trains.

    Fig.3:CGS of the three-train example,where formula ci means that train i clashes in the tunnel and formula ei means that train i exits the traffic system.

    The local rules for three agents are quite simple:whenever there is space limitation for two trains to go through,the one which is more urgent can go first and the other one which less urgent needs to wait.The set of temporal formulas is{◇e1,◇e2,◇e3},each of which means that agentiexits the system.Given an SOMAS(S,M,Γ),suppose agenta2is more urgent than agenta1,so agenta1waits until agenta2passes through the first tunnel.Because agenta3goes while agenta1is waiting,agenta3can exit the system without meeting agenta1by the Exit3.Thus,we have the following verification information in Table 1.From Table 1 we can see that coalition{a1,a2}has full contribution to the result of◇e1and◇e2in stateq0in(S,M,Γ)as what we had previously,and{a1,a2,a3}has full contribution to◇e3in stateq0in(S,M,Γ).In particular,agenta3cannot bring about the result of exiting the system by itself,because ifa1goes anda2waits,which means that they do not follow their local rules to behave,a1anda3will meet Exit3 and need to cooperate in order to exit the system.

    Table.1:Verification information for SOMASs (S,M,Γ),where“SI”stands for structural independent.

    Table.2:Verification information for SOMAS (S,M′,Γ),where“SI”stands for structural independent.

    Now consider a new SOMAS(S,M′,Γ)under the change of internal functions fromMandM′,where the internal functions of agentsa1anda2change while the internal function of agenta3remains the same.In this case,agenta1chooses to go and agenta2chooses to wait.We can see thata1anda3will meet by Exit3 and thus they need to communicate with each other for their urgencies.Moreover,since only the internal function ofa3remains the same,and coalitions{a3}and?do not have full contribution to◇e1,◇e2or◇e3in the original system(S,M,Γ),by Theorem 16,we can reuse the verification information about{a3}from the original system by copying the columns of?and{a3}from Table 1 to Table 2.It shows that{a3}and?are either semantically dependent or structurally dependent.Copying this information can simplify the process of ensuring the minimality when doing modelchecking.For example,for checking whether coalition{a1,a2,a3}has full contribution to◇e3in stateq0in (S,M′,Γ),normally we need to check both semantic and structural independence for each subset of{a1,a2,a3},which isP({a1,a2,a3});since we know from the original system that?and{a3}are either semantically dependent w.r.t.◇e3or structurally dependent,the coalitions we need to check becomeP({a1,a2,a3}){?,{a3}}.We then have the following verification information in Table 2.As we can see,coalition{a1,a2,a3}is the minimal coalition that is both semantically independent(w.r.t.◇e1,◇e2or◇e3)and structurally independent,so coalition{a1,a2,a3}has full contribution to◇e1,◇e2and◇e3in stateq0in(S,M′,Γ).

    5 Conclusion

    When a self-organizing multi-agent system is deployed in an open environment,the change of participating agents might bring the system to an undesired state.As it is computationally expensive to verify a self-organizing multi-agent system,we need to think about how we can properly use the verification result that we get from the original system to better verify the new system.In this paper,we propose a framework to reason about the dynamics of self-organizing multi-agent systems under the change of participating agents.Agents in the system are divided into two parts:one whose internal functions remain the same and the other one whose internal functions change.We first proved that the full contribution of a coalition of agents remains the same if the internal function of any agent in the coalition remains the same.Furthermore,the properties of a coalition regarding not being semantically independent or structurally independent remain the same if the internal function of any agent in the coalition remains the same,which means that we do not need to check their semantic independence and structural independence when verifying the new system.Future work can be done in the direction of reasoning about the dynamics of self-organizing multi-agent systems in terms of revising agents’local rules.

    猜你喜歡
    趙偉公理計(jì)分
    到底誰會(huì)贏?
    3秒給答案
    假如你有很多錢,該怎么花?
    如何求函數(shù)y=Asin(ωx+φ)中φ的值
    引導(dǎo)素質(zhì)教育的新高考計(jì)分模式構(gòu)想:線性轉(zhuǎn)化計(jì)分模式
    基于單片機(jī)的中國式摔跤比賽計(jì)分器開發(fā)設(shè)計(jì)
    電子制作(2019年9期)2019-05-30 09:42:06
    歐幾里得的公理方法
    Abstracts and Key Words
    公理是什么
    計(jì)分考核表在績效管理中的應(yīng)用效果
    能在线免费观看的黄片| 99久久精品热视频| 老司机影院成人| 亚洲激情五月婷婷啪啪| 熟女人妻精品中文字幕| 只有这里有精品99| 韩国高清视频一区二区三区| 国产黄色免费在线视频| 成人二区视频| 国国产精品蜜臀av免费| 亚洲成人av在线免费| 欧美97在线视频| 六月丁香七月| 日本-黄色视频高清免费观看| 国产黄片视频在线免费观看| 国内精品美女久久久久久| 欧美高清性xxxxhd video| 亚洲高清免费不卡视频| 九九久久精品国产亚洲av麻豆| 亚洲性久久影院| 国产黄色视频一区二区在线观看| 草草在线视频免费看| 国产激情偷乱视频一区二区| 啦啦啦啦在线视频资源| 精品久久久久久久末码| 两个人的视频大全免费| 男女那种视频在线观看| 在线观看免费高清a一片| 少妇人妻一区二区三区视频| 国产欧美日韩精品一区二区| 国产在视频线精品| 亚洲精品乱码久久久久久按摩| 99热这里只有精品一区| 亚洲国产精品专区欧美| 亚洲精品成人av观看孕妇| 嫩草影院新地址| 2021天堂中文幕一二区在线观| 免费看日本二区| 国产av国产精品国产| 男女下面进入的视频免费午夜| 中文字幕av成人在线电影| 搞女人的毛片| 国产综合精华液| 美女黄网站色视频| 久久精品人妻少妇| 久久久久免费精品人妻一区二区| 一夜夜www| 国产精品一区二区性色av| 一级av片app| 爱豆传媒免费全集在线观看| 精品国内亚洲2022精品成人| 久久久色成人| 夫妻午夜视频| 男女边摸边吃奶| 久久久久免费精品人妻一区二区| 欧美 日韩 精品 国产| 好男人视频免费观看在线| 国产成人精品婷婷| 尾随美女入室| 建设人人有责人人尽责人人享有的 | 九色成人免费人妻av| 看黄色毛片网站| 男人狂女人下面高潮的视频| 丰满人妻一区二区三区视频av| 色网站视频免费| 亚洲精品一区蜜桃| 国产片特级美女逼逼视频| 国产精品人妻久久久影院| 色网站视频免费| 观看免费一级毛片| 简卡轻食公司| 最近最新中文字幕免费大全7| 欧美三级亚洲精品| 又黄又爽又刺激的免费视频.| 麻豆成人午夜福利视频| 国产综合精华液| 国产精品久久久久久精品电影| av天堂中文字幕网| 久久久a久久爽久久v久久| 一本久久精品| 日韩制服骚丝袜av| 亚洲电影在线观看av| 成人美女网站在线观看视频| 国产视频内射| 欧美另类一区| 男人舔女人下体高潮全视频| 亚洲激情五月婷婷啪啪| 亚洲av中文字字幕乱码综合| 麻豆乱淫一区二区| 国产精品久久视频播放| 淫秽高清视频在线观看| 国产免费一级a男人的天堂| 亚洲丝袜综合中文字幕| 成人亚洲精品av一区二区| 日日摸夜夜添夜夜爱| 亚洲综合色惰| av网站免费在线观看视频 | 18禁动态无遮挡网站| 久久韩国三级中文字幕| 国产精品一区二区三区四区久久| 搞女人的毛片| 麻豆精品久久久久久蜜桃| 日韩强制内射视频| 日韩制服骚丝袜av| 免费观看在线日韩| 国产成人午夜福利电影在线观看| 麻豆av噜噜一区二区三区| 最近中文字幕高清免费大全6| 国产av在哪里看| 蜜桃久久精品国产亚洲av| 亚洲国产色片| 亚洲国产精品成人久久小说| 美女内射精品一级片tv| 一级a做视频免费观看| 亚洲乱码一区二区免费版| 国产午夜福利久久久久久| 免费黄频网站在线观看国产| 国产精品一二三区在线看| 六月丁香七月| 国产精品爽爽va在线观看网站| 日日撸夜夜添| 精华霜和精华液先用哪个| 国产精品一区二区在线观看99 | 中文字幕亚洲精品专区| 一级毛片久久久久久久久女| 国产免费福利视频在线观看| 日韩视频在线欧美| 狂野欧美白嫩少妇大欣赏| 欧美一区二区亚洲| 搡女人真爽免费视频火全软件| 身体一侧抽搐| 黄色欧美视频在线观看| 久99久视频精品免费| 成人特级av手机在线观看| 国产黄色免费在线视频| 看十八女毛片水多多多| 欧美潮喷喷水| 又爽又黄无遮挡网站| 亚洲欧美日韩卡通动漫| 欧美日韩精品成人综合77777| 亚洲色图av天堂| av免费观看日本| 久久久久九九精品影院| 久久久欧美国产精品| 欧美+日韩+精品| 午夜激情福利司机影院| 日本欧美国产在线视频| 国产成人精品婷婷| 波野结衣二区三区在线| 久久久a久久爽久久v久久| 99热全是精品| 在线观看免费高清a一片| 久久久久久国产a免费观看| 少妇人妻一区二区三区视频| 国产在视频线在精品| 免费黄色在线免费观看| 一级毛片我不卡| 男女边吃奶边做爰视频| 深夜a级毛片| 亚洲经典国产精华液单| 麻豆成人av视频| 伊人久久国产一区二区| 日韩亚洲欧美综合| 日韩强制内射视频| 日本色播在线视频| 尾随美女入室| 欧美xxxx黑人xx丫x性爽| 色综合亚洲欧美另类图片| 波野结衣二区三区在线| 日韩国内少妇激情av| 极品教师在线视频| av国产久精品久网站免费入址| 搡老乐熟女国产| 黄片wwwwww| 亚洲第一区二区三区不卡| 亚洲av成人精品一区久久| 久久久久久久久久久丰满| 大片免费播放器 马上看| 嫩草影院新地址| 色综合站精品国产| 国产精品av视频在线免费观看| 国产av在哪里看| 成人毛片a级毛片在线播放| 国产精品1区2区在线观看.| 精品久久久久久久人妻蜜臀av| 91精品国产九色| 丝袜美腿在线中文| 偷拍熟女少妇极品色| 一级毛片 在线播放| 永久免费av网站大全| 国产精品一区二区在线观看99 | 精品久久久久久成人av| 国产成人aa在线观看| 18禁裸乳无遮挡免费网站照片| av免费在线看不卡| 五月伊人婷婷丁香| 日日啪夜夜撸| 亚洲在久久综合| 人妻系列 视频| 美女内射精品一级片tv| 欧美日韩精品成人综合77777| 亚洲va在线va天堂va国产| 国产男人的电影天堂91| 亚洲色图av天堂| 男插女下体视频免费在线播放| 高清午夜精品一区二区三区| 女的被弄到高潮叫床怎么办| 欧美zozozo另类| 搡老妇女老女人老熟妇| 国产精品爽爽va在线观看网站| 丰满乱子伦码专区| 国产精品美女特级片免费视频播放器| 久久精品国产亚洲av天美| 国产老妇伦熟女老妇高清| 日日摸夜夜添夜夜爱| 中文字幕av成人在线电影| 十八禁网站网址无遮挡 | 亚洲自拍偷在线| 99视频精品全部免费 在线| 天堂av国产一区二区熟女人妻| 丝袜美腿在线中文| 成人午夜高清在线视频| 国产黄a三级三级三级人| 国产精品av视频在线免费观看| 欧美日韩在线观看h| 国产真实伦视频高清在线观看| 日韩一本色道免费dvd| 国产爱豆传媒在线观看| 国产高清不卡午夜福利| 色综合色国产| 免费观看在线日韩| 国产精品国产三级专区第一集| 蜜臀久久99精品久久宅男| 91aial.com中文字幕在线观看| 91aial.com中文字幕在线观看| 少妇丰满av| 亚洲美女视频黄频| 亚洲精品乱久久久久久| 九色成人免费人妻av| av在线天堂中文字幕| 免费观看无遮挡的男女| 亚洲av男天堂| 国产精品综合久久久久久久免费| 亚洲最大成人中文| av黄色大香蕉| 在线观看人妻少妇| 久久人人爽人人片av| 久久综合国产亚洲精品| 男女下面进入的视频免费午夜| 欧美日韩综合久久久久久| 青春草视频在线免费观看| 精品久久久久久久久久久久久| 亚洲精品日本国产第一区| 最近中文字幕高清免费大全6| 日韩av免费高清视频| 久久久久久久久久久免费av| 麻豆精品久久久久久蜜桃| 免费无遮挡裸体视频| 亚洲性久久影院| 国产免费视频播放在线视频 | 精品久久久久久电影网| 精品人妻视频免费看| 亚洲精品日韩在线中文字幕| av网站免费在线观看视频 | 日本免费在线观看一区| av在线蜜桃| 在线免费观看的www视频| 2018国产大陆天天弄谢| 偷拍熟女少妇极品色| 丝袜美腿在线中文| av女优亚洲男人天堂| 麻豆成人午夜福利视频| 亚洲av不卡在线观看| 亚洲成人一二三区av| 精品一区在线观看国产| 国产精品女同一区二区软件| 亚洲怡红院男人天堂| 亚洲精品,欧美精品| 亚洲成人中文字幕在线播放| 久久精品夜夜夜夜夜久久蜜豆| 久久精品久久久久久噜噜老黄| 午夜免费男女啪啪视频观看| 色尼玛亚洲综合影院| 99热这里只有是精品在线观看| 最近2019中文字幕mv第一页| 日韩一区二区三区影片| 国产黄色视频一区二区在线观看| 成人av在线播放网站| 亚洲四区av| 久久99热6这里只有精品| 一级黄片播放器| 日韩av在线大香蕉| 69人妻影院| 国产老妇伦熟女老妇高清| 熟女人妻精品中文字幕| 男人和女人高潮做爰伦理| 精品人妻熟女av久视频| 国产美女午夜福利| 免费看日本二区| 97精品久久久久久久久久精品| 久久精品夜色国产| 亚洲人成网站在线播| 大又大粗又爽又黄少妇毛片口| 日本熟妇午夜| 亚洲欧美精品自产自拍| 亚洲乱码一区二区免费版| 国产精品一及| 国产高清国产精品国产三级 | 97热精品久久久久久| 成人午夜高清在线视频| 国产黄色小视频在线观看| 啦啦啦中文免费视频观看日本| 卡戴珊不雅视频在线播放| 综合色丁香网| 亚洲国产精品成人综合色| 亚洲国产欧美人成| a级毛片免费高清观看在线播放| 2018国产大陆天天弄谢| xxx大片免费视频| 国产精品女同一区二区软件| 日韩制服骚丝袜av| 天堂√8在线中文| 国产亚洲最大av| 欧美性猛交╳xxx乱大交人| 嫩草影院精品99| 激情 狠狠 欧美| 欧美性感艳星| 久久精品久久精品一区二区三区| 国产视频内射| 亚洲av成人精品一区久久| 国产成人午夜福利电影在线观看| 黄色配什么色好看| 91久久精品电影网| 免费高清在线观看视频在线观看| 神马国产精品三级电影在线观看| 中文字幕av成人在线电影| 久久精品人妻少妇| 国产午夜精品久久久久久一区二区三区| 国产精品国产三级国产av玫瑰| 亚洲av.av天堂| 免费播放大片免费观看视频在线观看| 日韩不卡一区二区三区视频在线| 看十八女毛片水多多多| 91久久精品电影网| 亚洲精品日韩av片在线观看| 日韩欧美精品v在线| 最新中文字幕久久久久| 免费大片18禁| 日韩 亚洲 欧美在线| 亚洲久久久久久中文字幕| 成人综合一区亚洲| 国产成人freesex在线| 亚洲欧美一区二区三区黑人 | 欧美极品一区二区三区四区| 男女视频在线观看网站免费| 777米奇影视久久| 日韩伦理黄色片| 国产精品一区二区三区四区久久| 精品99又大又爽又粗少妇毛片| 蜜桃亚洲精品一区二区三区| 成人综合一区亚洲| 麻豆成人av视频| 伦理电影大哥的女人| 国产精品一区二区性色av| 国内少妇人妻偷人精品xxx网站| 亚洲精品,欧美精品| 国产精品久久久久久精品电影| 成人漫画全彩无遮挡| 美女cb高潮喷水在线观看| 男人爽女人下面视频在线观看| 超碰97精品在线观看| 亚洲av在线观看美女高潮| 欧美潮喷喷水| 国产伦精品一区二区三区四那| 欧美变态另类bdsm刘玥| 亚洲在久久综合| 国产免费福利视频在线观看| 精品酒店卫生间| 熟女电影av网| 亚洲成人av在线免费| 日韩伦理黄色片| 天美传媒精品一区二区| 亚洲最大成人手机在线| 熟妇人妻不卡中文字幕| 国产成人一区二区在线| 大香蕉久久网| 午夜福利网站1000一区二区三区| 人人妻人人澡欧美一区二区| 亚洲欧美成人综合另类久久久| 一夜夜www| 亚洲久久久久久中文字幕| 美女脱内裤让男人舔精品视频| 一级毛片久久久久久久久女| 国产成人a区在线观看| 神马国产精品三级电影在线观看| 91久久精品国产一区二区成人| 免费黄频网站在线观看国产| 精品人妻偷拍中文字幕| 国产一区亚洲一区在线观看| 午夜福利在线观看吧| 国产日韩欧美在线精品| 日韩,欧美,国产一区二区三区| 国产三级在线视频| 亚洲aⅴ乱码一区二区在线播放| 亚洲美女搞黄在线观看| 亚洲成色77777| 99热网站在线观看| 一个人观看的视频www高清免费观看| 亚洲av在线观看美女高潮| 精品国产露脸久久av麻豆 | 亚洲欧美日韩无卡精品| or卡值多少钱| 国产精品久久久久久久久免| 亚洲av二区三区四区| 亚洲国产精品专区欧美| 国产精品嫩草影院av在线观看| 久久久a久久爽久久v久久| 永久免费av网站大全| or卡值多少钱| 如何舔出高潮| 国产精品1区2区在线观看.| 日本wwww免费看| 丰满少妇做爰视频| 久久久久久久亚洲中文字幕| 久久热精品热| 中国国产av一级| 午夜福利成人在线免费观看| 最近中文字幕2019免费版| 国产成人91sexporn| 18禁裸乳无遮挡免费网站照片| 亚洲人成网站高清观看| 日韩一本色道免费dvd| 天美传媒精品一区二区| 高清毛片免费看| 成年女人看的毛片在线观看| 在线免费十八禁| 97精品久久久久久久久久精品| 秋霞伦理黄片| 精品人妻视频免费看| 少妇猛男粗大的猛烈进出视频 | 天天躁日日操中文字幕| 99久久人妻综合| 全区人妻精品视频| 欧美精品国产亚洲| 国产精品一区www在线观看| 在线播放无遮挡| 久久精品久久久久久噜噜老黄| 好男人视频免费观看在线| 免费黄频网站在线观看国产| 男的添女的下面高潮视频| av在线天堂中文字幕| 蜜桃亚洲精品一区二区三区| .国产精品久久| 国内揄拍国产精品人妻在线| 亚洲高清免费不卡视频| 成人美女网站在线观看视频| 久久久亚洲精品成人影院| 亚洲国产精品专区欧美| 亚洲国产欧美在线一区| 国产麻豆成人av免费视频| 久久这里有精品视频免费| 国产黄色免费在线视频| 男女下面进入的视频免费午夜| 十八禁网站网址无遮挡 | 久久久久久久久久久免费av| 亚洲av男天堂| a级毛色黄片| 少妇高潮的动态图| 国产成年人精品一区二区| 最近的中文字幕免费完整| 国产一区二区三区综合在线观看 | 精品一区二区三区人妻视频| 久久精品综合一区二区三区| 又爽又黄无遮挡网站| av天堂中文字幕网| 免费看美女性在线毛片视频| 亚洲三级黄色毛片| 婷婷六月久久综合丁香| 国产人妻一区二区三区在| www.av在线官网国产| 日韩av免费高清视频| 欧美 日韩 精品 国产| 中文天堂在线官网| 欧美成人a在线观看| 国产午夜精品一二区理论片| av免费观看日本| 亚洲精品日本国产第一区| 免费看光身美女| 麻豆国产97在线/欧美| 免费黄网站久久成人精品| 91午夜精品亚洲一区二区三区| 一个人观看的视频www高清免费观看| 美女被艹到高潮喷水动态| 国产精品av视频在线免费观看| 乱系列少妇在线播放| 女人久久www免费人成看片| 精品久久久久久久久av| 蜜桃久久精品国产亚洲av| 自拍偷自拍亚洲精品老妇| 国产亚洲av嫩草精品影院| av在线亚洲专区| 亚洲熟妇中文字幕五十中出| 亚洲精品国产av蜜桃| 国产黄色免费在线视频| 国产精品久久视频播放| 亚洲精华国产精华液的使用体验| 日韩欧美三级三区| 日本黄色片子视频| 精品熟女少妇av免费看| 欧美一区二区亚洲| 色尼玛亚洲综合影院| 日韩欧美精品v在线| 亚洲四区av| 搞女人的毛片| 国产一区亚洲一区在线观看| 超碰97精品在线观看| 大话2 男鬼变身卡| 午夜福利视频精品| 在线播放无遮挡| 国产成人精品婷婷| 内地一区二区视频在线| 亚洲精品亚洲一区二区| 性色avwww在线观看| 亚洲,欧美,日韩| 国产成人精品婷婷| 别揉我奶头 嗯啊视频| 欧美日韩在线观看h| 午夜爱爱视频在线播放| 人体艺术视频欧美日本| 日本免费a在线| 99久久精品一区二区三区| 美女主播在线视频| 国产黄色视频一区二区在线观看| 成人亚洲欧美一区二区av| 我要看日韩黄色一级片| 日本一本二区三区精品| 少妇被粗大猛烈的视频| 亚洲精品成人av观看孕妇| 在线天堂最新版资源| 国产黄片视频在线免费观看| 久久久久久久久中文| 少妇的逼好多水| 免费黄频网站在线观看国产| 少妇丰满av| 蜜桃亚洲精品一区二区三区| 久久久亚洲精品成人影院| 性色avwww在线观看| 岛国毛片在线播放| 亚洲av电影在线观看一区二区三区 | 麻豆成人av视频| 高清av免费在线| 精品人妻一区二区三区麻豆| 91aial.com中文字幕在线观看| 亚洲精品日本国产第一区| 国产黄片美女视频| 欧美性猛交╳xxx乱大交人| 成人综合一区亚洲| 日韩制服骚丝袜av| 啦啦啦啦在线视频资源| 日韩人妻高清精品专区| 18禁裸乳无遮挡免费网站照片| 国产精品99久久久久久久久| 国产亚洲午夜精品一区二区久久 | 国语对白做爰xxxⅹ性视频网站| 免费av观看视频| 国产欧美另类精品又又久久亚洲欧美| 亚洲av电影不卡..在线观看| 国产av在哪里看| 男人爽女人下面视频在线观看| 亚洲成色77777| 啦啦啦中文免费视频观看日本| 中文资源天堂在线| 亚洲国产欧美人成| 国产日韩欧美在线精品| 高清日韩中文字幕在线| 精品人妻一区二区三区麻豆| 欧美bdsm另类| 91精品国产九色| 91aial.com中文字幕在线观看| 日韩一区二区三区影片| 午夜福利高清视频| 日韩亚洲欧美综合| 网址你懂的国产日韩在线| 日本免费a在线| 久久亚洲国产成人精品v| 97在线视频观看| 小蜜桃在线观看免费完整版高清| 欧美另类一区| 中文字幕av在线有码专区| 高清av免费在线| 一级爰片在线观看| av免费在线看不卡| 亚洲av在线观看美女高潮| 精品久久久久久久久亚洲| 啦啦啦啦在线视频资源| 国产极品天堂在线| 国产成人aa在线观看| 亚洲欧美一区二区三区黑人 | 亚洲真实伦在线观看| 午夜激情欧美在线| 国产一级毛片七仙女欲春2| 少妇猛男粗大的猛烈进出视频 | 日韩亚洲欧美综合| 网址你懂的国产日韩在线| 日本爱情动作片www.在线观看| 亚洲三级黄色毛片| 久久99热这里只有精品18| 亚洲av不卡在线观看| 久久99蜜桃精品久久| 久久久久性生活片| 边亲边吃奶的免费视频| 午夜福利视频1000在线观看| 看免费成人av毛片| 校园人妻丝袜中文字幕| 国产伦一二天堂av在线观看|