Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874848 | Journal of Logical and Algebraic Methods in Programming | 2018 | 16 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Roberto Gorrieri,