2020 | NumRes : Reasoning about Concurrent Game Structures with Numerical Resources (NumRes)


Axe : SciLex, IID
Sujet : IID-3 Data management, knowledge representation and reasoning, Scilex-1 Security of systems

Directeurs de thèse: Stéphane Demri et Lutz Strassburger
Doctorant: Ashwin Bhaskar
Début: 2021
Laboratoire gestionnaire : LSV
Autres partenaires : LIX
Productions scientifiques :
Ressources :

 


Contexte : Many logical formalisms exist for specifying the strategic behaviour of agents in multi-agent systems, including the alternating-time temporal logic ATL and extensions in which actions may consume or produce resources.

Formal relationships have been also established between model-checking problems for resource-bounded logics and decision problems for generalisations of VASS so that new complexity characterisations can be inherited from problems on counter machines. The main objective of the thesis proposal is to investigate the computational properties of resource-bounded logics and fragments, to design optimal decision procedures possibly based on proof systems (for instance, nested sequents), and to study its relationships with computational models such as alternating VASS and branching VASS (closely related to the linear logic MELL).