Mes: junio 2008

Wiebe Van der Hoek

Social laws are set of rules with

• a goal of some desirable behaviour
• constrints the behaviour of the agents
• forbides perfoorminag actions in certain cases

Alternating-time Temporal Logic (ATL) is a framework that demonstrates that properties as effectiveness (goal satisfaction), feasibility (constrains satisfaction) and synthesis (find laws for observed properties) can be dealed with it. It can express social laws with legality of actions, and add deontic operations to language (off

Branching temporal logic is a natural way to see computations: linear in the past, branched in the future to solve non-determinism. Computation Tree Logic (CTL) is a popular logic (I used it in my PhD. Thesis). Its main problem is that has a exponential time complexity because it has to examine all possible models. Using model checking you can reduce, because you have to think only about one model (for instance, to check safety Aseuqrenot \phi and liveness are exhaustively checked. A good modelchecker shows you a trace of states that drivers to a failure, so the system can be improved. But another utility is using the trace as a plan (model checking as planning).

ATL uses branching to model the evolution of a system controlled by a set of agents that can affect the future by making choices. Path qualifiers A and E are replaced by cooperation modalities \(\langle \langle G \rangle \rangle \varphi\) meaning that a group G can cooperate to achieve \(\varphi\) or G have an strategy to force \(\varphi\). \(\langle \langle \empotyset \rangle \rangle\) is the same as \(A \land \langle \langle sigma \rangle \rangle \) is same as E. Satisfiability problem has exponential time complexity, but for \(mu\)-objectives is polynomial.

A social law ids formula is a pair \((\varphi,\beta)\) where \(\varphi\) is an ATL formula (objective) and \(\beta\) is a behavioural constraint. Behavioural constraints have to be reasonable (every agent has to do something)., A law is effective iff \(\[S \dag \beta, q_0….|= \langle \langle \rangle \rangle Box \varphi\]\) Properties of update (look for them too):

• closure
• idempotence
• implementation preserves universal properties
• existential properties are anti-preserved

So the effectiveness problem is: given S and a social formula \((\varphi,\beta)\), calculate \(S \dag \beta\) and check \(\langle \langle \rangle \rangle \Box ¬\varphi\).

Problem: We try to constraint the behaviour of agents to guarantee some desirable property but, what happens if noboby complain it? To identify sufficient and necessary coalitions to the norm is needed. Consider how many agents can violate the rule and keep the systems effective.

• Sufficiency iff (look)
• Necessary iff (look)

Adding deontic notions:
obligations: \(\varphi\) is obligatory in no if \(\varphi\) is true on all n-conformant computations (formula)
permisions (i’ve lost it… too fast for me)

To sum up:

social laws that refer explicitly to legality of actions extend the framework to incorporate the notion of knowledge. Minimality and simplicity could be investigated in the framework. Synthesis of social laws using algorithms to give agents incentives to obide the law (Mechanism Design)

Blogged with the Flock Browser

Marco Schorlemmer, from the IIIA-CSIC, talks about ontology alignment.

Multi-agent interactions are based on illocutionary speech acts. But it is unfeasible: normative structures that regulate under which conditions agents can communicate and the meaning of the communication is needed. The illocutionary particles and agents roles are the interaction model, whereas the content language is the ontology. In the case of MAS, ontologies are previously engineered and agents coordinate or negotiate its use.

Share ontologies are useful for stable domains and closed communities because of the cost of maintaining them. Syntax, linguistic elements, synonyms in thesaurus, instances or hierarchies are all elements to be shared. But all that work is doe prior to interaction. But there’s equivalences that only can be detected while the communication process is being performed.

The idea is that the token of syntactic expression to be aligned is an interaction state transition where the type is the content of an illocution. So a minimal semantic agreement is needed previous to interactions and the matchings are been performed in different iterations while agents communicate. So we can transcend from a semantic web vision into a vision of a web of interactions.

Blogged with the Flock Browser