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.
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.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.