Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userComputing the Expected Execution Time of Probabilistic Workflow Nets
60
0
0.0
(
0
)
Added by
Philipp J. Meyer
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWNs), and give them a Markov Decision Process (MDP) semantics. Since the time needed to execute two parallel tasks is the maximum of the times, and not their sum, the expected time cannot be directly computed using the theory of MDPs with rewards. In our first contribution, we overcome this obstacle with the help of earliest-first schedulers, and give a single exponential-time algorithm for computing the expected time. In our second contribution, we show that computing the expected time is #P-hard, and so polynomial algorithms are very unlikely to exist. Further, #P-hardness holds even for workflows with a very simple structure in which all transitions times are 1 or 0, and all probabilities are 1 or 0.5. Our third and final contribution is an experimental investigation of the runtime of our algorithm on a set of industrial benchmarks. Despite the negative theoretical results, the results are very encouraging. In particular, the expected time of every workflow in a popular benchmark suite with 642 workflow nets can be computed in milliseconds.
rate research
Read More
Workflow graphs extend classical flow charts with concurrent fork and join nodes. They constitute the core of business processing languages such as BPMN or UML Activity Diagrams. The activities of a workflow graph are executed by humans or machines, generically called resources. If concurrent activities cannot be executed in parallel by lack of resources, the time needed to execute the workflow increases. We study the problem of computing the minimal number of resources necessary to fully exploit the concurrency of a given workflow, and execute it as fast as possible (i.e., as fast as with unlimited resources). We model this problem using free-choice Petri nets, which are known to be equivalent to workflow graphs. We analyze the computational complexity of tw
The paper addresses the problem of computing maximal expected time to termination of probabilistic timed automata (PTA) models, under the condition that the system will, eventually, terminate. This problem can exhibit high computational complexity, in particular when the automaton under analysis contains cycles that may be repeated very often (due to very high probabilities, e.g. p =0.999). Such cycles can degrade the performance of typical model checking algorithms, as the likelihood of repeating the cycle converges to zero arbitrarily slowly. We introduce an acceleration technique that can be applied to improve the execution of such cycles by collapsing their iterations. The acceleration process of a cyclic PTA consists of several formal steps necessary to handle the cumulative timing and probability information that result from successive executions of a cycle. The advantages of acceleration are twofold. First, it helps to reduce the computational complexity of the problem without adversely affecting the outcome of the analysis. Second, it can bring the worst case execution time problem of PTAs within the bounds of feasibility for model checking techniques. To our knowledge, this is the first work that addresses the problem of accelerating execution of cycles that exhibit both timing and probabilistic behavior.
We present a novel modular approach to infer upper bounds on the expected runtime of probabilistic integer programs automatically. To this end, it computes bounds on the runtime of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool KoAT.
We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with $n$ vertices and $m$ edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires $O(n^2)$ symbolic operations and $O(1)$ symbolic space. The only other symbolic algorithm for the MEC decomposition requires $O(n sqrt{m})$ symbolic operations and $O(sqrt{m})$ symbolic space. A main open question is whether the worst-case $O(n^2)$ bound for symbolic operations can be beaten. We present a symbolic algorithm that requires $widetilde{O}(n^{1.5})$ symbolic operations and $widetilde{O}(sqrt{n})$ symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all $0<epsilon leq 1/2$ the symbolic algorithm requires $widetilde{O}(n^{2-epsilon})$ symbolic operations and $widetilde{O}(n^{epsilon})$ symbolic space ($widetilde{O}$ hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of $omega$-regular objectives for MDPs. We consider the canonical parity objectives for $omega$-regular objectives, and for parity objectives with $d$-priorities we present an algorithm that computes the almost-sure winning region with $widetilde{O}(n^{2-epsilon})$ symbolic operations and $widetilde{O}(n^{epsilon})$ symbolic space, for all $0 < epsilon leq 1/2$.
We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an events occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the models dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
