From Sound Workflow Nets to LTLf Declarative Specifications by Casting Three Spells
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912910763098112 |
|---|---|
| author | Barbaro, Luca Varricchione, Giovanni Montali, Marco Di Ciccio, Claudio |
| author_facet | Barbaro, Luca Varricchione, Giovanni Montali, Marco Di Ciccio, Claudio |
| contents | In process management, effective behavior modeling is essential for understanding execution dynamics and identifying potential issues. Two complementary paradigms have emerged in the pursuit of this objective: the imperative approach, representing all allowed runs of a system in a graph-based model, and the declarative one, specifying the rules that a run must not violate in a constraint-based specification. Extensive studies have been conducted on the synergy and comparisons of the two paradigms. To date, though, whether a declarative specification could be systematically derived from an imperative model such that the original behavior was fully preserved (and if so, how) remained an unanswered question. In this paper, we propose a three-fold contribution. (1) We introduce a systematic approach to synthesize declarative process specifications from safe and sound Workflow nets. (2) We prove behavioral equivalence of the input net with the output specification, alongside related guarantees. (3) We experimentally demonstrate the scalability and compactness of our encoding through tests conducted with synthetic and real-world testbeds. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_05114 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | From Sound Workflow Nets to LTLf Declarative Specifications by Casting Three Spells Barbaro, Luca Varricchione, Giovanni Montali, Marco Di Ciccio, Claudio Logic in Computer Science Formal Languages and Automata Theory In process management, effective behavior modeling is essential for understanding execution dynamics and identifying potential issues. Two complementary paradigms have emerged in the pursuit of this objective: the imperative approach, representing all allowed runs of a system in a graph-based model, and the declarative one, specifying the rules that a run must not violate in a constraint-based specification. Extensive studies have been conducted on the synergy and comparisons of the two paradigms. To date, though, whether a declarative specification could be systematically derived from an imperative model such that the original behavior was fully preserved (and if so, how) remained an unanswered question. In this paper, we propose a three-fold contribution. (1) We introduce a systematic approach to synthesize declarative process specifications from safe and sound Workflow nets. (2) We prove behavioral equivalence of the input net with the output specification, alongside related guarantees. (3) We experimentally demonstrate the scalability and compactness of our encoding through tests conducted with synthetic and real-world testbeds. |
| title | From Sound Workflow Nets to LTLf Declarative Specifications by Casting Three Spells |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.05114 |