Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Vaandrager F. Action versus state based logics for transition systems. In: LITP Spring School on Theoretical Computer Science. (La Roche Posay, France, April 1990). Proceedings, pp. 407 - 419. I. Guessarian (ed.). (Lecture notes in computer science, vol. 469). Springer, 1990.
A temporal logic based all actions rather than on states is presented and interpreted over labelled transition systems. It is proved that it has essentially the same power as CTL, a temporal logic interpreted over Kripke structures. The relationship between the two logics is established by introducing two mappings from Kripke structures to labelled transition systems and viceversa and two transformation functions between the two logics which preserve truth. A branching time version of the action based logic is also introduced. This new logic for transition systems can play an important role as an imermediate between Hennessy-Milner Logic and the modal μ-calculus. It is sufficiently expressive to describe safety and liveness properties but permits model checking in linear time.
Subject Transition System

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