Rate Lifting for Stochastic Process Algebra by Transition Context Augmentation
提出一种算法，在给定组合平坦模型速率时，确定随机过程代数模型中顺序过程的未知速率，通过求解非线性方程组并调整同步结构实现速率提升，用于模型逆向工程和修复。
This article presents an algorithm for determining the unknown rates in the sequential processes of a Stochastic Process Algebra (SPA) model, provided that the rates in the combined flat model are given. Such a rate lifting is useful for model reverse engineering and model repair. Technically, the algorithm works by solving systems of nonlinear equations and—if necessary—adjusting the model’s synchronisation structure, without changing its transition system. The adjustments cause an augmentation of a transition’s context and thus enable additional control over the transition rate. The complete pseudo-code of the rate lifting algorithm is included and discussed in the article, and its practical usefulness is demonstrated by two case studies. The approach taken by the algorithm exploits some structural and behavioural properties of SPA systems, which are formulated here for the first time and could be very beneficial also in other contexts, such as compositional system verification.