Projekt PDT Logic (intern)
Probabilistic Doxastic Temporal (PDT) Logic is a formalism to represent and reason about probabilistic beliefs and their temporal evolutions in multi-agent systems.
In most realistic scenarios, an agent has only incomplete and inaccurate information about the actual state of the world, and thus considers several different worlds as actually being possible. As it receives new information (e.g., it observes some facts that currently hold), it has to update its beliefs about possible worlds such that they are consistent with new information. These updates can for example result in regarding some (previously considered possible) worlds as impossible or judging some worlds to be more likely than before. Thus, in addition to analyzing the set of worlds an agent believes to be possible, it is also expedient to quantify these beliefs in terms of probabilities. This provides means to specify fine-grained distinctions between the range of worlds that an agent considers possible but highly unlikely, and worlds that seem to be almost certainly the actual world.
When multiple agents are involved in such a setting, an agent may not only have varying beliefs regarding the facts of the actual world, but also regarding the beliefs of other agents. In many scenarios, the actions of one agent will not only depend on its belief of ontic facts (i.e., facts of the actual world), but also on its beliefs in some other agent's beliefs.
The aim of PDT Logic is to formalize reasoning about such beliefs in multi-agent settings. It provides a formalism which enables the representation of and reasoning about dynamically changing quantified temporal multi-agent beliefs through probability intervals. In contrast to related work, PDT Logic employs an explicit notion of time and thereby facilitates the expression of richer temporal relations.
By extending recent work on APT Logic, we have developed a general framework to represent and reason about belief changes in multi-agent systems with finite time-frames. A formal syntax and suitable semantics are provided to express these probabilistic beliefs and their temporal evolution.  Two alternative representation forms are defined to model problems in PDT Logic. Each representation form is well-suited for a certain type of problem domains. Sound and complete satisfiability checking procedures are given for both approaches. 
Additionally, we have developed an extension that enables the use of PDT Logic to reason about infinite Markovian streams of possible worlds . Another extension to PDT Logic gives a formal account of the abduction problem to enable abductive reasoning in PDT Logic. .
PDT Logic has been used as a formalism to model and analyze belief states of intruders and defenders in cyber-security scenarios. 
- Karsten Martiny, Ralf Möller: A Probabilistic Doxastic Temporal Logic for Reasoning about Beliefs in Multi-agent Systems Technical Report, IFIS, Universität zu Lübeck, 2015
- Karsten Martiny and Ralf Möller. Abduction in PDT Logic, Proceedings of the 28th Australasian Joint Conference on Artificial Intelligence 2015 (AI 2015)
- Karsten Martiny, Alexander Motzek and Ralf Möller. Formalizing Agents’ Beliefs for Cyber-Security Defense Strategy Planning, Proceedings of the 8th International Conference on Computational Intelligence in Security for Information Systems (CISIS 2015)
- Karsten Martiny and Ralf Möller. A Probabilistic Doxastic Temporal Logic for Reasoning about Beliefs in Multi-agent Systems, Proceedings of the 7th International Conference on Agents and Artificial Intelligence (ICAART 2015)
- Karsten Martiny and Ralf Möller. PDT Logic for Stream Reasoning in Multi-agent Systems , 6th International Symposium on Symbolic Computation in Software Science (SCSS 2014)