Modelling Complex Software Systems
Lecture PN03 III: Properties
Artem Polyvyanyy,
Copyright By PowCoder代写 加微信 powcoder
Semester 1, 2022
Important decision problems for elementary net systems
Workflow net systems and soundness
Recap: Reachable markings
Foranetsystem= , ,= ,, ,amarkingofisareachablemarking of if = or there exists a sequence of steps (a sequential run)
⋯ ,
where∈N,=,and∈, ∈ 1...
Marking Reachable
Example seq. run
BCC ACC
” ACC→ BCC
ACC→ BCC→ ACDE→ %’
ACDDE ABCDE
BCDE→ ADDEE→ ‘
Decision problems
A decision problem is a yes-or-no question over a possibly infinite set of inputs.[1]
A decision problem is often defined using two sets: the set of possible inputs and the set of inputs for which the answer to the question is yes
A decision problem is decidable, or effectively solvable, if there is an algorithm that takes an input, terminates after a finite amount of time, and correctly answers the question posed by the problem.
The problem of deciding whether a given natural number is a prime number is an example of a decidable decision problem
Given an arbitrary computer program and an input, the problem of deciding whether the program will finish running or continue to run forever is known as the halting problem and is an example of an undecidable decision problem
Boundedness
A net system is bounded if the set of all reachable markings of is finite; otherwise, is unbounded.
In 1969, . Karp and . Miller showed that the problem of deciding whether an elementary net system is bounded is decidable[2]
In1976,RichardJ.Liptonprovedthatdecidingboundednessrequiresatleast2) space, where * > 0 is some constant and is the size of the net[3]
Is the one cookie vending machine bounded?
Bounded? Yes!
Figure: A one cookie vending machine . Figure: The marking graph of .
The set of all reachable markings of the system is finite!!
An unbounded cookies vending machine
Figure: A replenishable cookie vending machine.
Which systems should be bounded / unbounded?
Coverability graphs
Figure: The coverability graph of the replenishable cookie vending machine.
–boundedness and safeness
Anetsystem= , ,= ,, ,is–bounded,-∈N,ifforeveryplace . ∈ and for every reachable marking of it holds that the number of tokens at . in is less than or equal to -, that is, (.) ≤ -.
A –bounded system is bounded
For a bounded system there exists – ∈ N for which the system is –bounded A –bounded system is also 2-bounded, where 2 ∈ N and 2 > –
A 1-bounded system is also called safe
Figure: A 2-bounded net system.
–boundedness and safeness
Figure: A 2-bounded net system .
Figure: The marking graph of .
Reachability
Given a net system and a marking , the reachability problem consists of deciding whether is a reachable marking of .
In 1976, . Lipton said that deciding reachability requires exponential space[3] In 1981, . Mayr proved decidability of the reachability problem[4]
In 1982, S. gave a simplified proof of decidability[5]
A book is devoted to a detailed and self-contained description of the proof[6]
The reachability problem is PSPACE-complete for safe systems[7]
Many problems were shown to be recursively equivalent to the reachability problem
Marking Reachable
ACC ADD ACDDE
= , ,= ,, ,atransition∈isliveiffromevery reachable marking of it is possible to reach a marking that enables , that is, for every marking = or = such that:
⋯ ,
where∈N,and ∈, ∈ 1.. ,thereexistsasequenceofsteps 3 3 ⋯ 4 4 ,
55 where-∈N,->,5 =,and6 ∈,7∈ ..- .
A live transition can become enabled again and again (infinitely many times)
A net system is live if every its transition is live
If a system is not live, it is possible to reach a marking after which some transitions
of the system will never get enabled again
. T. Hack showed that the problem of deciding whether a given net system
is live is recursively equivalent to the reachability problem[8] Which systems should be live?
Figure: A one cookie vending machine .
Transition c will never get enabled again!
Transition d will never get enabled again!!
Important decision problems for elementary net systems
Workflow net systems and soundness
Workflow nets
A workflow net, or a WF-net, is a net structure = , , with a special source place ∈ that has the empty pre-set ( = ∅), a special sink place ; ∈ that has the empty post-set (; = ∅), and every element of is on the vertex sequence of a directed walk from to ; in the graph ∪ , .[9]
The source place is used to denote the beginning of a workflow
The sink place is used to denote the termination of a workflow
Every element of a workflow net should have a chance to be executed
Figure: General structure of a workflow net.[9]
Workflow systems
A workflow system is a net system = , , where = ,, is a workflow net and “puts” one token at the source place ∈ of and no tokens elsewhere; that is, =1and . =0,.∈,. ≠ .[9]
The token at place denotes the beginning of a single workflow, or case
Cases are processed independently
All tokens of a reachable marking describe a reachable state of the workflow system
Figure: General structure of a workflow system.[9]
Soundness: An intuition
In 1997, Wil M. P. van der Aalst, proposed the soundness property of a workflow system[9], which relates to the dynamics of the system by imposing two constraints:
Every case eventually terminates; when a case terminates there is a token at the sink place and all the other places are empty
There are no dead transitions; for every transition , there is a case that executes
Figure: A workflow system.[9]
Option to complete
An option to complete property holds for a workflow system = ,
if and only if from every reachable marking of it is possible to reach a marking that puts a token at the sink place of .
Figure: No option to complete. Figure: Marking graph.
Proper completion
A proper completion property holds for a workflow system = , , = , , , if and only if the marking with one token at the sink place ; ∈ and no tokens elsewhere is the only reachable marking of with at least one token at place ;.
Figure: No proper completion.
Figure: Marking graph.
No dead transitions
A workflow system = , , = ,, , has no dead transitions if and only if for every transition ∈ there exists a reachable marking of that enables .
Figure: Dead transition. Figure: Marking graph.
A workflow system is sound if and only if option to complete, proper completion, and no dead transitions properties hold.[9]
Figure: A workflow system.[9]
Short-circuiting
The short-circuit version of a workflow system , , where = , , , ∈isthesourceplace,and;∈isthesinkplace,isthenetsystem >, , w h e r e > = ? , ? , ? , s u c h t h a t :
? = ∪ ∗ , ∗ ∉ ?= ∪ ;,∗,∗,
Figure: Short-circuiting of a workflow system.[9]
A necessary and sufficient condition for soundness
A workflow system is sound
if and only if
the short-circuit version of is live and bounded.[9]
Figure: A sound workflow system.[9]
Many properties of net systems are formulated as decision problems (for example, reachability, boundedness, liveness, and soundness)
Many properties of net systems are recursively equivalent to the reachability problem (for example, liveness, submarking reachability, zero reachability, single- place zero reachability)
The reachability problem over elementary net systems is decidable
Model checking of net systems (that is, verification of temporal logic properties) is often undecidable and, thus, some problems must be solved by voting (for example, see results of the 10th and 11th model checking contest https://youtu.be/ANXRLrbXIX0 and https://youtu.be/6ZN8pa6a-kg)
Workflow systems are a special class of net systems for modelling business processes and workflows
In a sound workflow system, every case terminates properly, and all elements of the system can participate in some case
The soundness problem is recursively equivalent to the problem of checking boundedness and liveness
The boundedness and liveness problems over elementary net systems are decidable 25 / 26
Further Reading
1. . Soare: Recursively Enumerable Sets and Degrees – A Study of Computable Functions and Computability Generated Sets. Perspectives in mathematical logic, Springer 1987, ISBN 978-3-540- 15299-6, pp. I-XVIII, 1-437 https://link.springer.com/book/9783540666813
2. . Karp, . Miller: Parallel Program Schemata. J. Comput. Syst. Sci. 3(2): 147-195 (1969) https://doi.org/10.1016/S0022-0000(69)80011-5
3. . Lipton: The Reachability Problem Requires Exponential Space. Department of Computer Science, Research Report 63, Yale University (1976) https://cpsc.yale.edu/sites/default/files/files/tr63.pdf
4. . Mayr: Persistence of Vector Replacement Systems is Decidable. 15: 309- 318 (1981) https://doi.org/10.1007/BF00289268
5. S. : Decidability of Reachability in Vector Addition Systems (Preliminary Version). STOC 1982: 267-281 https://doi.org/10.1145/800070.802201
6. : The Mathematics of . International (1990)
7. , , : Complexity Results for 1-safe Nets. FSTTCS 1993: 326-
337 https://doi.org/10.1007/3-540-57529-4_66
8. .T. Hack: Decidability Questions for . Ph.D. Thesis, M.I.T.
http://hdl.handle.net/1721.1/27441
9. Wil M. P. van der Aalst: Verification of Workflow Nets. ICATPN 1997: 407-426 https://doi.org/10.1007/3-540-63139-9_48
10. , : Decidability Issues for – A Survey. Bull. EATCS 52: 244- 262 (1994) https://www.brics.dk/RS/94/8/BRICS-RS-94-8.pdf
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com