From Sound Workflow Nets to LTLf Declarative Specifications
LucaBarbaro3
0 views
60 slides
Oct 13, 2025
Slide 1 of 60
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
About This Presentation
This presentation (helded in BPM 2025 Sevilla) explores our method for translating imperative process models into declarative specifications grounded in Linear Temporal Logic over finite traces (LTLf)
Slide Content
Luca Barbaro, Giovanni Varricchione, Marco Montali, Claudio Di Ciccio
From Sound Workflow Nets to LTLfDeclarative Specifications by Casting Three
Spells
13-10-2025
From Sound Workflow Nets to LTLfDeclarative Specifications by Casting Three
Spells
13-10-2025
ImperativeDeclarative
213-10-2025
•WorkflowNet•BPMN
Specifies all possible routes
Explicit but not flexible structure
Model all paths
213-10-2025
•WorkflowNet•BPMN
Specifies all possible routes
Explicit but not flexible structure
Model all paths
313-10-2025
•WorkflowNet•BPMN •DECLARE•DCR
Specifies all possible routes
Explicit but not flexible structureImplicit sequences, allows variability
Specifies rules that must hold
Model only the logicModel all paths
• If a happens, b must follow eventually
• a occurs at most once
• c can only happen if a occurred earlier
ImperativeDeclarative
•WorkflowNet•BPMN •DECLARE•DCR
Specifies all possible routes
Explicit but not flexible structureImplicit sequences, allows variability
Specifies rules that must hold
Model only the logicModel all paths
• If a happens, b must follow eventually
• a occurs at most once
• c can only happen if a occurred earlier
ImperativeDeclarative
413-10-2025
•WorkflowNet•BPMN •DECLARE•DCR
No representation would be always superior —both suit different comprehension
tasks.2
2Pichler, P., Weber, B., Zugal, S., et al.: Imperative versus declarative process modeling languages: An
empirical investigation. In: BPM Workshops 2011. vol. 99, pp. 383–394 (2011)
Specifies all possible routes
Explicit but not flexible structureImplicit sequences, allows variability
Specifies rules that must hold
Model only the logicModel all paths
• If a happens, b must follow eventually
• a occurs at most once
• c can only happen if a occurred earlier
ImperativeDeclarative
•WorkflowNet•BPMN •DECLARE•DCR
No representation would be always superior —both suit different comprehension
tasks.2
2Pichler, P., Weber, B., Zugal, S., et al.: Imperative versus declarative process modeling languages: An
empirical investigation. In: BPM Workshops 2011. vol. 99, pp. 383–394 (2011)
Specifies all possible routes
Explicit but not flexible structureImplicit sequences, allows variability
Specifies rules that must hold
Model only the logicModel all paths
• If a happens, b must follow eventually
• a occurs at most once
• c can only happen if a occurred earlier
ImperativeDeclarative
Translating Workflow Net into Declarative
Specifications
513-10-2025
3Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative
models.In: SIMPDA 2014. vol. 1293, pp. 162–173 (2014)
bcaDeclarative
Specification
Imperative
Model
Specifications
513-10-2025
3Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative
models.In: SIMPDA 2014. vol. 1293, pp. 162–173 (2014)
bcaDeclarative
Specification
Imperative
Model
Translating Workflow Net into Declarative
Specifications
613-10-2025
3Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative
models.In: SIMPDA 2014. vol. 1293, pp. 162–173 (2014)
bcaDeclarative
Specification
Imperative
Model
Specifications
613-10-2025
3Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative
models.In: SIMPDA 2014. vol. 1293, pp. 162–173 (2014)
bcaDeclarative
Specification
Imperative
Model
Key Problem
713-10-2025
•Can a declarative specification be synthesized from a
Workflow Net preserving the original behavior?
713-10-2025
•Can a declarative specification be synthesized from a
Workflow Net preserving the original behavior?
Key Problem
813-10-2025
•Can a declarative specification be synthesized from a
Workflow Net preserving the original behavior?
•Conversion established for ease conformance checking
procedures resortingon re-discovery over simulations,
state space exploration, or behavioral comparison.
813-10-2025
•Can a declarative specification be synthesized from a
Workflow Net preserving the original behavior?
•Conversion established for ease conformance checking
procedures resortingon re-discovery over simulations,
state space exploration, or behavioral comparison.
Contribution
913-10-2025
•We provide a direct and transformationfrom any safe and
sound Workflow Net to a compact DECLARE specification
with only three templates, preserving the exact behavior.
913-10-2025
•We provide a direct and transformationfrom any safe and
sound Workflow Net to a compact DECLARE specification
with only three templates, preserving the exact behavior.
Contribution
1013-10-2025
•We provide a direct and transformationfrom any safe and
sound Workflow Net to a compact DECLARE specification
with only three templates, preserving the exact behavior.
•We prove behavioral equivalence of the input net with the
output specification.
1013-10-2025
•We provide a direct and transformationfrom any safe and
sound Workflow Net to a compact DECLARE specification
with only three templates, preserving the exact behavior.
•We prove behavioral equivalence of the input net with the
output specification.
Contribution
1113-10-2025
•We provide a direct and transformationfrom any safe and
sound Workflow Net to a compact DECLARE specification
with only three templates, preserving the exact behavior.
•We prove behavioral equivalence of the input net with the
output specification.
•We experimentally demonstrate the scalabilityand
compactnessof our encoding through tests conducted
with synthetic and real-world testbeds.
1113-10-2025
•We provide a direct and transformationfrom any safe and
sound Workflow Net to a compact DECLARE specification
with only three templates, preserving the exact behavior.
•We prove behavioral equivalence of the input net with the
output specification.
•We experimentally demonstrate the scalabilityand
compactnessof our encoding through tests conducted
with synthetic and real-world testbeds.
1213-10-2025
a
p0ta
b
tb
p1
p2
c
d
e
f
g
u
w
v
p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
•Preset p
•Postsetp
P(the finite set of “places”)
T(the finite set of “transitions”) constitute the nodes (P ∩T = ∅),
F⊆(P ×T ⊎T ×P ) flow relation defines the edges.
Safe & Sound Workflow
Net
a
p0ta
b
tb
p1
p2
c
d
e
f
g
u
w
v
p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
•Preset p
•Postsetp
P(the finite set of “places”)
T(the finite set of “transitions”) constitute the nodes (P ∩T = ∅),
F⊆(P ×T ⊎T ×P ) flow relation defines the edges.
Safe & Sound Workflow
Net
1313-10-2025
a
p0ta
b
tb
p1
p2
c
d
e
f
g
u
w
v
p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Focus directly on the transitions not on the labels!
•Preset p
•Postsetp
P(the finite set of “places”)
T(the finite set of “transitions”) constitute the nodes (P ∩T = ∅),
F⊆(P ×T ⊎T ×P ) flow relation defines the edges.
Safe & Sound Workflow
Net
a
p0ta
b
tb
p1
p2
c
d
e
f
g
u
w
v
p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Focus directly on the transitions not on the labels!
•Preset p
•Postsetp
P(the finite set of “places”)
T(the finite set of “transitions”) constitute the nodes (P ∩T = ∅),
F⊆(P ×T ⊎T ×P ) flow relation defines the edges.
Safe & Sound Workflow
Net
1413-10-2025
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Safe & Sound Workflow
Net
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Safe & Sound Workflow
Net
1513-10-2025
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Run: valid sequence of transitions from
the initial state to some final state
Safe & Sound Workflow
Net
{ta,...,tg,tu,tv,tw}
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Run: valid sequence of transitions from
the initial state to some final state
Safe & Sound Workflow
Net
{ta,...,tg,tu,tv,tw}
1613-10-2025
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Safe & Sound Workflow
Net
Run: valid sequence of transitions from
the initial state to some final state{ta,...,tg,tu,tv,tw}
Trace:projection of the run on
labels of visible transitions
{a,...,g,u,v,w}
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Safe & Sound Workflow
Net
Run: valid sequence of transitions from
the initial state to some final state{ta,...,tg,tu,tv,tw}
Trace:projection of the run on
labels of visible transitions
{a,...,g,u,v,w}
1713-10-2025
•Soundness, Safety and State Space
Safeness
•1-bounded are safe (one place with at most one
token)
Soundness:
•Option to complete
•Proper completion
•No dead transitions
Safe and sound Workflow net are a superclass of sound S-coverable net,
which contains safe and sound free-choice and well-structured nets
Safe & Sound Workflow
Net
•Soundness, Safety and State Space
Safeness
•1-bounded are safe (one place with at most one
token)
Soundness:
•Option to complete
•Proper completion
•No dead transitions
Safe and sound Workflow net are a superclass of sound S-coverable net,
which contains safe and sound free-choice and well-structured nets
Safe & Sound Workflow
Net
1813-10-2025
LTLf-based declarative specifications
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”1.Alt.Prec.(y, x)
LTLf-based declarative specifications
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”1.Alt.Prec.(y, x)
1913-10-2025
LTLf-based declarative specifications
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”
2.”yoccurs at most once”
1.Alt.Prec.(y, x)
2.AtMostOne(y)
LTLf-based declarative specifications
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”
2.”yoccurs at most once”
1.Alt.Prec.(y, x)
2.AtMostOne(y)
2013-10-2025
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”
2.”yoccurs at most once”
3.”xis the last to occur”
1.Alt.Prec.(y, x)
2.AtMostOne(y)
3.End(x)
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
LTLf-based declarative specifications
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”
2.”yoccurs at most once”
3.”xis the last to occur”
1.Alt.Prec.(y, x)
2.AtMostOne(y)
3.End(x)
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
LTLf-based declarative specifications
2113-10-2025
A Declarative specification is a conjunction of such constraints, defining
a set of valid finite traces.
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”
2.”yoccurs at most once”
3.”xis the last to occur”
1.Alt.Prec.(y, x)
2.AtMostOne(y)
3.End(x)
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
LTLf-based declarative specifications
A Declarative specification is a conjunction of such constraints, defining
a set of valid finite traces.
Eachtemplate correspondsto an LTLfformula
1.“Whenever xoccurs, ymust have occurred before, with no xin between”
2.”yoccurs at most once”
3.”xis the last to occur”
1.Alt.Prec.(y, x)
2.AtMostOne(y)
3.End(x)
Declarative constraints are logic-based rules over finite traces. Each template defines a temporal
relationbetween activities.
LTLf-based declarative specifications
2213-10-2025
•LTLf -based declarative
specificationsDS= (Rep, Σ, K)
•Rep: repertoireof templates
•Σ: alphabetof symbols
•K: set of constraintswith mappingsκ
LTLf -based declarative specifications
•LTLf -based declarative
specificationsDS= (Rep, Σ, K)
•Rep: repertoireof templates
•Σ: alphabetof symbols
•K: set of constraintswith mappingsκ
LTLf -based declarative specifications
2313-10-2025
BranchedDECLARE extends standard Declare by allowing disjunctions over symbols from the alphabet Σ.
Alt.Prec.({a, w}, b) -"Beforeeveryb, eitheraor wmust havehappened—and no b in between"
Every LTLf formula can be translated into an FSA that accepts exactly
the traces satisfying the formula
DS= (Rep, Σ, K)
•Rep: repertoireof templates
•Σ: alphabetof symbols
•K: set of constraintswith mappingsκ
LTLf -based declarative specifications
BranchedDECLARE extends standard Declare by allowing disjunctions over symbols from the alphabet Σ.
Alt.Prec.({a, w}, b) -"Beforeeveryb, eitheraor wmust havehappened—and no b in between"
Every LTLf formula can be translated into an FSA that accepts exactly
the traces satisfying the formula
DS= (Rep, Σ, K)
•Rep: repertoireof templates
•Σ: alphabetof symbols
•K: set of constraintswith mappingsκ
LTLf -based declarative specifications
2413-10-2025
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Wizard’s guide
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
Wizard’s guide
•Synthesis of LTLfDECLARE specification from Workflow
Nets
2513-10-2025
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
InitializesDeclare Specification by
assigning its alphabet with the
transition set of the Workflow Net.
Wizard’s guide
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
InitializesDeclare Specification by
assigning its alphabet with the
transition set of the Workflow Net.
Wizard’s guide
•Synthesis of LTLfDECLARE specification from Workflow
Nets
Wizard’s guide
2613-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
InitializesDeclare Specification by
assigning its alphabet with the
transition set of the Workflow Net.
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Σ gets{ta,...,tg,tu,tv,tw}
2613-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
InitializesDeclare Specification by
assigning its alphabet with the
transition set of the Workflow Net.
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Σ gets{ta,...,tg,tu,tv,tw}
Wizard’s guide
2713-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
Sets the three necessary templates
that will be used: AtMostOne(x),
End(x), and Alt.Prec.(y,x)
2713-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
Sets the three necessary templates
that will be used: AtMostOne(x),
End(x), and Alt.Prec.(y,x)
Wizard’s guide
2813-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
A cycle begins to visit all places in
WN and update DS by including a
new constraint per place. Let the
magic happens!
Cast the first
Spell!
2813-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
A cycle begins to visit all places in
WN and update DS by including a
new constraint per place. Let the
magic happens!
Cast the first
Spell!
Wizard’s guide
2913-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Every time a transition in the postsetof p fires, it is necessary that at least one of the
transitions in the preset of p fired before and that no transition in the postsetof p has
fired since then.
2913-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Every time a transition in the postsetof p fires, it is necessary that at least one of the
transitions in the preset of p fired before and that no transition in the postsetof p has
fired since then.
Wizard’s guide
3013-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
3013-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
Wizard’s guide
3113-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb)
3113-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb)
Wizard’s guide
3213-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb) {ta,...,tu, tw, tb, …}
3213-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb) {ta,...,tu, tw, tb, …}
Wizard’s guide
3313-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb) {ta,...,tu, tv}
3313-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb) {ta,...,tu, tv}
Wizard’s guide
3413-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb)EXCLUSIVE CHIOCE!
3413-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•From p8wederive Alt.Prec.(tu,{tv,tw})
•Placep1leads to Alt.Prec.({ta,tw},tb)EXCLUSIVE CHIOCE!
Wizard’s guide
3513-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
A cycle begins to visit all places in
WN and update DS by including a
new constraint per place. Let the
magic happens!
Cast the second
Spell!
3513-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
A cycle begins to visit all places in
WN and update DS by including a
new constraint per place. Let the
magic happens!
Cast the second
Spell!
Wizard’s guide
3613-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Any of the transitions in the postsetof will start the run and will not repeat
afterwards (because no firing can assign with a token again by definition)
3613-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Any of the transitions in the postsetof will start the run and will not repeat
afterwards (because no firing can assign with a token again by definition)
Wizard’s guide
3713-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•tacan occur only once (AtMostOne(ta))
3713-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•tacan occur only once (AtMostOne(ta))
Wizard’s guide
3913-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
A cycle begins to visit all places in
WN and update DS by including a
new constraint per place. Let the
magic happens!
...and last but
not least. My
work is done!
3913-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
A cycle begins to visit all places in
WN and update DS by including a
new constraint per place. Let the
magic happens!
...and last but
not least. My
work is done!
Wizard’s guide
4013-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Every run must terminate with one of the transitions in the preset of ■
4013-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Every run must terminate with one of the transitions in the preset of ■
Wizard’s guide
4113-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•tvis the last event of the trace (End(tv))
4113-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
•tvis the last event of the trace (End(tv))
4213-10-2025
AtMostOne(ta)
End(tv)
Alt.Prec.({ta, tw}, tb)
Alt.Prec.(tb, {td, tc})
Alt.Prec.({td, tc}, te)
Alt.Prec.(te, tf)
Alt.Prec.(te, tg)
Alt.Prec.(tf, tu)
Alt.Prec.(tg, tu)
Alt.Prec.(tu, {tv, tw})
DECLARE specification generated from the Workflow net:
Declarative Specification
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Wizard’s guide
Workflow Net
AtMostOne(ta)
End(tv)
Alt.Prec.({ta, tw}, tb)
Alt.Prec.(tb, {td, tc})
Alt.Prec.({td, tc}, te)
Alt.Prec.(te, tf)
Alt.Prec.(te, tg)
Alt.Prec.(tf, tu)
Alt.Prec.(tg, tu)
Alt.Prec.(tu, {tv, tw})
DECLARE specification generated from the Workflow net:
Declarative Specification
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
tc tf
Wizard’s guide
Workflow Net
Wizard’s guide
4313-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
The mapping of the transitions of WN to labels can be treated as a post-hoc refinement
of the Workflow net and equivalently of declarative specification
a
p0ta
b
tb
p1
p2
c
d
e
f
g
u
w
v
p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
4313-10-2025
•Synthesis of LTLfDECLARE specification from Workflow
Nets
The mapping of the transitions of WN to labels can be treated as a post-hoc refinement
of the Workflow net and equivalently of declarative specification
a
p0ta
b
tb
p1
p2
c
d
e
f
g
u
w
v
p9p3
p4
p5p7
p6
p8
td
te
tg
tutv
tw
Theorem
4413-10-2025
Given a safe and sound Workflow net WN , our algorithm returns a Declare
specification DS such that: (i) any run of WN satisfies DS, and (ii) any trace
satisfying DS is a run of WN.
Theorem.
4413-10-2025
Given a safe and sound Workflow net WN , our algorithm returns a Declare
specification DS such that: (i) any run of WN satisfies DS, and (ii) any trace
satisfying DS is a run of WN.
Theorem.
Proof Key Ideas
4513-10-2025
Let σ be a run of WN . We show that σ |= φDS
•Correct completion: End constraint ensures correct completion (last transition fires
from output place)
•Forbidre-entrance: AtMostOneforbids re-entrance into the net
•Causaldependences: Alt.Prec.(p, p) preservescausaldependencies
4513-10-2025
Let σ be a run of WN . We show that σ |= φDS
•Correct completion: End constraint ensures correct completion (last transition fires
from output place)
•Forbidre-entrance: AtMostOneforbids re-entrance into the net
•Causaldependences: Alt.Prec.(p, p) preservescausaldependencies
Reachability FSA
4613-10-2025
tatb
tc
tdte
tf
tgtutv
tw
s0
[p0]
s1
[p1]
s2
[p2]
s3
[p3]
s4
[p4]tf
tg
s5
[p5]
s6
[p6]
s7
[p7]
s8
[p8]
s9
[p9]
•The state space of k-bounded Petri nets can be represented in the form of a deterministic labeled
transition system (LTS) that go under the name of reachability graph.
•The reachability graph of a safe and sound Workflow net behaves like a finite state automaton:
each markingis a state, and each transition firingis a labeled move between states.
4613-10-2025
tatb
tc
tdte
tf
tgtutv
tw
s0
[p0]
s1
[p1]
s2
[p2]
s3
[p3]
s4
[p4]tf
tg
s5
[p5]
s6
[p6]
s7
[p7]
s8
[p8]
s9
[p9]
•The state space of k-bounded Petri nets can be represented in the form of a deterministic labeled
transition system (LTS) that go under the name of reachability graph.
•The reachability graph of a safe and sound Workflow net behaves like a finite state automaton:
each markingis a state, and each transition firingis a labeled move between states.
4713-10-2025
A safe and sound Workflow net WN is bisimilarto a declarative
specification DS if and only if the reachability FSA of WN is
bisimilarto the specification FSA of DS
Behavioral Equivalence
•Bisimilarity
A safe and sound Workflow net WN is bisimilarto a declarative
specification DS if and only if the reachability FSA of WN is
bisimilarto the specification FSA of DS
Behavioral Equivalence
•Bisimilarity
4813-10-2025
A safe and sound Workflow net WN is bisimilarto a declarative
specification DS if and only if the reachability FSA of WN is
bisimilarto the specification FSA of DS
Behavioral Equivalence
•Bisimilarity
The two automatahave to accept the same language.
A safe and sound Workflow net WN is bisimilarto a declarative
specification DS if and only if the reachability FSA of WN is
bisimilarto the specification FSA of DS
Behavioral Equivalence
•Bisimilarity
The two automatahave to accept the same language.
4913-10-2025
A safe and sound Workflow net WN is bisimilarto a declarative
specification DS if and only if the reachability FSA of WN is
bisimilarto the specification FSA of DS
Behavioral Equivalence
•Bisimilarity
The two automatahave to accept the same language.
The declarative specification returned by the algorithm accepts all and only the
runs of the input safe and sound Workflow net
A safe and sound Workflow net WN is bisimilarto a declarative
specification DS if and only if the reachability FSA of WN is
bisimilarto the specification FSA of DS
Behavioral Equivalence
•Bisimilarity
The two automatahave to accept the same language.
The declarative specification returned by the algorithm accepts all and only the
runs of the input safe and sound Workflow net
Evaluation
5013-10-2025
•Bisimulation
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
tatb
tc
tdte
tf
tgtutv
tw
s0
[p0]
s1
[p1]
s2
[p2]
s3
[p3]
s4
[p4]tf
tg
s5
[p5]
s6
[p6]
s7
[p7]
s8
[p8]
s9
[p9]
Workflow Net
Reachability
FSA
5013-10-2025
•Bisimulation
p0tatb
p1
p2 p9p3
p4
p5p7
p6
p8
tc
td
te
tf
tg
tutv
tw
tatb
tc
tdte
tf
tgtutv
tw
s0
[p0]
s1
[p1]
s2
[p2]
s3
[p3]
s4
[p4]tf
tg
s5
[p5]
s6
[p6]
s7
[p7]
s8
[p8]
s9
[p9]
Workflow Net
Reachability
FSA
Evaluation
5113-10-2025
•Bisimulation
tatbtc
tdte
tf
tgtu
tw
s0s1s2s3s4tf
tg
s5
s6
s7s8s9
AtMostOne(ta)
End(tv)
Alt.Prec.({ta, tw}, tb)
Alt.Prec.(tb, {td, tc})
Alt.Prec.({td, tc}, te)
Alt.Prec.(te, tf)
Alt.Prec.(te, tg)
Alt.Prec.(tf, tu)
Alt.Prec.(tg, tu)
Alt.Prec.(tu, {tv, tw})
tv
DECLARE specification generated from the Workflow net:
Declarative Specification
Specification FSA
5113-10-2025
•Bisimulation
tatbtc
tdte
tf
tgtu
tw
s0s1s2s3s4tf
tg
s5
s6
s7s8s9
AtMostOne(ta)
End(tv)
Alt.Prec.({ta, tw}, tb)
Alt.Prec.(tb, {td, tc})
Alt.Prec.({td, tc}, te)
Alt.Prec.(te, tf)
Alt.Prec.(te, tg)
Alt.Prec.(tf, tu)
Alt.Prec.(tg, tu)
Alt.Prec.(tu, {tv, tw})
tv
DECLARE specification generated from the Workflow net:
Declarative Specification
Specification FSA
Evaluation
5213-10-2025
•Bisimulation
tatbtc
tdte
tf
tgtu
tw
s0s1s2s3s4tf
tg
s5
s6
s7s8s9tv
tatb
tc
tdte
tf
tgtutv
tw
s0
[p0]
s1
[p1]
s2
[p2]
s3
[p3]
s4
[p4]tf
tg
s5
[p5]
s6
[p6]
s7
[p7]
s8
[p8]
s9
[p9]
Reachability
FSA
Specification FSA
5213-10-2025
•Bisimulation
tatbtc
tdte
tf
tgtu
tw
s0s1s2s3s4tf
tg
s5
s6
s7s8s9tv
tatb
tc
tdte
tf
tgtutv
tw
s0
[p0]
s1
[p1]
s2
[p2]
s3
[p3]
s4
[p4]tf
tg
s5
[p5]
s6
[p6]
s7
[p7]
s8
[p8]
s9
[p9]
Reachability
FSA
Specification FSA
Evaluation
5313-10-2025
•ConstraintCardinality
•Space complexitygrows linearly with the size of
the flow relation. O(|F|)
•Time complexityis bounded byO(|P| ×|T|)
5313-10-2025
•ConstraintCardinality
•Space complexitygrows linearly with the size of
the flow relation. O(|F|)
•Time complexityis bounded byO(|P| ×|T|)
Evaluation
5413-10-2025
•Formula Size
•Space complexitygrows linearly with the size of
the flow relation. O(|F|)
•Time complexityis bounded byO(|P| ×|T|)
5413-10-2025
•Formula Size
•Space complexitygrows linearly with the size of
the flow relation. O(|F|)
•Time complexityis bounded byO(|P| ×|T|)
5513-10-2025
•Real-world process model testingEvaluation
Process ModelTransitionsPlacesNodes Mem.usage [MB] Exec.time [ms]
BPIC 12 78 54 174 19,97 5,11
BPIC 13_cp 19 54 44 19,76 1,7
BPIC 13_inc 23 17 50 19,89 2,03
BPIC 14_f 46 35 102 19,9 3,31
BPIC 15_1f 135 89 286 20,44 8,39
BPIC 15_2f 200 123 422 20,91 12,3
BPIC 15_3f 178 122 396 20,77 11,49
BPIC 15_4f 168 115 368 20,55 11,38
BPIC 15_5f 150 99 320 20,43 9,16
BPIC 17 87 55 184 19,91 5,67
RTFMP 34 29 82 19,81 3,47
Sepsis 50 39 116 19,75 3,65
•Real-world process model testingEvaluation
Process ModelTransitionsPlacesNodes Mem.usage [MB] Exec.time [ms]
BPIC 12 78 54 174 19,97 5,11
BPIC 13_cp 19 54 44 19,76 1,7
BPIC 13_inc 23 17 50 19,89 2,03
BPIC 14_f 46 35 102 19,9 3,31
BPIC 15_1f 135 89 286 20,44 8,39
BPIC 15_2f 200 123 422 20,91 12,3
BPIC 15_3f 178 122 396 20,77 11,49
BPIC 15_4f 168 115 368 20,55 11,38
BPIC 15_5f 150 99 320 20,43 9,16
BPIC 17 87 55 184 19,91 5,67
RTFMP 34 29 82 19,81 3,47
Sepsis 50 39 116 19,75 3,65
Process Diagnostics
5613-10-2025
•A downstream task: Using synthesized constraints
as determinants for process diagnostics
5613-10-2025
•A downstream task: Using synthesized constraints
as determinants for process diagnostics
Process Diagnostics
5713-10-2025
•A downstream task: Using synthesized constraints
as determinants for process diagnostics
ID 36:
Alt.Prec.({t01_HOOFD_490_1,t13_CRD_010},t01_HOOFD_490_1a)
when “Set Decision Status”(t01 HOOFD 490 1a) occurs, it
should be preceded by either “Create Environmental Permit
Decision” (t01 HOOFD 490 1) or “Coordination of
Application” (t13 CRD 010).
Violatingtraces:
(11369696, 9613229, 12135936),
Alternative execution:
“NoPermitNeeded or Only Notification Needed”
(t14_VRIJ_010)
5713-10-2025
•A downstream task: Using synthesized constraints
as determinants for process diagnostics
ID 36:
Alt.Prec.({t01_HOOFD_490_1,t13_CRD_010},t01_HOOFD_490_1a)
when “Set Decision Status”(t01 HOOFD 490 1a) occurs, it
should be preceded by either “Create Environmental Permit
Decision” (t01 HOOFD 490 1) or “Coordination of
Application” (t13 CRD 010).
Violatingtraces:
(11369696, 9613229, 12135936),
Alternative execution:
“NoPermitNeeded or Only Notification Needed”
(t14_VRIJ_010)
Process Diagnostics
5813-10-2025
•A downstream task: Using synthesized constraints
as determinants for process diagnostics
ID 58:
Constraints in the group have in common the presence
of tENDin the activator’s set.
The BPIC 15 log allows a multitude of possible
conclusions. The α-algorithm, though, disregards the
occurrence frequency of individual transitions during
model construction, resulting in a non-selective
inclusion of all events.
This affects the fitnessof those constraints.
5813-10-2025
•A downstream task: Using synthesized constraints
as determinants for process diagnostics
ID 58:
Constraints in the group have in common the presence
of tENDin the activator’s set.
The BPIC 15 log allows a multitude of possible
conclusions. The α-algorithm, though, disregards the
occurrence frequency of individual transitions during
model construction, resulting in a non-selective
inclusion of all events.
This affects the fitnessof those constraints.
Conclusion&Future Work
5913-10-2025
•Introduced a systematic translation from safe and sound Workflow nets
to bisimilarDeclare specifications
•Used only three LTLf templates
•Developed a proof-of-concept implementation
•Demonstrated scalabilityand tested on synthetic and real-world models
5913-10-2025
•Introduced a systematic translation from safe and sound Workflow nets
to bisimilarDeclare specifications
•Used only three LTLf templates
•Developed a proof-of-concept implementation
•Demonstrated scalabilityand tested on synthetic and real-world models
Conclusion&Future Work
6013-10-2025
•Introduced a systematic translation from safe and sound Workflow nets
to bisimilarDeclare specifications
•Used only three LTLf templates
•Developed a proof-of-concept implementation
•Demonstrated scalabilityand tested on synthetic and real-world models
•Extend to broader classes of imperative models
•Broaden the application of our solution to detect behavioral violations
•Investigate linksbetween specification inconsistency and unsound/safe nets
•Apply the transformation to enable hybrid models combining imperative and declarative
approaches
6013-10-2025
•Introduced a systematic translation from safe and sound Workflow nets
to bisimilarDeclare specifications
•Used only three LTLf templates
•Developed a proof-of-concept implementation
•Demonstrated scalabilityand tested on synthetic and real-world models
•Extend to broader classes of imperative models
•Broaden the application of our solution to detect behavioral violations
•Investigate linksbetween specification inconsistency and unsound/safe nets
•Apply the transformation to enable hybrid models combining imperative and declarative
approaches
6113-10-2025
https://github.com/l2brb/Sp3llsWizard
Luca Barbaro, Giovanni Varricchione, Marco Montali, Claudio Di Ciccio
From Sound
Workflow Nets to
LTLfDeclarative
Specifications by
Casting Three Spells
https://github.com/l2brb/Sp3llsWizard
Luca Barbaro, Giovanni Varricchione, Marco Montali, Claudio Di Ciccio
From Sound
Workflow Nets to
LTLfDeclarative
Specifications by
Casting Three Spells
Tags
Categories
TechnologyDownload
Download Slideshow Get the original presentation fileQuick Actions
Statistics
- Views 0
- Slides 60
- Age 49 days
Related Slideshows
11
8-top-ai-courses-for-customer-support-representatives-in-2025.pptx
JeroenErne2
44 views
10
7-essential-ai-courses-for-call-center-supervisors-in-2025.pptx
JeroenErne2
45 views
13
25-essential-ai-courses-for-user-support-specialists-in-2025.pptx
JeroenErne2
36 views
11
8-essential-ai-courses-for-insurance-customer-service-representatives-in-2025.pptx
JeroenErne2
33 views
21
Know for Certain
DaveSinNM
19 views
17
PPT OPD LES 3ertt4t4tqqqe23e3e3rq2qq232.pptx
novasedanayoga46
23 views