Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Fantechi A., Gnesi S., Ristori G. An action based framework for verifying logical and behavioural properties of concurrent systems. In: CAV '91 - 3rd Workshop on Computer Aided Verification. (Aalborg, Denmark, 1 - 4 July 1991). Proceedings, vol. 575 pp. 66 - 78. K.G. Larsen, A. Skou (eds.). (Lecture notes in Computer Sciences). Springer, 1991.
A system is described which supports proofs of both behavioural and logical properties of concurrent systems; these are specified by means of a process algebra and its associated logics. The logic is an action based version of the branching time logic CTL which we call ACTL. It is interpreted over transition labelled structures while CTL is interpreted over state labelled ones. The core of the system are two existing tools, AUTO and EMC. The first builds the labelled transition system corresponding to a term of a process algebra and permits proof of equivalence and simplification of terms, while the second checks the validity of CTL logical formulae. The integration is realized by means of two translation functions from the action based branching time logic ACTL to CTL and from transition-labelled to state-labelled structures. The correctness of the integration is guaranteed by the proof that the two functions when coupled preserve satisfiability of logical formulae.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional