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