-
Notifications
You must be signed in to change notification settings - Fork 0
Stochastic π calculus Notes
This page summarizes what I found out about stochastic π-calculus (Sπ) and its uses for this project.
The version I use here was described by Priami in [1]. It associates a rate (parameter of an exponential distribution) with each subject, which describes the rate of the action. Rates of composite processes (sum and par) and communication are then computed from the rates of active actions in those compositions. From the transition system described in the paper, we can get the set of reachable states and from the rates compute a transition matrix, yielding a continuous time markov chain. This markov chain can then be analysed to find rates of certain states.
Note that although the word "rate" is used, the action is consumed once it happens and therefore it can only happen once. The rate is more of an inverse of the delay before the action happens. The actual delay is an exponentially distributed random variable with the rate as the distribution's parameter.
The typically non-deterministic choice (sum) is here decided by a race condition between all the active summands - the fastest action is chosen.
Directly from the description in [1], we could get the CTMC and use standard analysis tools to find rates of particular states of interest (e.g. failure states). The problem is that generating the set of reachable states and computing the relevant rates would be computationally complex and require non-trivial additions to the reasoner. For this reason, I think that this direction is not particularly useful.
The system can currently simulate the duration of atomic processes, as well as draw that duration from a distribution. Choice between summands is made by the outputs of the processes and therefore doesn't require any new intervention. What is missing is simulation of the delay resulting from transporting an item from one machine to the next. This should be done in such a way that it is distinguished from machine use, so that bottlenecks can be better identified (i.e. is one machine too slow or are the two machines too far apart).
If the rate is known during workflow composition, it could be added to the channels and then used during communication reduction to simulate the duration of communication itself (separate from the processes). However if the rates are not known during composition, for example if two machines could fulfil the first process and have different distance from the machine required for the second process, the rates would have to be decided while simulating.
It seems to me that this could be better simulated by inserting an automatically generated Move process between any two processes with non-instantaneous travel time (i.e. processes with actual machine use as opposed to decisions). This process could then get the distance to travel from the simulation environment and set its own duration appropriately. Alternatively, this could be done without a process by just the simulation engine. Then the workflow would not have to know about this delay at all.
As a side note, I also took a look at a spatial and temporal extension of π-calculus in hopes that could help simulate the movement delays. This extension however seems to be mostly aimed at constraining communication to processes that are positioned sufficiently close together at the same time, not at describing delays from distance.
All in all, I think this requires further discussion about exactly what we want to get, what we can assume is known, and how we want to do it. Sπ could be useful, but using it to its full potential would require considerable effort. If we just want to enhance PEW simulation, there are probably simpler ways to do this.
1 - C. Priami, Stochastic π-Calculus, The Computer Journal, Volume 38, Issue 7, 1995, Pages 578–589, https://doi.org/10.1093/comjnl/38.7.578