O2.
To specify the interactions between computees and the
formation of societies of computees emerging from such interactions.
O2
will deliver a formal logic-based framework to characterise
the interactions between computees in a rule-based manner,
either by relying on protocols shared and agreed upon by
all computees in a given society, or by interaction patterns
that are specific to individual computees and possibly different
for different computees. O2 will be validated by (a) subjective
criteria: "is the framework rich enough to accommodate varieties
of interactive behaviours of computees?", "is the framework
suitable for interactions taking place in applications where
protocols cannot be imposed in advance, due to the complex
nature of global computing environments?"; "how can individual
interaction patterns be combined, and which global properties
will then hold?" and (b) objective criteria: "how do such
interaction patterns relate to existing protocols like those
envisaged by standardisation bodies?" .
O3.
To provide a computational framework in which the expected
behaviour of the computees is achieved.
O3
will deliver a computational counterpart to the logic-based
models developed within objectives O1-O2, in the form of
advanced extensions and integration of existing computational
logic proof procedures. O3 will be validated by (a) subjective
criteria: the computational framework should fall within
the realms of logic and should provably correspond to the
models in O1-O2, in that it should allow to automatise computees
so that they exhibit behaviour as specified in O1-O2; and
(b) objective criteria: ratification of the proposed framework
by peer review and by testing on concrete examples .
O4.
To identify and specify desired properties that should
be satisfied by the individual computees as well as by the
societies of computees as a whole.
O4 will propose a substantial number of interesting properties,
such as: characterisation of computees according to their
social behaviour (e.g. their "selfishness" or "altruism"),
termination of interactions between computees, effectiveness
of communication towards the achievement of the computees'
objectives, compliance of the computees' behaviour to interaction
protocols, and so on. O4 will be validated by (a) subjective
criteria: "are any of the identified properties useful for
concrete applications?"; "do they provide guidance in designing
and specifying practical applications?" and (b) objective
criteria: "how do the identified properties relate to existing
ones, e.g. as provided by game-theoretic accounts?" .
O5.
To verify when computees and societies of computees satisfy/violate
these properties.
O5
will provide formal verification of the properties identified
in O4, without having to resort to empirical simulation
as a way of predicting behaviour of concrete realisations
of (societies of) computees. In particular, we will prove/disprove
properties of societies given properties of the individual
computees inhabiting them. O5 will be validated by (a) subjective
criteria: "is the logic-based formal and computational framework
developed in O1-O3 sufficiently rich to support the verification
of properties?" and (b) objective criteria: "how does the
resulting framework for verification compare with existing
deductive and inductive approaches to validation?"
.
O6.
To evaluate and validate the framework by a series of
controlled experiments.
O6
will deliver an empirical study of computees and their societies,
grounded on a series of controlled experiments on a prototype
demonstrator. This experimental process will test the models
developed in O1-O5 under different conditions by varying
the parameters of the framework (such as the reasoning capabilities
of the individual computees, their mode of communication
and interaction, the scale of density of computees in a
society, the location of computees, and so on). The theoretical
results from O1-O5 will make predictions that can be tested
by experiments. These experiments can also demonstrate unforeseen
behaviour, which can guide us to further properties to specify
and verify formally, within O4-O5. O6 will also show that
the logic-based framework developed can provide a practical
basis for the design of classes of systems and applications
which require aggregate behaviour of computational entities
.