Publications
Fairness in Non-Repudiation Protocols.
Wojciech Jamroga, Sjouke Mauw and Matthijs Melissen; Proceedings of the 7th International Workshop on Security and Trust Management (to appear)
We indicate two problems with the specifications of fairness
that are currently used for the verification of non-repudiation and other
fair-exchange protocols. The first of these problems is the implicit
assumption of perfect information. The second problem is the possible
lack of effectiveness. We solve both problems in isolation by giving new
definitions of fairness, but leave the combined solution for further work.
Moreover, we establish a hierarchy of various definitions of fairness, and
indicate the consequences for existing work.
Doubtful Deviations and Farsighted Play.
Wojciech Jamroga and Matthijs Melissen; Progress in Artificial Intelligence, Proceedings of the 15th Portuguese Conference on Artificial Intelligence
Nash equilibrium is based on the idea that a strategy profile is stable
if no player can benefit from a unilateral deviation. We observe that some
locally rational deviations in a strategic form game may not be profitable anymore
if one takes into account the possibility of further deviations by the other
players. As a solution, we propose the concept of farsighted pre-equilibrium, which
takes into account only deviations that do not lead to a decrease of the player’s
outcome even if some other deviations follow. While Nash equilibria are taken to
include plays that are certainly rational, our pre-equilibrium is supposed to rule
out plays that are certainly irrational. We prove that positional strategies are
sufficient to define the concept, study its computational complexity, and show that
pre-equilibria correspond to subgame-perfect Nash equilibria in a meta-game
obtained by using the original payoff matrix as arena and the deviations as moves.
Attack-Defense Trees and Two-Player Binary Zero-Sum Extensive Form Games Are Equivalent.
Barbara Kordy, Sjouke Mauw, Matthijs Melissen and Patrick Schweitzer; Proceedings of GameSec 2010
Attack–defense trees are used to describe security weaknesses
of a system and possible countermeasures. In this paper, the connection
between attack–defense trees and game theory is made explicit. We show
that attack–defense trees and binary zero-sum two-player extensive form
games have equivalent expressive power when considering satisfiability,
in the sense that they can be converted into each other while preserving
their outcome and their internal structure.
The Generative Capacity of the Lambek–Grishin Calculus: A New Lower Bound.
Proceedings of the 14th Formal Grammar conference, Bordeaux, July 2009.
The Lambek–Grishin calculus LG is a categorial grammar obtained by turning the one-sided sequents of the non-associative Lambek calculus NL into two-sided sequents, and adding interaction postulates between the two families of connectives thus obtained. In this paper, we prove a new lower bound on the generative capacity of LG,
namely the class of languages that are the intersection of a context-free language and the permutation closure of a context-free language. This implies that LG recognizes languages like {a^n b^n c^n d^n e^n | n ∈ N} and the
permutation closure of {a^n b^n c^n | n ∈ N}.
Attack-Defense Trees and Two-Player Binary Zero-Sum Extensive Form Games Are Equivalent.
Barbara Kordy, Sjouke Mauw, Matthijs Melissen and Patrick Schweitzer; Proceedings of GameSec 2010
The Generative Capacity of the Lambek–Grishin Calculus: A New Lower Bound.
Proceedings of the 14th Formal Grammar conference, Bordeaux, July 2009 (in print).
The Lambek–Grishin calculus LG is a categorial grammar obtained by turning the one-sided sequents of the non-associative Lambek calculus NL into two-sided sequents, and adding interaction postulates between the two families of connectives thus obtained. In this paper, we prove a new lower bound on the generative capacity of LG,
namely the class of languages that are the intersection of a context-free language and the permutation closure of a context-free language. This implies that LG recognizes languages like {a^n b^n c^n d^n e^n | n ∈ N} and the
permutation closure of {a^n b^n c^n | n ∈ N}.
Lambek–Grishin Calculus Extended to Connectives of Arbitrary Arity.
Master's thesis, Cognitive Artificial Intelligence, Universiteit Utrecht.
In my thesis, I introduce the generalized Lambek–Grishin calculus and study its properties. The second part of this thesis studies the Lambek calculus and the Lambek–Grishin calculus from the perspective of formal language theory. The main result of this thesis is a new lower-bound on the generative complexity of the Lambek–Grishin calculus.
Lambek–Grishin Calculus Extended to Connectives of Arbitrary Arity.
Proceedings of the 20th Belgian-Netherlands Conference on Artificial Intelligence, Enschede, October 2008, pp 161-168.
This paper introduces Lambek–Grishin calculus for n-ary connectives, which can be seen as a generalization of binary and unary Lambek–Grishin calculus. A cut-free presentation of the calculus is showed, proving the decidability of the calculus. Finally we investigate the symmetries of the calculus by making use of group theory.
A solution to the emptiness problem for Lambek calculus and some of its extensions.
Proceedings of the 2nd NSVKI Student Conference, Utrecht, June 2008, pp. 19-24.
This paper presents a way of solving the emptiness problem, that is the problem of telling whether a given
language contains no strings at all, for associative and nonassociative Lambek calculus, and the logic of pure residuation in general. The corectness of this method is proved by first converting the Lambek grammar to context-free grammar, and then solving the emptiness problem for context-free grammar.
See also the other articles I wrote for my BSc and MSc courses in Cognitive Artificial Intelligence.