We present DeGAS, a differentiable Gaussian approximate semantics for loopless probabilistic programs that enables sample-free, gradient-based optimization in models with both continuous and discrete components. DeGAS evaluates programs under a Gaussian-mixture semantics and replaces measure-zero predicates and discrete branches with a vanishing smoothing, yielding closed-form expressions for posterior and path probabilities. We prove differentiability of these quantities with respect to program parameters, enabling end-to-end optimization via standard automatic differentiation, without Monte Carlo estimators. On thirteen benchmark programs, DeGAS achieves accuracy and runtime competitive with variational inference and MCMC. Importantly, it reliably tackles optimization problems where sampling-based baselines fail to converge due to conditioning involving continuous variables.

• Automatic model-based load test generation for elastic microservice applications. • Models explicitly couple application and autoscaler dynamics. • Optimization identifies failure-inducing workload traces offline. • Framework supports multiple objectives and workload scenarios. • Generated tests expose performance violations in real microservice applications. Microservice applications are required to consistently guarantee Service-Level Agreements (SLAs) under fluctuating workloads, a challenge commonly addressed through autoscaling mechanisms. However, the effectiveness of an autoscaler strongly depends on the workload scenario, and validating robustness across diverse workload conditions remains an open problem. To address this, we propose an offline model-based framework that automatically generates load test traces designed to expose performance failures in elastic microservice applications. The system under test is modeled as a closed-loop dynamical system where the microservice application and the autoscaler are explicitly coupled. Specifically, we encode both components as piecewise affine functions, allowing a wide set of applications and autoscalers to be captured. Test generation is framed using a falsification approach and solved as a mixed-integer linear program, eliminating the need for manual configuration or real system interactions during test generation. The generated test cases are designed to cause SLA violations, uncovering critical workload scenarios that may be overlooked by existing approaches. We evaluate the framework on both a realistic benchmark microservice application and a population of randomly generated systems, demonstrating that the generated traces consistently induce performance failures in real deployments. Furthermore, we show that the method generalizes across different autoscaling policies and workload patterns, producing valid test traces within short time intervals. Finally, we discuss and compare alternative approaches for load test generation. These experiments highlight both the effectiveness of the approach in exposing performance violations and its applicability to diverse autoscaling configurations.

Abstract Chemical reaction networks (CRNs) are an established population model defined as a system of coupled nonlinear ordinary differential equations across many disciplines. In many applications, for example, in systems biology and epidemiology, CRN parameters such as the kinetic reaction rates can be used as control inputs to steer the system toward a given target. Unfortunately, the resulting optimal control problem is nonlinear, therefore, computationally very challenging. We address this issue by introducing an optimality-preserving reduction algorithm for CRNs. The algorithm partitions the original state variables into a reduced set of macro-variables for which one can define a reduced optimal control problem with provably identical optimal values. The reduction algorithm runs with polynomial time complexity in the size of the CRN. We use this result to reduce verification and control problems of large-scale vaccination models over real-world networks.

Abstract Adaptive systems are designed to modify their behaviour at runtime in response to dynamically changing and open-ended environments as well as evolving requirements. Such systems may operate as individual adaptive entities or as collective adaptive systems composed of multiple collaborating components. Rigorous engineering of these systems requires appropriate methods, models, and tools that ensure reliability, correctness, and alignment with their intended purpose. This paper introduces the second part of the special section on Rigorous Engineering of Collective Adaptive Systems. It presents seven selected contributions and positions them within four major research directions: (i) Large Ensembles and Collective Dynamics, (ii) Knowledge, Consciousness and Emergence, (iii) Automated Reasoning for Better Interaction, and (iv) Analysing Collective Adaptive Systems. Together, they illustrate current progress and emerging challenges in the rigorous engineering of collective adaptive systems.

Network embedding is a fundamental technique to project a network into a lower-dimensional space while preserving similarities among nodes. Traditional network embeddings primarily capture node proximity, making them effective for community detection but insufficient for identifying roles, i.e., patterns of interaction beyond local neighborhoods. To address this limitation, we introduce a simple and efficient embedding technique based on approximate variants of equitable partitions. Our approach, called \varepsilon-BE, introduces a user-tunable tolerance parameter relaxing the otherwise strict condition for exact equitable partitions that can be hardly found in real-world networks. We exploit a relationship between equitable partitions and equivalence relations for Markov chains and ordinary differential equations to develop a partition refinement algorithm for computing an approximate equitable partition in polynomial time. We extend this framework to weighted and directed networks, ensuring applicability to a more general class of graphs and filling a gap in the literature where few approaches are present. We compare our method against state-of-the-art embedding techniques on synthetic and real-world networks. We report comparable—when not superior—performance for visualization, classification, clustering, and regression tasks with smaller running times, enabling the embedding of large-scale networks that could not be efficiently handled by most of the competing techniques. These results and the capability to handle weighted and directed networks make our approach a compelling alternative for structural network embedding.

Microservices have become the architecture of choice for cloud applications requiring high performance and scalability. Autoscaling, which dynamically adjusts resource allocation based on workload fluctuations, is key to optimizing performance and controlling costs. This paper presents$\mu$Opt, a computationally efficient, model-based autoscaler specifically designed for microservices.$\mu$Opt leverages a nonlinear optimization problem tied to a fluid approximation of a layered queuing network (LQN) model to determine optimal configurations that maximize key performance metrics—such as throughput, CPU usage, and response time—while minimizing operational costs. On a well-known benchmark application, our numerical experiments show that$\mu$Opt achieves fast solution times, enabling responsiveness to dynamic workloads. Compared to a state-of-the-art LQN-based autoscaler employing genetic algorithms,$\mu$Opt delivers improved application performance using fewer resources. To demonstrate the robustness and generalizability of our underlying model, we validate its prediction accuracy across ten randomly generated applications with diverse architectures, showing that its performance is a reliable foundation for autoscaling. Finally, it also outperforms Horizontal Pod Autoscaler, a production-ready solution for Kubernetes deployments in Google Cloud Platform, consistently reducing resource usage while more accurately tracking CPU utilization targets across both synthetic and real-world workloads.

Abstract Adaptive systems are designed to modify their behaviour at runtime in response to dynamically changing and open-ended environments as well as evolving requirements. Such systems may operate as individual adaptive entities or as collective adaptive systems composed of multiple collaborating components. Rigorous engineering of these systems requires appropriate methods, models, and tools that ensure reliability, correctness, and alignment with their intended purpose. This paper introduces the first part of the special section on Rigorous Engineering of Collective Adaptive Systems. It presents six of the thirteen selected contributions and positions them within two major research directions: (i) Modelling and Engineering Collective Adaptive Systems, and (ii) Analysing Collective Adaptive Systems. Together, these contributions illustrate current progress and emerging challenges in the rigorous engineering of collective adaptive systems.

Efficient methods for the simulation of quantum circuits on classical computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. In particular, we show that constrained bisimulation can boost decision-diagram-based quantum circuit simulation by several orders of magnitude, allowing thus for substantial synergy effects.

Structural network embedding is a crucial step in enabling effective downstream tasks for complex systems that aim to project a network into a lower-dimensional space while preserving similarities among nodes. We introduce a simple and efficient embedding technique based on approximate variants of equitable partitions. The approximation consists in introducing a user-tunable tolerance parameter relaxing the otherwise strict condition for exact equitable partitions that can be hardly found in real-world networks. We exploit a relationship between equitable partitions and equivalence relations for Markov chains and ordinary differential equations to develop a partition refinement algorithm for computing an approximate equitable partition in polynomial time. We compare our method against state-of-the-art embedding techniques on benchmark networks. We report comparable-when not superior-performance for visualization, classification, and regression tasks at a cost between one and three orders of magnitude smaller using a prototype implementation, enabling the embedding of large-scale networks that could not be efficiently handled by most of the competing techniques.

Abstract Efficient methods for the simulation of quantum circuits on classic computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. Furthermore, we show that constraint bisimulation complements state-of-the-art methods for the simulation of quantum circuits based on decision diagrams.

Computing the posterior distribution of a probabilistic program is a hard task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the exact probabilistic semantics of a bounded program by means of Gaussian mixtures. It is parametrized by a map that associates each program location with the moment order to be matched in the approximation. We provide two main contributions. The first is a universal approximation theorem stating that, under mild conditions, Gaussian Semantics can approximate the exact semantics arbitrarily closely. The second is an approximation that matches up to second-order moments analytically in face of the generally difficult problem of matching moments of Gaussian mixtures with arbitrary moment order. We test our second-order Gaussian approximation (SOGA) on a number of case studies from the literature. We show that it can provide accurate estimates in models not supported by other approximation methods or when exact symbolic techniques fail because of complex expressions or non-simplified integrals. On two notable classes of problems, namely collaborative filtering and programs involving mixtures of continuous and discrete distributions, we show that SOGA significantly outperforms alternative techniques in terms of accuracy and computational time.

Microservice (MS) architecture has become a popular paradigm in software engineering and has been embraced in the industry (e.g., Amazon, Netflix) for cloud-based applications with crucial performance requirements. Surprisingly, assessing how the MS designs affect performance is still a challenging issue, which is generally tackled by extensive and expensive profiling. In this paper, we propose$\mu \mathbf{P}$, a novel development framework for MS applications where performance can be predicted$by$design.$\mu \mathbf{P}$offers an API that automatically generates a per-formance model based on Layered Queuing Networks (LQNs) without requiring any development effort beyond writing the actual system code. The model can then be queried to predict performance metrics such as response time and utilization of individual microservices. We validate$\mu \mathbf{P}$on four benchmarks taken from the literature. The results show the effectiveness of$\mu \mathbf{P}$in accurately predicting performance due to increasing user load, vertical and horizontal scaling. We report prediction errors for response times consistently lower than 10% across a wide range of operating conditions.

Quantitative notions of bisimulation are well-known tools for the minimization of dynamical models such as Markov chains and ordinary differential equations (ODEs). In forward bisimulations, each state in the quotient model represents an equivalence class and the dynamical evolution gives the overall sum of its members in the original model. Here we introduce generalized forward bisimulation (GFB) for dynamical systems over commutative monoids and develop a partition refinement algorithm to compute the coarsest one. When the monoid is (ℝ,+), we recover probabilistic bisimulation for Markov chains and more recent forward bisimulations for nonlinear ODEs. Using (ℝ,•) we get nonlinear reductions for discrete-time dynamical systems and ODEs where each variable in the quotient model represents the product of original variables in the equivalence class. When the domain is a finite set such as the Booleans $\mathbb{B}$, we can apply GFB to Boolean networks (BN), a widely used dynamical model in computational biology. Using a prototype implementation of our minimization algorithm for GFB, we find disjunction- and conjunction-preserving reductions on 60 BN from two well-known repositories, and demonstrate the obtained analysis speed-ups. We also provide the biological interpretation of the reduction obtained for two selected BN, and we show how GFB enables the analysis of a large one that could not be analyzed otherwise. Using a randomized version of our algorithm we find product-preserving (therefore non-linear) reductions on 21 dynamical weighted networks from the literature that could not be handled by the exact algorithm.

BACKGROUND: Boolean Networks (BNs) are a popular dynamical model in biology where the state of each component is represented by a variable taking binary values that express, for instance, activation/deactivation or high/low concentrations. Unfortunately, these models suffer from the state space explosion, i.e., there are exponentially many states in the number of BN variables, which hampers their analysis. RESULTS: We present Boolean Backward Equivalence (BBE), a novel reduction technique for BNs which collapses system variables that, if initialized with same value, maintain matching values in all states. A large-scale validation on 86 models from two online model repositories reveals that BBE is effective, since it is able to reduce more than 90% of the models. Furthermore, on such models we also show that BBE brings notable analysis speed-ups, both in terms of state space generation and steady-state analysis. In several cases, BBE allowed the analysis of models that were originally intractable due to the complexity. On two selected case studies, we show how one can tune the reduction power of BBE using model-specific information to preserve all dynamics of interest, and selectively exclude behavior that does not have biological relevance. CONCLUSIONS: BBE complements existing reduction methods, preserving properties that other reduction methods fail to reproduce, and vice versa. BBE drops all and only the dynamics, including attractors, originating from states where BBE-equivalent variables have been initialized with different activation values The remaining part of the dynamics is preserved exactly, including the length of the preserved attractors, and their reachability from given initial conditions, without adding any spurious behaviours. Given that BBE is a model-to-model reduction technique, it can be combined with further reduction methods for BNs.

It is well known that exact notions of model abstraction and reduction for dynamical systems may not be robust enough in practice because they are highly sensitive to the specific choice of parameters. In this paper we consider this problem for nonlinear ordinary differential equations (ODEs) with polynomial derivatives. We introduce a model reduction technique based on approximate differential equivalence, i.e., a partition of the set of ODE variables that performs an aggregation when the variables are governed by nearby derivatives. We develop algorithms to (i) compute the largest approximate differential equivalence; (ii) construct an approximately reduced model from the original one via an appropriate perturbation of the coefficients of the polynomials; and (iii) provide a formal certificate on the quality of the approximation as an error bound, computed as an over-approximation of the reachable set of the reduced model. Finally, we apply approximate differential equivalences to case studies on electric circuits, biological models, and polymerization reaction networks.

We consider the problem of estimating the numerical accuracy of programs with operations in fixed-point arithmetic and variables of arbitrary, mixed precision, and possibly non-deterministic value. By applying a set of parameterised rewrite rules, we transform the relevant fragments of the program under consideration into sequences of operations in integer arithmetic over vectors of bits, thereby reducing the problem as to whether the error enclosures in the initial program can ever exceed a given order of magnitude to simple reachability queries on the transformed program. We describe a possible verification flow and a prototype analyser that implements our technique. We present an experimental evaluation on a particularly complex industrial case study, including a preliminary comparison between bit-level and word-level decision procedures.

We introduce polynomial couplings, a generalization of probabilistic couplings, to develop an algorithm for the computation of equivalence relations which can be interpreted as a lifting of probabilistic bisimulation to polynomial differential equations, a ubiquitous model of dynamical systems across science and engineering. The algorithm enjoys polynomial time complexity and complements classical partition-refinement approaches because: (a) it implements a local exploration of the system, possibly yielding equivalences that do not necessarily involve the inspection of the whole system of differential equations; (b) it can be enhanced by up-to techniques; and (c) it allows the specification of pairs which ought not be included in the output. Using a prototype, these advantages are demonstrated on case studies from systems biology for applications to model reduction and comparison. Notably, we report four orders of magnitude smaller runtimes than partition-refinement approaches when disproving equivalences between Markov chains.

The automatic derivation of analytical performance models is an essential tool to promote a wider adoption of performance engineering techniques in practice. Unfortunately, despite the importance of such techniques, the attempts pursuing that goal in the literature either focus on the estimation of service demand parameters only or suffer from scalability issues and sub-optimality due to the intrinsic complexity of the underlying optimization methods.

MOTIVATION: Stochastic reaction networks are a widespread model to describe biological systems where the presence of noise is relevant, such as in cell regulatory processes. Unfortunately, in all but simplest models the resulting discrete state-space representation hinders analytical tractability and makes numerical simulations expensive. Reduction methods can lower complexity by computing model projections that preserve dynamics of interest to the user. RESULTS: We present an exact lumping method for stochastic reaction networks with mass-action kinetics. It hinges on an equivalence relation between the species, resulting in a reduced network where the dynamics of each macro-species is stochastically equivalent to the sum of the original species in each equivalence class, for any choice of the initial state of the system. Furthermore, by an appropriate encoding of kinetic parameters as additional species, the method can establish equivalences that do not depend on specific values of the parameters. The method is supported by an efficient algorithm to compute the largest species equivalence, thus the maximal lumping. The effectiveness and scalability of our lumping technique, as well as the physical interpretability of resulting reductions, is demonstrated in several models of signaling pathways and epidemic processes on complex networks. AVAILABILITY AND IMPLEMENTATION: The algorithms for species equivalence have been implemented in the software tool ERODE, freely available for download from https://www.erode.eu. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

MOTIVATION: Detailed mechanistic models of biological processes can pose significant challenges for analysis and parameter estimations due to the large number of equations used to track the dynamics of all distinct configurations in which each involved biochemical species can be found. Model reduction can help tame such complexity by providing a lower-dimensional model in which each macro-variable can be directly related to the original variables. RESULTS: We present CLUE, an algorithm for exact model reduction of systems of polynomial differential equations by constrained linear lumping. It computes the smallest dimensional reduction as a linear mapping of the state space such that the reduced model preserves the dynamics of user-specified linear combinations of the original variables. Even though CLUE works with non-linear differential equations, it is based on linear algebra tools, which makes it applicable to high-dimensional models. Using case studies from the literature, we show how CLUE can substantially lower model dimensionality and help extract biologically intelligible insights from the reduction. AVAILABILITY AND IMPLEMENTATION: An implementation of the algorithm and relevant resources to replicate the experiments herein reported are freely available for download at https://github.com/pogudingleb/CLUE. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

Bioinformatics (2021) doi: 10.1093/bioinformatics/btab010 There were some typographical and formatting errors in the originally published version of this paper. These errors have now been corrected online. These errors were the fault of the publisher, and the publisher apologises for the errors.

Markov chains are a useful model for the quantitative analysis of extra-functional properties of software systems such as performance, reliability, and energy consumption. However building Markov models of software systems remains a difficult task. Here we present a statistical method that learns a Markov chain directly from a program, by means of execution runs with inputs sampled by given probability distributions. Our technique is based on learning algorithms for so-called variable length Markov chains, which allow us to capture data dependency throughout execution paths by encoding part of the program history into each state of the chain. Our domain-specific adaptation exploits structural information about the program through its control-flow graph. Using a prototype implementation, we show that this approach represents a significant improvement over state-of-the-art general-purpose learning algorithms, providing accurate models in a number of benchmark programs.

It is well known that building analytical performance models in practice is difficult because it requires a considerable degree of proficiency in the underlying mathematics. In this paper, we pro- pose a machine-learning approach to derive performance models from data. We focus on queuing networks, and crucially exploit a deterministic approximation of their average dynamics in terms of a compact system of ordinary differential equations. We encode these equations into a recurrent neural network whose weights can be directly related to model parameters. This allows for an inter- pretable structure of the neural network, which can be trained from system measurements to yield a white-box parameterized model that can be used for prediction purposes such as what-if analyses and capacity planning. Using synthetic models as well as a real case study of a load-balancing system, we show the effectiveness of our technique in yielding models with high predictive power.

Abstract Electric circuits manipulate electric charge and magnetic flux via a small set of discrete components to implement useful functionality over continuous time-varying signals represented by currents and voltages. Much of the same functionality is useful to biological organisms, where it is implemented by a completely different set of discrete components (typically proteins) and signal representations (typically via concentrations). We describe how to take a linear electric circuit and systematically convert it to a chemical reaction network of the same functionality, as a dynamical system. Both the structure and the components of the electric circuit are dissolved in the process, but the resulting chemical network is intelligible. This approach provides access to a large library of well-studied devices, from analog electronics, whose chemical network realization can be compared to natural biochemical networks, or used to engineer synthetic biochemical networks.

Accurate estimation of resource demands is one of the key challenges to be able to use queuing networks (QNs) for performance prediction, especially in cases where the profiling is to be performed through a non-intrusive system instrumentation. This problem is worsened when one needs to obtain a continuously updated model (e.g., for control and adaptation purposes) because it becomes crucial to use fast estimation methods that do not interfere with the behavior of the running system. A crucial limitation in the state of the art is the assumption that the measurement are taken from a system in the steady state regime. To the best of our knowledge, this paper presents the first approach-here developed for single-class QNs-that does not make such assumption. Our service-demand estimation technique relies on a deterministic approximation of the QN where the transient evolution of the queue lengths is modeled by means of a compact analytical representation based on a system of coupled nonlinear ordinary differential equations. We set up a moving-horizon estimation problem whereby the governing equations of the model, appropriately unfolded over a given time horizon, represent the constraints of a quadratic program that seeks to find the optimal choice of service demands that minimize the error between the measured queue lengths and the predicted ones. An extensive numerical evaluation demonstrates the efficiency and the effectiveness of our approach against the state-of-the-art techniques for service demands estimation.

Discovering relations between chemical reaction networks (CRNs) is a relevant problem in computational systems biology for model reduction, to explain if a given system can be seen as an abstraction of another one; and for model comparison, useful to establish an evolutionary path from simpler networks to more complex ones. This is also related to foundational issues in computer science regarding program equivalence, in light of the established interpretation of a CRN as a kernel programming language for concurrency. Criteria for deciding if two CRNs can be formally related have been recently developed, but these require that a candidate mapping be provided. Automatically finding candidate mappings is very hard in general since the search space essentially consists of all possible partitions of a set. In this paper we tackle this problem by developing a genetic algorithm for a class of CRNs called influence networks, which can be used to model a variety of biological systems including cell-cycle switches and gene networks. An extensive numerical evaluation shows that our approach can successfully establish relations between influence networks from the literature which cannot be found by exact algorithms due to their large computational requirements.

A key challenge in software systems that are exposed to runtime variabilities, such as workload fluctuations and service degradation, is to continuously meet performance requirements. In this paper we present an approach that allows performance self-adaptation using a system model based on queuing networks (QNs), a well-assessed formalism for software performance engineering. Software engineers can select the adaptation knobs of a QN (routing probabilities, service rates, and concurrency level) and we automatically derive a Model Predictive Control (MPC) formulation suitable to continuously configure the selected knobs and track the desired performance requirements. Previous MPC approaches have two main limitations: i) high computational cost of the optimization, due to nonlinearity of the models; ii) focus on long-run performance metrics only, due to the lack of tractable representations of the QN's time-course evolution. As a consequence, these limitations allow adaptations with coarse time granularities, neglecting the system's transient behavior. Our MPC adaptation strategy is efficient since it is based on mixed integer programming, which uses a compact representation of a QN with ordinary differential equations. An extensive evaluation on an implementation of a load balancer demonstrates the effectiveness of the adaptation and compares it with traditional methods based on probabilistic model checking.

We study chemical reaction networks (CRNs) as a kernel language for concurrency models with semantics based on ordinary differential equations. We investigate the problem of comparing two CRNs, i.e., to decide whether the trajectories of a source CRN can be matched by a target CRN under an appropriate choice of initial conditions. Using a categorical framework, we extend and relate model-comparison approaches based on structural (syntactic) and on dynamical (semantic) properties of a CRN, proving their equivalence. Then, we provide an algorithm to compare CRNs, running linearly in time with respect to the cardinality of all possible comparisons. Finally, we apply our results to biological models from the literature.

Ordinary differential equations (ODEs) are widespread in many natural sciences including chemistry, ecology, and systems biology, and in disciplines such as control theory and electrical engineering. Building on the celebrated molecules-as-processes paradigm, they have become increasingly popular in computer science, with high-level languages and formal methods such as Petri nets, process algebra, and rule-based systems that are interpreted as ODEs. We consider the problem of comparing and minimizing ODEs automatically. Influenced by traditional approaches in the theory of programming, we propose differential equivalence relations. We study them for a basic intermediate language, for which we have decidability results, that can be targeted by a class of high-level specifications. An ODE implicitly represents an uncountable state space, hence reasoning techniques cannot be borrowed from established domains such as probabilistic programs with finite-state Markov chain semantics. We provide novel symbolic procedures to check an equivalence and compute the largest one via partition refinement algorithms that use satisfiability modulo theories. We illustrate the generality of our framework by showing that differential equivalences include (i) well-known notions for the minimization of continuous-time Markov chains (lumpability), (ii)~bisimulations for chemical reaction networks recently proposed by Cardelli et al., and (iii) behavioral relations for process algebra with ODE semantics. With a prototype implementation we are able to detect equivalences in biochemical models from the literature that cannot be reduced using competing automatic techniques.

Applications executed on multicore embedded systems interact with system software [such as the operating system (OS)] and hardware, leading to widely varying thermal profiles which accelerate some aging mechanisms, reducing the lifetime reliability. Effectively managing the temperature therefore requires: 1) autonomous detection of changes in application workload and 2) appropriate selection of control levers to manage thermal profiles of these workloads. In this paper, we propose a technique for workload change detection using density ratio-based statistical divergence between overlapping sliding windows of CPU performance statistics. This is integrated in a runtime approach for thermal management, which uses reinforcement learning to select workload-specific thermal control levers by sampling on-board thermal sensors. Identified control levers override the OSs native thread allocation decision and scale hardware voltage-frequency to improve average temperature, peak temperature, and thermal cycling. The proposed approach is validated through its implementation as a hierarchical runtime manager for Linux, with heuristic-based thread affinity selected from the upper hierarchy to reduce thermal cycling and learningbased voltage-frequency selected from the lower hierarchy to reduce average and peak temperatures. Experiments conducted with mobile, embedded, and high performance applications on ARM-based embedded systems demonstrate that the proposed approach increases workload change detection accuracy by an average 3.4×, reducing the average temperature by 4 °C-25 °C, peak temperature by 6 °C-24 °C, and thermal cycling by 7%-35% over state-of-the-art approaches.

We study the problem of making forecasts about the future availability of bicycles in stations of a bike-sharing system (BSS). This is relevant in order to make recommendations guaranteeing that the probability that a user will be able to make a journey is sufficiently high. To do this we use probabilistic predictions obtained from a queuing theoretical time-inhomogeneous model of a BSS. The model is parametrized and successfully validated using historical data from the Vélib' BSS of the City of Paris.

We present two quantitative behavioral equivalences over species of a chemical reaction network (CRN) with semantics based on ordinary differential equations. Forward CRN bisimulation identifies a partition where each equivalence class represents the exact sum of the concentrations of the species belonging to that class. Backward CRN bisimulation relates species that have identical solutions at all time points when starting from the same initial conditions. Both notions can be checked using only CRN syntactical information, i.e., by inspection of the set of reactions. We provide a unified algorithm that computes the coarsest refinement up to our bisimulations in polynomial time. Further, we give algorithms to compute quotient CRNs induced by a bisimulation. As an application, we find significant reductions in a number of models of biological processes from the literature. In two cases we allow the analysis of benchmark models which would be otherwise intractable due to their memory requirements.

In software performance engineering, what-if scenarios, architecture optimization, capacity planning, run-time adaptation, and uncertainty management of realistic models typically require the evaluation of many instances. Effective analysis is however hindered by two orthogonal sources of complexity. The first is the infamous problem of state space explosion -- the analysis of a single model becomes intractable with its size. The second is due to massive parameter spaces to be explored, but such that computations cannot be reused across model instances. In this paper, we efficiently analyze many queuing models with the distinctive feature of more accurately capturing variability and uncertainty of execution rates by incorporating general (i.e., non-exponential) distributions. Applying product-line engineering methods, we consider a family of models generated by a core that evolves into concrete instances by applying simple delta operations affecting both the topology and the model's parameters. State explosion is tackled by turning to a scalable approximation based on ordinary differential equations. The entire model space is analyzed in a family-based fashion, i.e., at once using an efficient symbolic solution of a super-model that subsumes every concrete instance. Extensive numerical tests show that this is orders of magnitude faster than a naive instance-by-instance analysis.

Variant Process Algebra is designed for the formal behavioral modeling of software variation, as arises, for instance, in software product line engineering. Process terms are labelled with the sets of variants, i.e., specific products, where they are enabled. A multi-modal operational semantics enables two compositional forms of reasoning. The first one is concerned with relating the behavior of a variant to the whole family. The second notion relates variants between each other, for instance to be able to formally capture the intuitive idea that a variant is a conservative extension of another, in the sense that it adds more behavior without breaking any existing one. Sufficient conditions are given to establish such a relation statically, by means of syntactic checks on process terms.

When performance characteristics are taken into account in a software design, models can be used to identify optimal configurations of the system's parameters. Unfortunately, for realistic scenarios, the cost of the optimization is typically high, leading to computational difficulties in the exploration of large parameter spaces. This paper proposes an approach to provably exact parameter-space pruning for a class of models of large-scale software systems analyzed with fluid techniques, efficient and scalable deterministic approximations of massively parallel stochastic models. We present a result of monotonicity of fluid solutions with respect to the model parameters, and employ it in the context of optimization programs with evolutionary algorithms by discarding candidate configurations a priori, i.e., without ever solving them, whenever they are proven to give lower fitness than other configurations. An extensive numerical validation shows that this approach yields an average twofold runtime speed-up compared to a baseline optimization algorithm that does not exploit monotonicity. Furthermore, we find that the optimal configuration is within a few percent from the true one obtained by stochastic simulation, whose solution is however orders of magnitude more expensive.

Fluid models have gained popularity in the performance modeling of computing systems and communication networks. When the model under study consists of many different types of agents, the size of the associated system of ordinary differential equations (ODEs) increases with the number of types, making the analysis more difficult. We study this problem for a class of models where heterogeneity is expressed as a perturbation of certain parameters of the ODE vector field. We provide an a-priori bound that relates the solutions of the original, heterogenous model with that of an ODE system of smaller size which arises from aggregating system variables concerning different types of agents. By showing that this bound grows linearly with the intensity of the perturbation, we provide a formal justification to the intuitive possibility of neglecting small differences in agents' behavior as a means to reducing the dimensionality of the original system.

Layered queueing networks are a useful tool for the performance modeling and prediction of software systems that exhibit complex characteristics such as multiple tiers of service, fork/join interactions, and asynchronous communication. These features generally result in nonproduct form behavior for which particularly efficient approximations based on mean value analysis (MVA) have been devised. This paper reconsiders the accuracy of such techniques by providing an interpretation of layered queueing networks as fluid models. Mediated by an automatic translation into a stochastic process algebra, PEPA, a network is associated with a set of ordinary differential equations (ODEs) whose size is insensitive to the population levels in the system under consideration. A substantial numerical assessment demonstrates that this approach significantly improves the quality of the approximation for typical performance indices such as utilization, throughput, and response time. Furthermore, backed by established theoretical results of asymptotic convergence, the error trend shows monotonic decrease with larger population sizes-a behavior which is found to be in sharp contrast with that of approximate mean value analysis, which instead tends to increase.

In software engineering, design patterns are commonly used and represent robust solution templates to frequently occurring problems in software design and implementation. In this paper, we consider performance simulation for two design patterns for processing of parallel messaging. We develop continuous-time Markov chain models of two commonly used design patterns, Half-Sync/Half-Async and Leader/Followers, for their performance evaluation in multicore machines. We propose a unified modeling approach which contemplates a detailed description of the application-level logic and abstracts away from operating system calls and complex locking and networking application programming interfaces. By means of a validation study against implementations on a 16-core machine, we show that the models accurately predict peak throughputs and variation trends with increasing concurrency levels for a wide range of message processing workloads. We also discuss the limits of our models when memory-level internal contention is not captured.

This paper presents an analytical model for the performance prediction of queueing networks with batch services and batch arrivals, related to the fluid limit of a suitable single-parameter sequence of continuous-time Markov chains and interpreted as the deterministic approximation of the average behaviour of the stochastic process. Notably, the underlying system of ordinary differential equations exhibits discontinuities in the right-hand sides, which however are proven to yield a meaningful solution. A substantial numerical assessment is used to study the quality of the approximation and shows very good accuracy in networks with large job populations.

In this paper we report on progress in the use of stochastic process algebras for representing systems which contain many replications of components such as clients, servers and devices. Such systems have traditionally been difficult to analyse even when using high-level models because of the need to represent the vast range of their potential behaviour. Models of concurrent systems with many components very quickly exceed the storage capacity of computing devices even when efficient data structures are used to minimize the cost of representing each state. Here, we show how population-based models that make use of a continuous approximation of the discrete behaviour can be used to efficiently analyse the temporal behaviour of very large systems via their collective dynamics. This approach enables modellers to study problems that cannot be tackled with traditional discrete-state techniques such as continuous-time Markov chains.

Reasoning about the performance of models of software systems typically entails the derivation of metrics such as throughput, utilization, and response time. If the model is a Markov chain, these are expressed as real functions of the chain, called reward models. The computational complexity of reward-based metrics is of the same order as the solution of the Markov chain, making the analysis infeasible when evaluating large-scale systems. In the context of the stochastic process algebra PEPA, the underlying continuous-time Markov chain has been shown to admit a deterministic (fluid) approximation as a solution of an ordinary differential equation, which effectively circumvents state-space explosion. This paper is concerned with approximating Markovian reward models for PEPA with fluid rewards, i.e., functions of the solution of the differential equation problem. It shows that (1) the Markovian reward models for typical metrics of performance enjoy asymptotic convergence to their fluid analogues, and that (2) via numerical tests, the approximation yields satisfactory accuracy in practice.

The exact performance analysis of large-scale software systems with discrete-state approaches is difficult because of the well-known problem of state-space explosion. This paper considers this problem with regard to the stochastic process algebra PEPA, presenting a deterministic approximation to the underlying Markov chain model based on ordinary differential equations. The accuracy of the approximation is assessed by means of a substantial case study of a distributed multithreaded application.

Studying the existence of product forms of performance models described with compositional techniques is of central importance since this may lead to particularly efficient solution methods. This paper considers a class of models in the stochastic process algebra PEPA which do not enjoy the exact product form solutions available in the literature. However, they can be interpreted as queueing networks with service vacations and multiple resource possession, which have been shown to admit accurate analytical approximations based on mean value analysis. Special attention is devoted to situations where the use of the competing approximate method based on ordinary differential equations may be questionable due to the presence of components with few replicas.

We propose a model-based approach to analysing the performance of mobile applications where physical mobility and state changes are modelled by graph transformations from which a model in the Performance Evaluation Process Algebra (PEPA) is derived. To fight scalability problems with state space generation we adopt a modular solution where the graph transformation system is decomposed into views, for which labelled transition systems (LTS) are generated separately and later synchronised in PEPA. We demonstrate that the result of this modular analysis is equivalent to that of the monolithic approach and evaluate practicality and scalability by means of a case study.

In this paper we propose a Markovian model of BitTorrent. Unlike already developed works which capture demographic dynamics, it focuses on the behavior of individual peers. To this end, we center our attention on a generic peer, called tagged peer (TP); for each possible logical state of a BT peer-to-peer connection maintained by the TP, we consider a stochastic process which counts the number of such links, and characterize them according to their state. Validation is carried out and steady-state analysis is performed in order to illustrate how performance evaluation can be extracted from our model

BitTorrent is today one of the largest P2P systems which allows file sharing for Internet users. Very little effort has been dedicated to this target up to now. The goal of this paper is to develop an analytical model of a free-rider in a BitTorrent network. Unlike previous analytical models which capture the behavior of the network as a whole, the proposed model is able to analyze the performance from the user perspective. The model is applied to a case study to evaluate performance in a real case, and to obtain some insights into the influence of BitTorrent parameters on system performance.