Andrea Burattin
Associate Professor
Technical University of Denmark
Encoding Petri Nets into CCS
B. Bogø, A. Burattin, A. Scalas
Abstract
This paper explores the problem of determining which classes of Petri nets can be encoded into behaviourally-equivalent CCS processes. Most of the existing related literature focuses on the inverse problem (i.e., encoding process calculi belonging to the CCS family into Petri nets), or extends CCS with Petri net-like multi-synchronisation (Multi-CCS). In this work, our main focus are free-choice and workflow nets (which are widely used in process mining to describe system interactions) and our target is plain CCS. We present several novel encodings, including one from free-choice workflow nets (produced by process mining algorithms like the Alpha-miner) into CCS processes, and we prove that our encodings produce CCS processes that are weakly bisimilar to the original net. Besides contributing new expressiveness results, our encodings open a door towards bringing analysis and verification techniques from the realm of process calculi into the realm of process mining.
Paper Information and Files
In Proceedings of COORDINATION; Groningen, The Netherlands; June 2024.
- DOI: 10.1007/978-3-031-62697-5_3
- BibTeX: see at DBLP
- Download text
General rights
Copyright and moral rights for the publications made accessible in the public website are retained by the authors and/or other copyright owners and it is a condition of accessing publications that users recognise and abide by the legal requirements associated with these rights.
- Users may download and print one copy of any publication from the website for the purpose of private study or research.
- You may not further distribute the material or use it for any profit-making activity or commercial gain.
If you believe that this document breaches copyright please contact us providing details, and we will remove access to the work immediately and investigate your claim.