Extending the review of CTL models to Kripke model transition systems

• Grant number: 12/16308-1
• Support Opportunities: Research Grants - Visiting Researcher Grant - Brazil
• Start date: August 20, 2012
• End date: August 19, 2013
• Field of knowledge: Physical Sciences and Mathematics - Computer Science - Computing Methodologies and Techniques
• Principal Investigator: Renata Wassermann
• Grantee: Renata Wassermann
• Visiting researcher: Aline Maria Santos Andrade
• Visiting researcher institution: Universidade Federal da Bahia (UFBA). Instituto de Matemática, Brazil
• Host Institution: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brazil

Abstract

The Kripke modal transitions systems are adequate models to represent systems with partial information as software specifications with incomplete requirements and abstractions of CTL models. The Kripke modal transitions systems are models of the Mu-calculus and can be submitted to model checking. When a desired property is not verified by model checking, the model must be changed to satisfy the property. Modifying automatically models is a research challenge nowadays and exist several proposals to change CTL models based on review and update of beliefs. This project proposes investigate the problem of review and update Kripke modal transitions systems starting from results of review and update CTL models. (AU)