Revising Specifications with CTL Properties using Bounded Model Checking

==========================================
Adolfo Neto
Departamento Acadêmico de Informática
Universidade Tecnológica Federal do Paraná
Fone: (41) 3310-4644 / Fax: (41) 3310-4646
Web: http://www.dainf.ct.utfpr.edu.br/~adolfo
Blog: http://professoradolfo.blogspot.com
==========================================

---------- Forwarded message ----------
From: Marcelo Finger <mfinger@ime.usp.br>
Date: Thu, Nov 13, 2008 at 2:27 PM
Subject: Seminário LIAMF dia 17/11/2008
To: liamf-anuncios@ime.usp.br
Cc: liamf-seminarios@ime.usp.br

Título: Revising Specifications with CTL Properties using Bounded Model Checking

Palestrantes:  Marcelo Finger e Renata Wassermann

Data:   17/11/2008, 14h30
Local:  Sala 03B, IME-USP

Resumo:

 During the process of software development, it is very common that
 inconsistencies arise between the formal specification and some
 desired property. Belief Revision deals with the problem of
 accommodating new information that may be inconsistent with an
 existing knowledge base.

 In this paper, we propose the use of belief revision techniques in
 order to deal with inconsistencies in formal specifications. The
 main problem to be solved is that the most well known results for
 belief revision only hold for logics which are monotonic and
 compact, while most discrete-time temporal logics used to
 express system properties -- and in particular, CTL --- are not
 compact.  We suggest the use of bounded model-checking, transforming
 the problem from CTL into classical propositional logic and then
 transforming back the results to suggest revisions to the user.

--
 Marcelo Finger
 Departamento de Ciencia da Computacao
 Instituto de Matematica e Estatistica | home page:
 Universidade de Sao Paulo             |   www.ime.usp.br/~mfinger
 Rua do Matao, 1010                    | Tel: +55 11 3091 6310, 3091 6135
 05508-090    Sao Paulo, SP     Brazil | Fax: +55 11 3091 6134, 3814 4135