Sujet : Logics for dynamically changing models.
Responsable : Igor Walukiewicz
Téléphone : 05 40 00 69 03
e-mail : igw@labri.fr
Équipe : Méthodes Formelles
Thème : Logic and complexity
Présentation du sujet : In a classical approach to
verification, a
system is modeled by a graph and a specification is
expressed by a
formula of some logic. The task of verification is reduced
to that of
model checking: verifying if the formula holds in a given
node of the
graph.
In some applications, in particular in control, the system
itself can
change in time. For example one can consider a network when
during its
operation
some of the connections may go down and some other
connections
may be put in. Of course, one can model this situation in
the
standard setting described in the paragraph above but the size of
graph will
often grow exponentially. The other solution is to consider
logics able
to talk about dynamic changes directly. Papers [LR03] and
[M96] define
and study such logics.
The goal of this mémoire will be to study formalisms
expressing
dynamic changes of system structure. In particular, the work
will
concentrate on expressive power and complexity of (some
variants of)
the logics proposed in the references.
Mot-clés : modal logics, games, computational compexity,
expressive power
Références :
[LR03] Christof Löding and Philipp Rohde. Solving the sabotage
game
is PSPACE-hard. Technical Report AIB-05-2003, RWTH Aachen,
2003. Available at
http://www-i7.informatik.rwth-aachen.de/d/publications/index.html
[M96] The Dynamic Logic of Permission, R. van der Meyden,
Journal of
Logic and Computation, Vol 6, No. 3 pp. 465-479, 1996. A
version of
this paper appeared at the IEEE Symposium on Logic in
Computer
Science, Philadelphia, 1990. Available at
http://www.cse.unsw.edu.au/~meyden/research/permissions.abs.html