Most existing approaches to modelling computational entities and interactions between them result either in low-level implementations with no obvious logical characterisation, or in abstract specifications possibly employing quite expressive modalities without a computational counterpart. Approaches of the first kind are very difficult to verify and to use as models for designing systems with similar aims or applications within similar settings. Approaches of the second kind are computationally intractable in many cases, and therefore difficult to turn into systems or applications provably compliant with the given specifications. To bridge this gap, SOCS aims at supplying models of computees and interaction between them that lend themselves to concrete realisations which can be proven correct with respect to those models and can be used in practice to design systems and applications in the envisaged environments. These applications range from air traffic management systems, where different airlines, pilots and control centres work in a global and open environment, to electronic commerce applications which require modelling of groups of business entities in a global trading environment.

The formal models for (societies of) computees that we aim at providing have a computational counterpart that is operational and executable, but at the same time provably correct with respect to the formal models. The computational counterpart will be in the form of computational logic proof procedures, allowing to perform automatically the form of reasoning and exhibit the form of behaviour envisaged by the formal models. This computational counterpart will play a considerable role in providing a correct prototype demonstrator, to animate the societies of computees we aim at designing, and test the proposed approach on concrete scenaria of varying scales

The formal and computational models will require an integrated treatment of different features and behaviours of (societies of) computees. Amongst these features are the capability of dealing with dynamic environments and incomplete information about the environment and the knowledge and behaviour of the computees inhabiting the societies. The environment is dynamic as it is open, with computees joining and leaving societies and modifying their objectives and knowledge over time. The computees have incomplete information as they only have a partial view and knowledge of the environment and of other computees in the societies. Computees might even hold erroneous beliefs about other computees' objectives, availability of resources, knowledge and so on. In order to cope with the openness, incompleteness and misconceptions in their knowledge, computees might need to resort to making (intelligent) assumptions as well as communication with other computees. For example, suppose a computee c1 knows that another computee c2 has to complete a task by a given time t, and c1 is looking for a computee to delegate another task to. Then c1 can assume by default that c2 would not be a good candidate for this delegation until after t. Computees might need to negotiate in order to achieve their own objectives, as well as the objectives they share with other computees, for example by exchanging resources, tasks and knowledge

Some of the aspects outlined above have been studied already, both within computational logic boundaries and outside them, but in isolation. Their integration requires a considerable effort in synthesis as well as novel extensions in order to produce the functionalities of the societies we envisage. For example, there are well-known proposals for computational logic-based techniques for reasoning with incomplete information, and there are well-known techniques for assimilating new knowledge. It is not trivial to integrate the two to allow for knowledge assimilation during reasoning in such a way as to minimise the loss of any partial results of the reasoning process that remain valid after the assimilation.  

Back to: Workplan Menu