The modeling and analysis of adaptive distributed systems, specifically those that possess (self-)reconfiguration or modification capabilities, present a considerable challenge, necessitating the use of appropriate formalisms and techniques. Traditional quantitative analysis frameworks demonstrate constrained expressiveness and should be amalgamated with innovative methodologies. Rewriting-based frameworks appear to be more suitable, despite their predominant application in formal verification. This paper examines the use of Maude as a framework for performance or probabilistic analysis in adaptive distributed systems, highlighting recent advances.
Analyzing and modeling adaptive distributed systems, particularly those with capabilities for (self-) reconfiguration or modification, pose significant challenges and require the application of suitable formalisms and techniques. Traditional quantitative analysis frameworks, including stochastic process algebras, timed and stochastic Petri nets (PN) and timed/probabilistic automata exhibit limited expressiveness when the system undergoes big changes during its execution. These modeling frameworks lead to the merging of functional and non-functional elements within models, impacting scalability. Various noteworthy extensions have been suggested, such as the -calculus, the Ambient calculus, and the Nets-within-Nets paradigm. However, these extensions have not been well-supported by tools and eficient analysis features. Systems based on rewriting, especially Graph Transformation Systems, are more suitable, but they are mainly used for formal verification. This paper explores the utilization of Maude as a framework for performance or probabilistic analysis in adaptive distributed systems, focusing on recent progress.
Maude [
Maude possesses intuitive rewriting semantics. Statements are classified as equations (utilized as
simplifications) or rewrite rules (representing local concurrent transitions). A Maude specification
comprises Functional modules (which contain only equations) and System modules (which include
rules and potentially equations). A functional module characterizes a theory (Σ , ∪ ) within the
framework of membership equational logic: Σ constitutes the signature (operators, sorts, subsorts),
comprises the set of axioms, and encapsulates the operator equational attributes (such as AC).
The model of an equational theory is the initial algebra, specifically, the quotient term algebra Σ/∪,
which, assuming confluence and termination conditions are met, is isomorphic to the canonical term
algebra: consequently, the mathematical and operational semantics align. A system module represents a
rewrite theory (Σ , ∪ , ), being a nonempty set of rules. The corresponding model is set forth as
a labeled transition system (TS) associated with each term: therein, the distributed states are represented
by canonical terms, whereas state transitions illustrate classes of equivalent rewrites.
Related Works Several options exist for timed and probabilistic analysis using Maude. [
In [
Calculating the MC stochastic matrix exactly is challenging due to rewriting logic semantics, which obfuscates multiple state transitions. The methodology, which functions for any Maude executable specification, is illustrated through a challenging application domain: stochastic PN with a dynamically changing structure (see the next section). This application example outlines all the potential issues related to the accurate derivation of a Markov process from Maude executable modules.
The rewriting logic establishes a labeled transition system (TS) associated with ground terms of any type. However, deriving a consistent Markov chain for this TS presents challenges for three main reasons: TS state transitions correspond to equivalence classes of rewrites; equivalent rewrites may be logically indistinguishable and need to be united; and local rewrites of subterms within a specific term may occur. To our knowledge, none of the mentioned techniques addresses all these issues. Our method, which delineates a class of meta-operators at the object level, is more straightforward to implement and significantly more eficient than the predefined Maude’s meta-level modules when addressing extensive state spaces (comprising dozens or hundreds millions of states). In addition, it shows greater precision compared to using the Maude’s strategy language.
Stochastic parameters are first integrated into a Maude executable specification (a system module) lfexibly and intuitively. Next, the challenge of accurately calculating state transition rates is tackled by methodically preprocessing executable modules so that they generate an enhanced description of states associated with terms, which contains all the information to calculate state-transition rates exactly. Thus, we obtain the corresponding MC generator matrix through fundamental text processing.
We will outline the method to obtain the MC generator matrix using the Maude
representation of Stochastic Petri Nets (SPN) [
This module is imported in the protecting mode, thus preserving the initial semantics within the module SPN-SIG, utilizing the formal parameter PL as the actual parameter for BAG. Specifically, the sort Pbag encompasses multisets of places. SPN transitions, which are terms of sort Tran, are characterized by labels associated with adjacency lists, conveyed through Pbag triples [I, O, H]. These labels consist of a descriptive tag (a String in our context), a Float representing the rate parameter of a negative exponential firing delay, and a Nat that specifies the firing policy. For example, the ground term:
t("a", 1.5, 0) |-> [1 . p(1) + 2 . p(2), 1 . p(1), 2 . p(1)] delineates a transition identified by the label "a", an exponential firing rate = 1.5, and typified by an infinite-server type. This transition requires the presence of exactly one token in place 1 and a minimum of two tokens in place 2 for the enabling. Upon firing, it removes two tokens from 2. The PT net that underlies an SPN, classified as a term of type Net, is defined straightforwardly in a modular fashion through the utilization of the associative/commutative juxtaposition ; and the subsort relationship Tran < Net.
Using the predefined firingRate operator, we can define marking-dependent rates: The current definition is based on the enabling degree ( (, )), which refers to the occurrences of a transition that are simultaneously enabled in a marking. Under the infinite server policy (0), the transition exponential rate is · (, ). Under the -server policy, > 0, it is · ((, ), ).
The system module SPN-SYS{TL :: TRIV, PL ::TRIV} extends SPN-SIG by defining the SPN ifring rule as a rewrite rule. This rule applies to the System terms, composed of a Net and a Pbag subterm.
In the Transition System (TS) generated in Maude, a single state transition may amalgamate multiple
"equivalent" instances. For instance, consider various (SPN) transitions that are enabled in a given
marking and upon firing reach the same target marking. This occurs frequently, for example, when
generating a TS quotient using a canonical representative for markings [
1. rewrite rules are translated into kinds of "meta-level" operators (at the object-level), which compute every distinguished rule match 2. because rewrite rules can apply locally to fragments of subject terms, they are encapsulated at the level of a subject term of in accordance with the terms’ abstract syntax graph 3. upon preprocessing, an augmented TS is created wherein states include the exact state transition rates
Several experiments show tolerable overhead resulting from redundant state representation. Alternatives relying on Maude’s predefined meta-level modules or strategy language tend to be unwieldy or imprecise and lack the capacity for full automation.
Focusing on point 1, which is critical in the process, the following excerpt shows the result of the automated encoding of the SPN firing rule in a corresponding firing match operator (subject to further optimization, here ignored): A term of sort StateTran{System} encompasses a target marking and the corresponding rate. The classic fixed-point iteration is used to calculate all possible matches (variable substitutions) of the rule. The same schema applies to any rewrite rule. var T : Tran . vars M M’ : Pbag . vars N N’ : Net . var S : System . var R : Float . var X : Set{StateTran{System}}. var XM : Match. crl [firing] : N M => N fire(T, M) if T ; N’ := N /\ enabled(T, M) /\ R := firingRate(T, M) . ∗∗∗ rule’s translation into an operator op firing−match : System −> Set{StateTran{System}} . eq firing−match(S) = $firing−match(S,noStateTranS) . op $firing−match : System Set{StateTran{System}} −> Set{StateTran{System}} . ceq $firing−match(S, X) = $firing−match(S, (XM −−> S’ : R) U X) if (T ; N) M := S /\ enabled(T, M) /\ S’ := (T ; N) firing(T, M) /\ R := firingRate(T, M) /\ XM := {N} & {T} & {M} /\ (XM −−> M’ : R) in X = false . eq $firing−match(S, X) = X [owise] .
Rewritable Petri nets ([
Rewriting rule Pattern
Rewrite Application
Rewriting rule Pattern
Rewrite
Application
Rewrite rules that rely on symmetric net transformations preserve this labeling strategy. Analyzing models modulo automorphisms is essential to maintain scalability across all frameworks predicated on graph transformation systems, of which rewritable PNs serve as an exemplar. In [13], we have extended rewritable PNs by incorporating stochastic parameters and outline a semi-automated procedure to extract a compact continuous-time Markov chain (CTMC) from the TS quotient.
m1
S0 m2 m1
S0 m2 … m1 m1
S0 m2 m1
… m1
m2 S1 m2 m1
S1 m2 m1
S2 m2
This CTMC satisfies the exact lumpability property, which parallels the strong bisimilarity observed
in the quotient transition system. The eficacy of this approach has been illustrated using a composite
model of a gracefully degrading production system. We believe that by integrating the methodology
described in [
By creating proper rules, the semantics of a specific modeling formalism can be implemented. For example, Fig.1 shows how the semantics of a Petri net can be interpreted as a graph rewriting system. In particular, in Fig.1a), a rule matches a pattern consisting of a place marked with one token, connected to a transition, which is further connected to a place. The application of the rule rewrites the identified subnetwork, with one in which the token has been moved to the second place. Fig.1b) shows how these rewriting rules can be extended to a more complex case, where a pattern contains two tokens inside two input places, and the rewriting rule combines them and marks the third place. Please note that, generally, rules are specified using functional expressions, so one rule can match a large number of cases, making this process enumerable and feasible.
One of the most interesting properties of these types of rewriting system is that the nodes of the graphs can be graphs themselves. In this way, the rewriting can even produce the infinitesimal generator of a Stochastic Petri Net Model, as shown in Fig.2. In this case, the initial graph is composed of a single node, which is itself a graph that corresponds to the Petri Net in its initial state.
The first rewriting (whose formalization as a rule is omitted for simplicity) transforms this graph into another that adds a node, with the marking obtained by the first transition, and a connection, labeled with the transition rate ( 1) at which this event occurred. A second rewriting adds a third node to the m1 m2 S2
m1 0x outermost graph, which contains the final Petri net configuration, connected with an arc labeled with rate 2. This corresponds to the CTMC that describe the evolution of the considered Stochastic Petri Nets, as shown in Fig.3
One of the advantages of creating the infinitesimal generator through graph rewriting is that the configurations of the model represented by the states of the CTMC are created in a compact way that natively performs lumping, as shown in Fig.4. This allows us to generate CTMCs with state spaces much smaller than in conventional techniques.
In this example, a model where three identical components are present, plus a second diferent one, is encoded by having the three possible evolution of each subcomponent exposed, and counting that we have three of them representing the initial state of the system are required. Also, the lower part of the model is encoded with an additional sub-network, where currently the version with the empty place is used once. This makes the classical state-space reduction techniques based on symmetries considered native, thus reducing the generated state spaces.
In [15], we examine Hornets enhanced by incorporating firing probabilities to represent multi-agent systems with capabilities for self-modification. The theory is explained in more detail in [ 14]. Hornets [16] embody a Nets-within-Nets formalism, a type of Petri net formalism characterized by tokens that themselves are Petri nets. Each net-token possesses its own firing rate, which operates independently from the firing rates of other net-tokens. Hornets furnish algebraic operations that enable modification of net tokens during firing. Within our probabilistic extension, these operators are capable of individually adjusting the net-token firing rate.
Our model is used to conduct a quantitative analysis of self-modifying systems. Hornets are particularly adept at modeling self-adaptive systems engaged in a MAPE-like loop (monitor-analyzeplan-execute). In this context, the system net represents the feedback loop, whereas the net-tokens illustrate the adapted model elements. We introduce a subclass of Hornets that can be readily formalized in Maude. Consequently, this allows for the utilization of additional tools for generating probabilistic state spaces, specifically, discrete Markov chains, in our stochastic framework.
We would like to illustrate our ideas by an idea first presented in [ 14]. Our self-adaptive system is based on the battle-of-sexes scenario, which is well known in game theory. Two agents, named 0 and 1, must choose between two actions, labeled and , = 0, 1. They receive a positive reward if they choose the same action (i.e. coordinate) and zero otherwise.
In this game, the first agent prefers action , while the second prefers . If we assume that the reward for the preferred outcome is three times higher than for the other, then the game is specified by the payof matrix: 0 0
1 (3, 1) (0, 0)
1 (0, 0) (1, 3)
Let (⟨⟩⊕ ⟨⟩) describe the probabilistic xor choice between action and where Λ( ) = and Λ( ) = . The object net that models this game is shown as a net-token in Fig. 5; it is a parallel composition (denoted by _‖_) of two choices (for some initial values of 0, 0, 1, and 1): 1Λ = (0⟨0⟩⊕ ⟨0⟩0) ‖ (1⟨1⟩⊕ ⟨1⟩1) (1)
The system net observes the decision history and adapts by modifying the rates (cf. eHornet in Fig. 5). We have four transitions named play game on the right side corresponding to the four diferent ways of choosing the actions. We give the payof as a reward signal to the agents. (There may be more appropriate ways to adapt, but for this simple example, we do not care about the eficiency of the learning process.) For example, when the agents play (0, 1), then we update the rates in the workflow by the payof (3, 1), and we obtain the following.
2Λ = (0⟨0+3⟩⊕ ⟨0⟩0) ‖ (1⟨1+1⟩⊕ ⟨1⟩1) (2)
We have another source of adaption in the system net: Choices that are chosen quite regularly over a longer time period are converted into fixed structures without choice by the two transitions named adapt XOR on the left-hand side. In this example, the transformation is allowed whenever 0 is chosen 0 in more than 80% of the time. This is expressed by the transition guard (0+0) > 0.8. Then, we obtain 3Λ = 0 ‖ (1⟨1⟩⊕ ⟨1⟩1) as the modified net structure. Analogously, whenever 0 dominates. (For simplicity, we omit modifications in the model whenever the second agent has a dominating option.)
In [14] we implemented Hornets in Maude to translate our game-theoretical model into a Discrete Time Markov Chain (DTMC) to establish guarantees for the occurrence of structural modifications within a given number of execution steps.
Rewriting also provides solid and powerful support for the analysis of multiformalism models [17]. Multiformalism models typically exhibit complexity, modularity and heterogeneity in the formalisms which define modules: rewriting can be used to add dynamic solution-time features to multiformalism models, by allowing the dynamic generation or adaptation of modules to take into account partial results and ease model parameterization while lowering the complexity of the analysis process. For example, rewriting is being used to incorporate in SIMTHESys [18] the features obtained in OsMoSys [19] by means of a complex orchestration engine [20].
Fig.6 shows a re-writable multiformalism model, which is detailed in Fig.7.
The model represents a two-tier architecture that serves requests generated by users, whose "think time" is modeled by the place 3 and the transition 3 of the submodel 2. The two tiers can be deployed on two servers that might experience down periods. In particular, place 2 of the submodel 1 contains as many tokens as the current number of active servers, 1 models the possibility that a PN2
T1 T2
P2 PN1
P1
T1 T2
P2 PN1
P1
T1 T2
P2
V2 V1
Q1
Q2
Q3 A->BCS1 PN2
NP3
T3
V0
P5
P4 T4 server goes down, 1 accounts for the number of servers that are not available, and 2 models the return in operation of one of the servers. Depending on the marking 2, the submodel identified with ? is replaced by a diferent implementation. In particular, when both servers are available, the submodel used is 2, a queueing network with two stations 1 and 2 that represents the two tiers. Each station is characterized by its own service time. When one server goes down, the submodel ? becomes the multiclass queuing network represented in 1. In this case, a single multiclass queueing station 3 is used, where the current tier being executed is represented by the class of the job. When the first-tier jobs end, they change class due to the class switch 1 and re-enters 3 as costumers of the other class. When the second tier finishes, they can leave the subnetwork. If both servers are down simultaneously, ? is replaced by the Colored Petri Net represented in 0. Here, jobs are tokens, colored by their current stage. The place 5 collects interrupted jobs that wait for server availability. The place 4 and the forever disabled transition 4 illustrate the blockage of the system, preventing user activity.
As briefly shown in this paper, rewriting techniques have a great potential as means to improve the eficiency of the analysis of complex stochastic models and to support advanced modeling approaches such as multiformalism modeling, on which future work will focus to verify at which extent this potential will manage to support the implementation of advanced dynamic features for the parametric analysis-time model adaptation and generation.
This work was partially funded by the MUR project “T-LADIES” (PRIN 2020TL3X8X).
The author(s) have not employed any Generative AI tools. [13] L. Capra, M. Gribaudo, A lumped CTMC for modular rewritable PN, in: J. Doncel, A. Remke, D. Di Pompeo (Eds.), Computer Performance Engineering, Springer Nature Switzerland, Cham, 2025, pp. 106–120. [14] M. Köhler-Bußmeier, L. Capra, Analysing probabilistic Hornets, in: E. Amparore, L. Mikulski (Eds.), Application and Theory of Petri Nets and Concurrency (PETRI NETS 2025), volume 15714 of LNCS, Springer, 2025, pp. 287–309. doi:10.1007/978-3-031-94634-9_14. [15] M. Köhler-Bußmeier, L. Capra, Modelling and simulation of adaptive multi-agent systems with stochastic nets-within-nets, in: Proceedings of the 16th International Joint Conference on Computational Intelligence - Volume 1: ECTA, INSTICC, SciTePress, 2024, pp. 313–320. [16] M. Köhler-Bußmeier, Hornets: Nets within nets combined with net algebra, in: K. Wolf, G. Franceschinis (Eds.), International Conference on Application and Theory of Petri Nets (ICATPN’2009), volume 5606 of LNCS, Springer, 2009, pp. 243–262. doi:10.1007/978-3-642-02424-5_15. [17] M. Gribaudo, M. Iacono, Theory and application of multi-formalism modeling, 2013. [18] E. Barbierato, M. Gribaudo, M. Iacono, Modeling hybrid systems in SIMTHESys, Electronic Notes in Theoretical Computer Science 327 (2016) 5 – 25. [19] V. Vittorini, G. Franceschinis, M. Gribaudo, M. Iacono, N. Mazzocca, DrawNet++: Model Objects to Support Performance Analysis and Simulation of Complex Systems, in: Proc. of the 12th Int. Conference on Modelling Tools and Techniques for Computer and Communication System Performance Evaluation (TOOLS 2002), London, UK, 2002. [20] F. Moscato, F. Flammini, G. Di Lorenzo, V. Vittorini, S. Marrone, M. Iacono, The software architecture of the OsMoSys multisolution framework, in: VALUETOOLS 2007 - 2nd International ICST Conference on Performance Evaluation Methodologies and Tools, 2007.