• <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)用效果
    久久久久久久亚洲中文字幕| 我要搜黄色片| 日本五十路高清| 日韩在线高清观看一区二区三区| 久久人人爽人人片av| 99国产精品一区二区蜜桃av| 国产一区二区在线观看日韩| 国产精品99久久久久久久久| 亚洲人成网站在线播| 久久久久九九精品影院| 成年女人永久免费观看视频| 国产三级在线视频| 一个人看的www免费观看视频| 十八禁国产超污无遮挡网站| 国产欧美日韩精品一区二区| 联通29元200g的流量卡| 在线播放无遮挡| 国产成人freesex在线| 亚洲欧美精品自产自拍| 久久精品久久久久久噜噜老黄 | 校园人妻丝袜中文字幕| 一边摸一边抽搐一进一小说| 能在线免费观看的黄片| 麻豆av噜噜一区二区三区| 亚洲av电影不卡..在线观看| 国产精品伦人一区二区| 欧美成人一区二区免费高清观看| 亚洲伊人久久精品综合 | 久久99热这里只有精品18| 亚洲精品久久久久久婷婷小说 | 久久精品综合一区二区三区| 亚洲欧洲日产国产| 国产精品一区二区三区四区久久| 丰满人妻一区二区三区视频av| 长腿黑丝高跟| 美女xxoo啪啪120秒动态图| 性色avwww在线观看| 久99久视频精品免费| 蜜桃亚洲精品一区二区三区| 日本av手机在线免费观看| 国产av在哪里看| 欧美性感艳星| 少妇熟女aⅴ在线视频| 秋霞伦理黄片| 国产成人a区在线观看| 午夜爱爱视频在线播放| 国产成人福利小说| 亚洲欧美精品自产自拍| av专区在线播放| 国产成人aa在线观看| 国产黄a三级三级三级人| 精品一区二区三区人妻视频| 日韩一区二区视频免费看| 欧美另类亚洲清纯唯美| 中文字幕免费在线视频6| 色视频www国产| 超碰97精品在线观看| 久久久久性生活片| 久久久a久久爽久久v久久| 欧美高清成人免费视频www| 免费av观看视频| 中国美白少妇内射xxxbb| 国产成人freesex在线| 在线a可以看的网站| 日韩人妻高清精品专区| 又粗又硬又长又爽又黄的视频| 国产黄片视频在线免费观看| 非洲黑人性xxxx精品又粗又长| 18禁动态无遮挡网站| 天堂影院成人在线观看| 一级毛片aaaaaa免费看小| 色综合色国产| 日韩一本色道免费dvd| 亚洲国产精品sss在线观看| 国产精品一区二区性色av| 在线a可以看的网站| 欧美最新免费一区二区三区| 日本熟妇午夜| 欧美成人免费av一区二区三区| 乱系列少妇在线播放| 听说在线观看完整版免费高清| 看非洲黑人一级黄片| 午夜福利网站1000一区二区三区| 永久免费av网站大全| 成人毛片a级毛片在线播放| 日韩成人伦理影院| 大香蕉久久网| 国产精品久久久久久久电影| 国产乱人视频| 午夜日本视频在线| 欧美精品一区二区大全| 边亲边吃奶的免费视频| 午夜福利网站1000一区二区三区| 日本色播在线视频| 国产精品一区二区三区四区久久| 校园人妻丝袜中文字幕| 热99re8久久精品国产| 观看免费一级毛片| 天天一区二区日本电影三级| 麻豆久久精品国产亚洲av| 欧美日韩精品成人综合77777| 男女边吃奶边做爰视频| 久久久久久大精品| 性插视频无遮挡在线免费观看| 能在线免费看毛片的网站| 国模一区二区三区四区视频| 美女cb高潮喷水在线观看| 免费黄色在线免费观看| 中文字幕免费在线视频6| 午夜免费男女啪啪视频观看| 全区人妻精品视频| 亚洲欧洲国产日韩| 亚洲精品国产成人久久av| 在现免费观看毛片| 国产久久久一区二区三区| 国产午夜精品一二区理论片| 亚洲成色77777| 欧美日韩在线观看h| 亚洲怡红院男人天堂| 听说在线观看完整版免费高清| 精品欧美国产一区二区三| 免费观看精品视频网站| 欧美日韩精品成人综合77777| 精品久久久久久久末码| 精品国内亚洲2022精品成人| 一区二区三区高清视频在线| 免费观看性生交大片5| 国产在线一区二区三区精 | www.色视频.com| 99久国产av精品国产电影| 国产精品野战在线观看| 看非洲黑人一级黄片| 六月丁香七月| 波多野结衣巨乳人妻| 黄片无遮挡物在线观看| 国产在视频线精品| 国产伦理片在线播放av一区| 美女国产视频在线观看| 久久精品夜色国产| 亚洲最大成人中文| 国产一区二区在线av高清观看| 一级黄片播放器| 伊人久久精品亚洲午夜| АⅤ资源中文在线天堂| 中文字幕免费在线视频6| 久久精品91蜜桃| 淫秽高清视频在线观看| 尤物成人国产欧美一区二区三区| 国产精品国产三级专区第一集| 最近中文字幕高清免费大全6| 别揉我奶头 嗯啊视频| 国产精品一区二区在线观看99 | 免费观看在线日韩| 深爱激情五月婷婷| 国产精品麻豆人妻色哟哟久久 | 一级黄色大片毛片| 亚洲精品自拍成人| 国产成人免费观看mmmm| 18禁在线播放成人免费| 国产精品嫩草影院av在线观看| 精品99又大又爽又粗少妇毛片| 91精品一卡2卡3卡4卡| 在线观看一区二区三区| 少妇猛男粗大的猛烈进出视频 | 99久国产av精品| 成人亚洲欧美一区二区av| 国产成人精品婷婷| 中文字幕精品亚洲无线码一区| 欧美高清成人免费视频www| 亚洲乱码一区二区免费版| 日韩av在线大香蕉| 一级爰片在线观看| 亚洲精品乱码久久久久久按摩| 一个人免费在线观看电影| av黄色大香蕉| 只有这里有精品99| 国产在视频线精品| 免费看光身美女| 亚州av有码| 能在线免费观看的黄片| 午夜免费男女啪啪视频观看| 精品人妻视频免费看| 久久久久九九精品影院| 久久久久免费精品人妻一区二区| 99久久精品热视频| 久久久久性生活片| 三级国产精品欧美在线观看| 欧美zozozo另类| 成人美女网站在线观看视频| 男女下面进入的视频免费午夜| 国产老妇伦熟女老妇高清| 看黄色毛片网站| 欧美精品一区二区大全| 日日撸夜夜添| 男人的好看免费观看在线视频| 国产乱人偷精品视频| 可以在线观看毛片的网站| 精品国产露脸久久av麻豆 | 国产白丝娇喘喷水9色精品| 人妻夜夜爽99麻豆av| 成人毛片a级毛片在线播放| 只有这里有精品99| 久久精品综合一区二区三区| 国产精品嫩草影院av在线观看| 99热6这里只有精品| 国产又黄又爽又无遮挡在线| 国产免费又黄又爽又色| 九草在线视频观看| 亚洲av中文av极速乱| 亚洲精品成人久久久久久| 国产午夜精品久久久久久一区二区三区| 亚洲18禁久久av| 亚洲aⅴ乱码一区二区在线播放| 亚洲国产精品成人综合色| 美女cb高潮喷水在线观看| 免费在线观看成人毛片| 国产 一区 欧美 日韩| 日韩,欧美,国产一区二区三区 | 波多野结衣高清无吗| 国产精品国产三级国产av玫瑰| 亚洲18禁久久av| 亚洲婷婷狠狠爱综合网| 久久久国产成人精品二区| 国产伦一二天堂av在线观看| 欧美精品一区二区大全| 亚洲精品乱久久久久久| av卡一久久| 久热久热在线精品观看| 国产在线男女| 我的老师免费观看完整版| 亚洲18禁久久av| 69av精品久久久久久| 久久这里有精品视频免费| 久久精品夜夜夜夜夜久久蜜豆| 国产成人aa在线观看| av福利片在线观看| 岛国在线免费视频观看| 91狼人影院| 亚洲自偷自拍三级| 国产乱人偷精品视频| 亚洲精品,欧美精品| 国产亚洲精品久久久com| 国产精品乱码一区二三区的特点| 国产亚洲午夜精品一区二区久久 | 精品无人区乱码1区二区| 九九在线视频观看精品| av卡一久久| 中国美白少妇内射xxxbb| 日韩三级伦理在线观看| 又爽又黄a免费视频| 1000部很黄的大片| 男女国产视频网站| 99热全是精品| 成人综合一区亚洲| 九草在线视频观看| 日本午夜av视频| 高清av免费在线| 2021少妇久久久久久久久久久| 婷婷色av中文字幕| 国产在线一区二区三区精 | 麻豆成人av视频| 小说图片视频综合网站| 三级国产精品欧美在线观看| 日本与韩国留学比较| 日韩制服骚丝袜av| 日日撸夜夜添| 久久综合国产亚洲精品| 蜜桃亚洲精品一区二区三区| 国内精品一区二区在线观看| 美女大奶头视频| 亚洲高清免费不卡视频| 久久久久九九精品影院| 亚洲在线自拍视频| 纵有疾风起免费观看全集完整版 | av黄色大香蕉| 少妇的逼水好多| 1000部很黄的大片| 色综合站精品国产| 免费黄网站久久成人精品| 黄色日韩在线| 美女黄网站色视频| 最后的刺客免费高清国语| 国产高清三级在线| 国产成人精品久久久久久| 久久人人爽人人爽人人片va| 欧美xxxx黑人xx丫x性爽| 欧美潮喷喷水| 欧美又色又爽又黄视频| 99久久无色码亚洲精品果冻| 国产又黄又爽又无遮挡在线| 亚洲精品aⅴ在线观看| 在线观看美女被高潮喷水网站| 久久精品久久久久久久性| 国产精品.久久久| 国产精品一及| 男插女下体视频免费在线播放| 可以在线观看毛片的网站| 亚洲真实伦在线观看| 国产精品三级大全| 国产精华一区二区三区| 天堂网av新在线| 九九在线视频观看精品| 日本wwww免费看| 久久韩国三级中文字幕| 国产单亲对白刺激| 日韩在线高清观看一区二区三区| 在线观看av片永久免费下载| 99久久精品热视频| 国产高清有码在线观看视频| 51国产日韩欧美| 精品国内亚洲2022精品成人| 夫妻性生交免费视频一级片| 美女大奶头视频| 综合色av麻豆| 欧美色视频一区免费| 久久久久久久亚洲中文字幕| 一级黄色大片毛片| 男人舔女人下体高潮全视频| 一夜夜www| 国产精品国产三级国产专区5o | 自拍偷自拍亚洲精品老妇| 高清av免费在线| 男插女下体视频免费在线播放| 大又大粗又爽又黄少妇毛片口| 日韩欧美精品v在线| 欧美高清性xxxxhd video| 免费av观看视频| 中文欧美无线码| 青青草视频在线视频观看| 美女高潮的动态| 国产精品不卡视频一区二区| 波多野结衣高清无吗| 深爱激情五月婷婷| 国产单亲对白刺激| 精品少妇黑人巨大在线播放 | 视频中文字幕在线观看| 色视频www国产| 久久久久免费精品人妻一区二区| 91aial.com中文字幕在线观看| 欧美性猛交╳xxx乱大交人| 午夜爱爱视频在线播放| 国产伦精品一区二区三区四那| 男人舔奶头视频| 久久久久久大精品| 精品人妻熟女av久视频| 国产一区有黄有色的免费视频 | 国产乱人偷精品视频| 亚洲激情五月婷婷啪啪| 色播亚洲综合网| av在线老鸭窝| 日韩中字成人| 亚洲欧美中文字幕日韩二区| 特级一级黄色大片| 国产亚洲91精品色在线| 禁无遮挡网站| 十八禁国产超污无遮挡网站| 在线观看66精品国产| 日本wwww免费看| 少妇猛男粗大的猛烈进出视频 | 我的老师免费观看完整版| 日日撸夜夜添| 国产精品久久久久久av不卡| 欧美极品一区二区三区四区| 久久精品国产亚洲av涩爱| 久久热精品热| 天堂√8在线中文| 国产精品熟女久久久久浪| 日韩欧美国产在线观看| 小说图片视频综合网站| 国产成人91sexporn| 欧美xxxx黑人xx丫x性爽| 99久久人妻综合| 网址你懂的国产日韩在线| 哪个播放器可以免费观看大片| 色哟哟·www| 简卡轻食公司| 亚洲av中文字字幕乱码综合| 天天躁夜夜躁狠狠久久av| 色哟哟·www| 国产麻豆成人av免费视频| 国产伦精品一区二区三区四那| 国产精品综合久久久久久久免费| 又粗又硬又长又爽又黄的视频| 国内精品宾馆在线| 久久久精品大字幕| 国产高潮美女av| 有码 亚洲区| 久久精品夜色国产| 日韩在线高清观看一区二区三区| 亚洲av中文av极速乱| 日韩强制内射视频| 久久99热6这里只有精品| 色5月婷婷丁香| 精品人妻视频免费看| 国产黄片美女视频| 免费播放大片免费观看视频在线观看 | 欧美一区二区精品小视频在线| 亚洲aⅴ乱码一区二区在线播放| 日韩一区二区视频免费看| 22中文网久久字幕| 精品久久国产蜜桃| 亚洲人与动物交配视频| 亚洲精华国产精华液的使用体验| 国产av在哪里看| 校园人妻丝袜中文字幕| 如何舔出高潮| 国产白丝娇喘喷水9色精品| 久久精品夜夜夜夜夜久久蜜豆| 午夜福利在线观看吧| 色尼玛亚洲综合影院| 欧美区成人在线视频| 国产成年人精品一区二区| 精品一区二区三区视频在线| a级一级毛片免费在线观看| 欧美一区二区精品小视频在线| 欧美性猛交黑人性爽| 国产黄色视频一区二区在线观看 | av免费在线看不卡| 午夜精品在线福利| 一级毛片aaaaaa免费看小| 久久久午夜欧美精品| 欧美一区二区亚洲| 亚洲av电影不卡..在线观看| 国产黄片美女视频| 七月丁香在线播放| 毛片女人毛片| 欧美97在线视频| 2022亚洲国产成人精品| 一级二级三级毛片免费看| 成人鲁丝片一二三区免费| 欧美激情国产日韩精品一区| 国产不卡一卡二| 亚洲综合精品二区| 免费人成在线观看视频色| 国产av在哪里看| 99国产精品一区二区蜜桃av| 国产在线一区二区三区精 | eeuss影院久久| 一级毛片我不卡| 成人一区二区视频在线观看| 亚洲精品,欧美精品| 一二三四中文在线观看免费高清| 亚洲天堂国产精品一区在线| 中文天堂在线官网| 午夜亚洲福利在线播放| 欧美成人午夜免费资源| 大话2 男鬼变身卡| 亚洲av电影在线观看一区二区三区 | 国产免费又黄又爽又色| 亚洲精品久久久久久婷婷小说 | 久久精品国产亚洲网站| 黄色配什么色好看| 七月丁香在线播放| 热99re8久久精品国产| 色5月婷婷丁香| 久久精品国产自在天天线| 日本一二三区视频观看| 欧美97在线视频| 日韩人妻高清精品专区| 精品免费久久久久久久清纯| 人人妻人人澡人人爽人人夜夜 | 尾随美女入室| 少妇被粗大猛烈的视频| 亚洲av免费高清在线观看| 亚洲国产日韩欧美精品在线观看| 最新中文字幕久久久久| 1024手机看黄色片| 欧美日本视频| 久久婷婷人人爽人人干人人爱| av女优亚洲男人天堂| 天天一区二区日本电影三级| 在线免费观看的www视频| 麻豆乱淫一区二区| 成年版毛片免费区| АⅤ资源中文在线天堂| 欧美3d第一页| 国产高清不卡午夜福利| 国产精品人妻久久久影院| 非洲黑人性xxxx精品又粗又长| 久久精品国产亚洲av涩爱| 草草在线视频免费看| 亚洲国产精品成人久久小说| 看免费成人av毛片| 亚洲av男天堂| 精品无人区乱码1区二区| 精品酒店卫生间| 长腿黑丝高跟| 一卡2卡三卡四卡精品乱码亚洲| 两个人的视频大全免费| 一级二级三级毛片免费看| 高清在线视频一区二区三区 | 2022亚洲国产成人精品| 毛片一级片免费看久久久久| 国产淫语在线视频| 男人舔女人下体高潮全视频| 亚洲成人久久爱视频| 三级经典国产精品| 一级毛片电影观看 | 国产探花极品一区二区| 亚洲av福利一区| 99热这里只有精品一区| 国内少妇人妻偷人精品xxx网站| 色播亚洲综合网| 久久久久久久久中文| 国产三级中文精品| 亚洲av熟女| 国产激情偷乱视频一区二区| 久久99热这里只有精品18| 免费看日本二区| 色噜噜av男人的天堂激情| 三级毛片av免费| 一个人看的www免费观看视频| 男女国产视频网站| 国产大屁股一区二区在线视频| 国产午夜精品久久久久久一区二区三区| 美女cb高潮喷水在线观看| 天天一区二区日本电影三级| 麻豆国产97在线/欧美| 亚洲久久久久久中文字幕| 欧美又色又爽又黄视频| 日本一二三区视频观看| 人妻制服诱惑在线中文字幕| 国国产精品蜜臀av免费| 精品久久久久久久久久久久久| 国产三级在线视频| 国产淫片久久久久久久久| 欧美不卡视频在线免费观看| 欧美性猛交黑人性爽| 国产色爽女视频免费观看| 久久精品国产自在天天线| 免费在线观看成人毛片| 精品不卡国产一区二区三区| 免费看美女性在线毛片视频| 免费观看精品视频网站| 菩萨蛮人人尽说江南好唐韦庄 | 国产色婷婷99| 久久99热这里只有精品18| 又爽又黄无遮挡网站| 天天躁夜夜躁狠狠久久av| 18禁裸乳无遮挡免费网站照片| 两性午夜刺激爽爽歪歪视频在线观看| 久久久久久国产a免费观看| 久久人妻av系列| 亚洲美女视频黄频| 久久久国产成人精品二区| 国内少妇人妻偷人精品xxx网站| 午夜老司机福利剧场| 黄色一级大片看看| 免费大片18禁| 欧美变态另类bdsm刘玥| 免费人成在线观看视频色| 久久国产乱子免费精品| 99热全是精品| 国产爱豆传媒在线观看| 国产亚洲av嫩草精品影院| 亚洲成色77777| 亚洲欧美日韩卡通动漫| 欧美日韩国产亚洲二区| 成人特级av手机在线观看| 夜夜爽夜夜爽视频| 免费电影在线观看免费观看| 内地一区二区视频在线| 91av网一区二区| 成年免费大片在线观看| 日韩人妻高清精品专区| 欧美色视频一区免费| 精品国产露脸久久av麻豆 | 精品酒店卫生间| 我要搜黄色片| 99热精品在线国产| 日韩欧美三级三区| 99热这里只有精品一区| 欧美日韩在线观看h| 99热这里只有是精品在线观看| 国内少妇人妻偷人精品xxx网站| 大香蕉97超碰在线| 插逼视频在线观看| 嫩草影院入口| h日本视频在线播放| 卡戴珊不雅视频在线播放| 国产精品乱码一区二三区的特点| 欧美一区二区亚洲| 国产伦理片在线播放av一区| 舔av片在线| 国产精品野战在线观看| 日本猛色少妇xxxxx猛交久久| 99热这里只有是精品50| 亚洲精品乱久久久久久| 老师上课跳d突然被开到最大视频| 99久久精品热视频| 99久久成人亚洲精品观看| 久久这里只有精品中国| 亚洲久久久久久中文字幕| 免费播放大片免费观看视频在线观看 | 18禁裸乳无遮挡免费网站照片| 在线观看66精品国产| videossex国产| 人体艺术视频欧美日本| 能在线免费看毛片的网站| 最近中文字幕2019免费版| 日韩欧美精品免费久久| 精品国产一区二区三区久久久樱花 | 在线播放无遮挡| 亚洲av电影在线观看一区二区三区 | 国产午夜福利久久久久久| 男插女下体视频免费在线播放| 日本黄色视频三级网站网址| 99久久精品国产国产毛片| 国产午夜福利久久久久久| 亚洲精品国产av成人精品| 成年女人看的毛片在线观看| 午夜精品在线福利| 两个人的视频大全免费| 国产精品美女特级片免费视频播放器| 精品人妻偷拍中文字幕|