Associating a Markov Process with Maude Executable Modules

In this paper, we explore a methodology for generating a Markov chain directly from executable modules in Maude. Initially, we incorporate stochastic parameters in Maude specifications in a straightforward and flexible way. Then, we focus on accurately computing state transition rates, a challenging task due to the complexities introduced by rewriting logic semantics. Our methodology is general and relies on a structured description of states that includes the exact state transition rates. This capability allows for the complete automation of the process, a crucial aspect of our ongoing research. We illustrate this methodology using stochastic rewritable Petri nets, a powerful model for adaptive distributed systems. Finally, we present some preliminary findings based on application examples.