CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWe present a formalism for handling finite-state concurrent systems in a mechanical way. In the 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, etc. A procedure has been implemented to produce a Kripke model from an axiomatic description of a concurrent system and to perform model checking on it.
| Titolo: | A temporal logic approach to specify and to prove properties of finite state concurrent systems | |
| Autori: | ||
| Data di pubblicazione: | 1989 | |
| Abstract: | We present a formalism for handling finite-state concurrent systems in a mechanical way. In the 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, etc. A procedure has been implemented to produce a Kripke model from an axiomatic description of a concurrent system and to perform model checking on it. | |
| Handle: | http://hdl.handle.net/11562/430365 | |
| Appare nelle tipologie: | 04.01 Contributo in atti di convegno |
File in questo prodotto:
Copyright © 2021