Finite-state machines, a simple class of finite Petri nets, are equipped with a truly concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends classic bisimulation equivalence over labeled transition systems and which is checked in a distributed manner, without necessarily building a global model of the overall behavior. An associated distributed modal logic, called basic team modal logic(BTML, for short), is presented and shown to be coherent with team equivalence: two markings are team equivalent if and only if they satisfy the same BTML formulae.

Roberto Gorrieri (2018). Verification of finite-state machines: A distributed approach. THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 96, 65-80 [10.1016/j.jlamp.2017.11.005].

Verification of finite-state machines: A distributed approach

Roberto Gorrieri
2018

Abstract

Finite-state machines, a simple class of finite Petri nets, are equipped with a truly concurrent, bisimulation-based, behavioral equivalence, called team equivalence, which conservatively extends classic bisimulation equivalence over labeled transition systems and which is checked in a distributed manner, without necessarily building a global model of the overall behavior. An associated distributed modal logic, called basic team modal logic(BTML, for short), is presented and shown to be coherent with team equivalence: two markings are team equivalent if and only if they satisfy the same BTML formulae.
2018
Roberto Gorrieri (2018). Verification of finite-state machines: A distributed approach. THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 96, 65-80 [10.1016/j.jlamp.2017.11.005].
Roberto Gorrieri
File in questo prodotto:
Eventuali allegati, non sono esposti

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/11585/669223
 Attenzione

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

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