Rate Lifting for Stochastic Process Algebra by Transition Context Augmentation
Article No.: 20, Pages 1 - 30
Abstract
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.
References
[1]
C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29, 6 (2003), 524–541. DOI:
[2]
E. Bartocci, R. Grosu, P. Katsaros, C. R. Ramakrishnan, and S.A. Smolka. 2011. Model repair for probabilistic systems. In Tools and Algorithms for the Construction and Analysis of Systems. Springer, LNCS 6605, 326–340.
[3]
M. Bernardo. 1999. Theory and Application of Extended Markovian Process Algebra. Ph.D. Dissertation. University of Bologna.
[4]
C. Cai, J. Sun, G. Dobbie, Z. Hóu, H. Bride, J. Dong, and S. Lee. 2022. Fast automated abstract machine repair using simultaneous modifications and refactoring. Form. Asp. Comput. 34, 2 (2022), 8:1–8:31.
[5]
T. Chen, E. M. Hahn, T. Han, M. Kwiatkowska, H. Qu, and L. Zhang. 2013. Model repair for Markov decision processes. In 2013 International Symposium on Theoretical Aspects of Software Engineering. 85–92.
[6]
C. Dehnert, S. Junges, J.-P. Katoen, and M. Volk. 2017. A storm is coming: A modern probabilistic model checker. In Computer Aided Verification, R. Majumdar and V. Kunčak (Eds.). Springer, LNCS 10427, Cham, 592–600.
[7]
N. Götz. 1994. Stochastische Prozessalgebren: Integration von funktionalem Entwurf und Leistungsbewertung Verteilter Systeme. Ph.D. Dissertation. University of Erlangen-Nuremberg, Germany. http://d-nb.info/941439879
[8]
A. Gouberman, M. Siegle, and B. S. K. Tati. 2019. Markov chains with perturbed rates to absorption: Theory and application to model repair. Perform. Eval. 130 (2019), 32–50. DOI:
[9]
M. Grau-Sanchez, A. Grau, and M. Noguera. 2011. On the computational efficiency index and some iterative methods for solving systems of nonlinear equations. J. Comput. Appl. Math. 236, 6 (2011), 1259–1266.
[10]
H. Hermanns, U. Herzog, and J.-P. Katoen. 2002. Process algebra for performance evaluation. Theor. Comput. Sci. 274, 1 (2002), 43–87. DOI:
[11]
J. Hillston. 1996. A Compositional Approach to Performance Modelling. Cambridge University Press, New York, NY, USA.
[12]
O. Ibe and K. Trivedi. 1990. Stochastic Petri net models of polling systems. IEEE J. Sel. Areas Commun. 8, 9 (1990), 1649–1657.
[13]
Gurobi Optimization, Inc.(n.d.). Gurobi, Version 9.5, 2022. https://www.gurobi.com
[14]
The MathWorks, Inc.(n.d.). Matlab, Version R2022a, 2022. https://www.mathworks.com
[15]
Wolfram Research, Inc.(n.d.). Mathematica, Version 12.2.0.0. https://www.wolfram.com/mathematica
[16]
M. Kuntz, M. Siegle, and E. Werner. 2004. Symbolic performance and dependability evaluation with the tool CASPA. In Applying Formal Methods: Testing, Performance and M/E Commerce (FORTE ’04 Workshops), European Performance Engineering Workshop. Springer, LNCS 3236, 293–307.
[17]
M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11) (LNCS), Vol. 6806. Springer, 585–591.
[18]
J. M. Martínez. 1994. Algorithms for solving nonlinear systems of equations. In Algorithms for Continuous Optimization: The State of the Art, Emilio Spedicato (Ed.). Springer Netherlands, 81–108.
[19]
J. Meyer. 1980. On evaluating the performability of degradable computing systems. IEEE Trans. Comput. C-29, 8 (1980), 720–731. DOI:
[20]
R. Milner. 1980. A Calculus of Communicating Systems. Springer, LNCS 92.
[21]
S. Pathak, E. Ábrahám, N. Jansen, A. Tacchella, and J.-P. Katoen. 2015. A greedy approach for the efficient repair of stochastic models. In NASA Formal Methods, K. Havelund, G. Holzmann, and R. Joshi (Eds.). Springer, LNCS 9058, Cham, 295–309.
[22]
PRISM. Cyclic Server Polling System CTMC case study. Retrieved September 14, 2023 from https://www.prismmodelchecker.org/casestudies/polling.php
[23]
J. R. Sharma, R. K. Guha, and R. Sharma. 2013. An efficient fourth order weighted-Newton method for systems of nonlinear equations. Numer. Algorithms 62 (2013), 307–323.
[24]
M. Siegle and A. Soltanieh. 2022. Rate lifting for stochastic process algebra—Exploiting structural properties. In Quantitative Evaluation of Systems, E. Ábrahám and M. Paolieri (Eds.). Springer, LNCS 13479, Cham, 67–84.
[25]
K. Sikorski. 1985. Optimal solution of nonlinear equations. J. Complex. 1, 2 (1985), 197–209.
[26]
A. Soltanieh. 2022. Compositional Stochastic Process Algebra Models: A Focus on Model Repair and Rate Lifting. Ph.D. Dissertation. Universität der Bundeswehr München, Dept. of Computer Science.
[27]
A. Soltanieh and M. Siegle. 2020. It sometimes works: A lifting algorithm for repair of stochastic process algebra models. In Measurement, Modelling and Evaluation of Computing Systems. Springer, LNCS 12040, 190–207.
[28]
A. Soltanieh and M. Siegle. 2021. Solving systems of bilinear equations for transition rate reconstruction. In Fundamentals of Software Engineering, H. Hojjat and M. Massink (Eds.). Springer, LNCS 12818, Cham, 157–172.
[29]
B. S. K. Tati and M. Siegle. 2016. Rate reduction for state-labelled Markov chains with upper time-bounded CSL requirements. In Proceedings of Casting Workshop onGames for the Synthesis of Complex Systems and 3rd International Workshop onSynthesis of Complex Parameters (Electronic Proceedings in Theoretical Computer Science), T. Brihaye, B. Delahaye, L. Jezequel, N. Markey, and J. Srba (Eds.), Vol. 220. Open Publishing Association, 77–89. DOI:
[30]
H. Wang, D. I. Laurenson, and J. Hillston. 2008. Evaluation of RSVP and mobility-aware RSVP using performance evaluation process algebra. In IEEE International Conference on Communications (ICC). IEEE, 192–197.
Index Terms
- Rate Lifting for Stochastic Process Algebra by Transition Context Augmentation
Recommendations
Rate Lifting for Stochastic Process Algebra – Exploiting Structural Properties –
Quantitative Evaluation of SystemsAbstractThis paper 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 ...
Giving a net semantics to Markovian process algebra
PNPM '95: Proceedings of the Sixth International Workshop on Petri Nets and Performance ModelsWe define two compositional net semantics for the stochastic process algebra Markovian process algebra (MPA), based on a class of stochastic Petri nets. The first semantics is operational in style and is defined by structural induction. We prove that ...
A fluid analysis framework for a Markovian process algebra
Markovian process algebras, such as PEPA and stochastic @p-calculus, bring a powerful compositional approach to the performance modelling of complex systems. However, the models generated by process algebras, as with other interleaving formalisms, are ...
Comments
Information & Contributors
Information
Published In
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 10 July 2024
Online AM: 08 April 2024
Accepted: 26 March 2024
Revised: 15 December 2023
Received: 30 March 2023
Published in TOMACS Volume 34, Issue 3
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 74Total Downloads
- Downloads (Last 12 months)74
- Downloads (Last 6 weeks)9
Reflects downloads up to 22 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in