Formal modelling of requirements and temporal multi-agent logics




Thesis defended on june 20th in the Institut Supérieur de l'Aéronautique et de l'Espace ( ISAE Toulouse, France).

Keywords

  • requirements
  • agents
  • roles
  • multi-strategies
  • strategy refinement

    • Jury

    Jean-Paul Bodeveix     president
    Julien Brunel     co-tutor
    David Chemouil     co-tutor
    Régine Laleau     report writer
    Nicolas Markey     report writer
    Sophie Pinchinat     examiner

    Abstract

    These works concern formal modelling of requirements and interactions between agents. We develop a modelling language for the requirements of a system to be elaborated, Khi. We also propose a temporal multi-agent logic, USL.

        To our knowledge, there is no formalisation, in the field of requirements engineering, dealing on the one hand with time and on the other hand with agents actions. This is what we propose with Khi. This language borrows from the Kaos method it means for the formally describing behavioral requirements and deriving from these requirements the operations specifications for a system. It also borrows from the Tropos-i* methods a conceptual frame enabling to express the question of the effective capacity of agents to ensure the satisfaction of the specifications assigned to them. We call this last question the "assignment problem". Thus, language Khi proposes an original synthesis enabling to formalise in an unique language the behavioral requirements of a system and the actions capacities of the agents in this system. Furthermore, Khi offers a conceptual frame enabling to express the assignment problem.

        To give Khi concepts a formalism and some means to solve the assignment problem, we also introduce a a temporal multi-agent logic, USL. IT is inspired from works in the domain such as ATLsc and SL. As these last formalisms, USL makes use of strategy contexts to express capacities of agents to ensure the satisfaction of temporal properties. USL is different from other existing formalisms by two mains aspects: first it uses non-deterministic strategies. We call them multi-strategies. So we can express properties of multi-strategy refinment. Furthermore, for USL we use executions in the system that may not be infinite. Thus we can formalise the notions of contradictory commitments for an agent and conflictual capacities of actions for a set of agents. We show that the expressivity of USL embeds the expressivity of pre-existing formalisms. This logic enables in particular to formalise the property, new in the field, of sustainable controle. It also enables to introduce predicates of comparison and equality between multi-strategies and/or strategies. A study of relations of dependencies between multi-strategies and/or strategies is also initiated with USL. We also show that the complexity of model-checking and satisfiability problems for USL is equivalent to that for pre-existing formalisms.

        Then we reduce the satisfaction of correction criteria expressing the assignment problem in Khi to instances of model-checking in an adequate version of USL, USLKhi. We give a resolution algorithm for this problem, it use a polynomial space. So, the development of Khi and the adequate use of USL enable to express, formalise and resolve the assignment problem. All these concepts is also illustrated by use of a case study figuring missions of spatial observations.