Semantic Embedding of Petri Nets into Event-B
<|reference_start|>Semantic Embedding of Petri Nets into Event-B: We present an embedding of Petri nets into B abstract systems. The embedding is achieved by translating both the static structure (modelling aspect) and the evolution semantics of Petri nets. The static structure of a Petri-net is captured within a B abstract system through a graph structure. This abstract system is then included in another abstract system which captures the evolution semantics of Petri-nets. The evolution semantics results in some B events depending on the chosen policies: basic nets or high level Petri nets. The current embedding enables one to use conjointly Petri nets and Event-B in the same system development, but at different steps and for various analysis.<|reference_end|>
@article{attiogbe2005semantic,
    title={Semantic Embedding of Petri Nets into Event-B},
    author={Christian Attiogbe},
    journal={arXiv preprint arXiv:cs/0510073},
    year={2005},
    archivePrefix={arXiv},
    eprint={cs/0510073},
    primaryClass={cs.LO}
}