Hoy ha comenzado el curso de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.
En la clase de hoy se ha presentado la asignatura y se ha comentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Otter/Mace, ACL2, PVS e Isabelle/HOL.
Read More “RA2010: Visión panorámica del razonamiento automático”
EL 29 de Octubre se publicó un nuevo artículo de vrificación: Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude, Science of Computer Programming en la revista Science of Computer Programming.
Los autores del artículo son Kyungmin Bae (de la University de Illinois en Urbana-Champaign), Peter Csaba Olveczky (de la Universidad de Oslo), Thomas Huining Feng, Edward A. Lee y Stavros Tripakis (los tres últimos, de la Universidad de California en Berkeley).
El resumen del artículo es
This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.
Una versión previa del artículo, de libre acceso, es Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude.