Model checking for the concurrent constraint paradigm

Article type: Other

Authors: Villanueva, Alicia

Affiliations: Dep. de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera, s/n, E‐46022 Valencia, Spain E‐mail: villanue@dsic.upv.es

Abstract: This paper abstracts the contents of the PhD dissertation which has been recently defended by the author. Although model checking was defined to automatically verify hardware, in the last decades it has been showed that it is possible to apply the technique also to software. The concurrent constraint paradigm is a simple but powerful computational model which we can use to specify reactive and hybrid systems. The thesis considers three of the timed languages of this paradigm. It presents two methods to apply the model checking technique to two different timed concurrent constraint languages, and it is also defined a denotational semantics which is fully abstract w.r.t. the operational behavior of another timed concurrent constraint language. This new semantics allows one to perform useful static analysis of programs.

Keywords: Timed concurrent constraint languages, model checking, denotational semantics

Journal: AI Communications, vol. 17, no. 2, pp. 93-94, 2004