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