We present a formalism to handle finite state concurrent systems in a mechanical way. In such a formalism we can axiomatically define concurrent systems by means of a branching time language. We show that, starting from the axiomatic description of a concurrent system, we can obtain automatically a finite Kripke model H such that theorem proving is reduced to model checking with respect to H. By means of such a formal procedure, we can model a large class of concurrent systems including Petri nets, CSP, Interaction Systems and so on. A tool has been implemented to produce a Kripke model from an axiomatical description of a concurrent system and to perform model checking on it.

A temporal logic approach to specify and to prove properties of finite state concurrent systems

DANELUTTO, MARCO;
1989-01-01

Abstract

We present a formalism to handle finite state concurrent systems in a mechanical way. In such a formalism we can axiomatically define concurrent systems by means of a branching time language. We show that, starting from the axiomatic description of a concurrent system, we can obtain automatically a finite Kripke model H such that theorem proving is reduced to model checking with respect to H. By means of such a formal procedure, we can model a large class of concurrent systems including Petri nets, CSP, Interaction Systems and so on. A tool has been implemented to produce a Kripke model from an axiomatical description of a concurrent system and to perform model checking on it.
1989
9783540516590
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11568/7664
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact