Research Interests


My main research interests focus on modal (epistemic, deontic, temporal) logics, and formal methods, with emphasis on the application of these to the specification and verification of real-time and multi-agent systems. Other interests include model checking of Java programs. I have published over 40 research papers in the above areas.

A real-time system is one in which the correctness of the computations depends not only on their logical correctness, but also on the time at which the result is produced. The formalism of such systems has successfully been used in safety-critical systems, planing, communication protocols, etc. Agents are autonomous, self-interested processes operating in a distributed system and interacting with one another as well as with the environment to reach a private goal. The formalism of multi-agent systems has successfully been used in a number of Information Technology areas such as software engineering, e-commerce, networks, automated argumentation, automated contracting, and others.

Having completed a PhD on (real-time) systems verification in 2003, I have published about 15 research papers on this and related topics. The approach I have pursued involves both a definition of an extension of the Bounded Model Checking (BMC) method to verification of universal branching time properties of real-time systems, and an implementation of this technique. This is the only method available that enables a translation of the real-time model checking problem to the SAT problem.

Since 2004 I have also focused on the area of specification and verification of multi-agent systems and I have published about 20 research papers on this and related topics. In this line I have worked on both defining and investigating modal logics for representing key attitudes of (real-time) multi­agent systems, such as their knowledge, awareness, and evolution of these over (real) time, and on developing model checking algorithms (with particular focus on the bounded model checking technique) for the verification of specifications of (real-time) multi-agent systems by means of a variety of temporal, epistemic and deontic languages. Key to the modal logics line is the study of the formal properties of (real-time) multi-agent systems, such as their expressivity, completeness, decidability, and computational complexity. Key to the model checking line is to develop a new efficient model checking techniques.

I am also one of the authors of VerICS model checker developed at Institute of Computer Science, Polish Academy of Sciences, under the supervision of doc. dr hab. Wojciech Penczek. By means of the tool a variety of systems have been verified, including protocols like Train-Gate-Controller, Fischer's mutual exclusion, Alternating Bit Protocol, Dining Cryptographers.

At present my work concentrates on developing modal logics for real-time multi-agent systems, and model checking of Java programs.

Thank you for showing an interest in my work.