Modern computer systems involve dynamic interaction between various components. Naive logical modelling of dynamic interactions often leads to systems which are computationally more complex than the original problem. The aim of the project is to discover which aspects of such modellings cause intractability, and use this knowledge to design formal systems which faithfully reflect the complexity of the original problem, but are still expressive enough to capture its essential features.
We will undertake this research from both a logical and an algebraic perspective, and develop the mathematical methods as necessary for this. The general framework of combining logics was especially created to design systems which can capture different dimensions and their interactions. We will find out when interaction blocks transfer of tractability to the combinations, and use this knowledge to design tractable interactive systems. From the algebraic side, focussing on dynamic aspects of algebras of relations will allow us to develop algebras finely tuned for applications --- sufficiently expressive but not excessively complex.
The formalisms we develop will be evaluated with respect to both their theoretical complexity and their suitability for practical applications in the verification and specification of programs and distributed and multi-agent systems.