1,721,076 research outputs found
Reproducibility Report for the Paper: Efficient Non-Blocking Event Management for Speculative Parallel Discrete Event Simulation
No full textThis is a report on the reproducibility of the experiments in the paper "Efficient Non-Blocking Event Management for Speculative Parallel Discrete Event Simulation"presented at the 38th ACM SIGSIM conference on Principles of Advanced Discrete Simulation (PADS'24). The artifact got badges Artifacts Evaluated - Functional v1.1, Artifacts Available v1.1, and Results Reproduced v1.1. The Artifacts Evaluated Functional badge has been assigned since the artifact associated with the research is documented, consistent, complete, exercisable, and includes evidence of verification and validation. The Artifacts Available badge has been given since the authors made the artifact permanently available. Finally, the Result Replicated badge has been assigned because the results shown in the paper have been reproduced by persons other than the authors, using artifacts provided by the authors
Process Mining meets Statistical Model Checking: Towards a Novel Approach to Model Validation and Enhancement
No full textWe propose a novel research line integrating Statistical Model Checking (SMC), a family of simulation-based analysis techniques from quantitative formal methods, with Process Mining (PM), a collection of data-driven process-oriented techniques. SMC and PM are complementary. SMC focuses on performing the right number of simulations to obtain statistically-reliable estimations (e.g., the probability of success of an attack). PM focuses on reconstructing a model of a system using logs of its traces. Nevertheless, both approaches aim at providing evidence of issues/guarantees of the system, and at proposing enhancements. We aim at enriching SMC by explaining why it produced specific estimates. This might help, e.g., identifying issues in the model (validation) or suggesting improvements (enhancement). Given that SMC uses statistics to decide what is the correct number of simulations (or traces), we avoid by-construction the complex issue of under-representation of system behavior in the logs crucial to many PM exercises. This work-in-progress paper demonstrates the proposed methodology and its usefulness using a simple example from the security threat modeling domain. We show how PM helps highlighting both mistakes in the model, and possibilities for improvement.<br/
A large-scale assessment of exact lumping of quantitative models in the BioModels repository
Full text linkChemical reaction networks are a popular formalism for modeling biological processes which supports both a deterministic and a stochastic interpretation based on ordinary differential equations and continuous-time Markov chains, respectively. In most cases, these models do not enjoy analytical solution, thus typically requiring expensive computational methods based on numerical solvers or stochastic simulations. Exact model reduction techniques can be used as an aid to lower the analysis cost by providing reduced networks that preserve the dynamics of interest to the modeler without incurring any approximation error. We hereby consider a family of techniques for both deterministic and stochastic networks which are based on equivalence relations over the species in the network, leading to a coarse graining which provides the exact aggregate time-course evolution for each equivalence class. We present a large-scale empirical assessment on the BioModels repository by measuring their compression capability over 579 models. Through a number of selected case studies, we also show their ability in yielding physically interpretable reductions that can reveal dynamical patterns of the bio-molecular processes under consideration, independently of the values of the kinetic parameters used in the models.</p
White-Box Validation of Collective Adaptive Systems by Statistical Model Checking and Process Mining
No full textModeling and analyzing collective adaptive systems with heterogeneous components poses challenges to language designers, software engineers, and computer scientists interested in the formal verification of the modeled systems. This requires the integration of computational, reasoning, and analysis tools, but also of techniques to validate and shed light on the actual behavior described by a model. We build on a methodology built in collaboration with Rocco De Nicola, based on his influential contributions in the modeling and programming of distributed and adaptive systems. Such methodology allows to model and analyze collective adaptive systems equipped with reasoning capabilities. It combines SCEL, a language for programming collective adaptive systems, with Pirlo, a reasoner that can enrich agents with reasoning capabilities, and MultiVeStA, a statistical model checker that can analyze the obtained models by simulating them. Here, we further enrich this methodology with techniques from process-oriented data science, and in particular process mining, to ease the validation and debugging of such models. This follows recent proposals from the literature that validate models by explaining graphically the behaviors observed by a statistical model checker. We demonstrate our approach by considering a simple collision-avoidance robotic scenario where a group of robots moves in an arena while aiming at minimizing the number of collisions
Improved estimations of stochastic chemical kinetics by finite-state expansion
Full text linkStochastic reaction networks are a fundamental model to describe interactions between species where random fluctuations are relevant. The master equation provides the evolution of the probability distribution across the discrete state space consisting of vectors of population counts for each species. However, since its exact solution is often elusive, several analytical approximations have been proposed. The deterministic rate equation (DRE) gives a macroscopic approximation as a compact system of differential equations that estimate the average populations for each species, but it may be inaccurate in the case of nonlinear interaction dynamics. Here we propose finite-state expansion (FSE), an analytical method mediating between the microscopic and the macroscopic interpretations of a stochastic reaction network by coupling the master equation dynamics of a chosen subset of the discrete state space with the mean population dynamics of the DRE. An algorithm translates a network into an expanded one where each discrete state is represented as a further distinct species. This translation exactly preserves the stochastic dynamics, but the DRE of the expanded network can be interpreted as a correction to the original one. The effectiveness of FSE is demonstrated in models that challenge state-of-the-art techniques due to intrinsic noise, multi-scale populations and multi-stability. </p
MultiVeStA: Statistical Analysis of Economic Agent-Based Models by Statistical Model Checking
No full textWe overview our recent work on the statistical analysis of simulation models and, especially, economic agent-based models (ABMs). We present a redesign of MultiVeStA, a fully automated and model-agnostic toolkit that can be integrated with existing simulators to inspect simulations and perform counterfactual analysis. Our approach: (i) is easy-to-use by the modeler, (ii) improves reproducibility of results, (iii) optimizes running time given the modeler’s machine, (iv) automatically chooses the number of required simulations and simulation steps to reach user-specified statistical confidence, and (v) automatically performs a variety of statistical tests. In particular, our framework is designed to distinguish the transient dynamics of the model from its steady-state behavior (if any), estimate properties of the model in both “phases”, and provide indications on the ergodic (or non-ergodic) nature of the simulated processes – which, in turns allows one to gauge the reliability of a steady-state analysis. Estimates are equipped with statistical guarantees, allowing for robust comparisons across computational experiments. This allows us to obtain new insights from models from the literature, and to fix some erroneous conclusions on them.</p
Automated and Distributed Statistical Analysis of Economic Agent-Based Models
No full textWe propose a novel approach to the statistical analysis of stochastic
simulation models and, especially, agent-based models (ABMs). Our main goal is
to provide fully automated, model-independent and tool-supported techniques and
algorithms to inspect simulations and perform counterfactual analysis. Our
approach: (i) is easy-to-use by the modeller, (ii) improves reproducibility of
results, (iii) optimizes running time given the modeller's machine, (iv)
automatically chooses the number of required simulations and simulation steps
to reach user-specified statistical confidence, and (v) automates a variety of
statistical tests. In particular, our techniques are designed to distinguish
the transient dynamics of the model from its steady-state behaviour (if any),
estimate properties in both 'phases', and provide indications on the
(non-)ergodic nature of the simulated processes - which, in turn, allows one to
gauge the reliability of a steady-state analysis. Estimates are equipped with
statistical guarantees, allowing for robust comparisons across computational
experiments. To demonstrate the effectiveness of our approach, we apply it to
two models from the literature: a large-scale macro-financial ABM and a small
scale prediction market model. Compared to prior analyses of these models, we
obtain new insights and we are able to identify and fix some erroneous
conclusions
Differential Equivalence for Linear Differential Algebraic Equations
Full text linkDifferential-algebraic equations (DAEs) are a widespread dynamical model that describes continuously evolving quantities defined with differential equations, subject to constraints expressed through algebraic relationships. As such, DAEs arise in many fields ranging from physics, chemistry, and engineering. In this paper we focus on linear DAEs, and develop a theory for their minimization up to an equivalence relation. We present differential equivalence, which relates DAE variables that have equal solutions at all time points (thus requiring them to start with equal initial conditions) and extends the line of research on bisimulations developed for Markov chains and ordinary differential equations. We apply our results to the electrical engineering domain, showing that differential equivalence can explain invariances in certain networks as well as analyze DAEs which could not be originally treated due to their size
Formal Approaches for Modeling and Analysis of Business Process Collaborations
Full text linkThe paper introduces a general framework for handling BPMN graphical (semi-formal) models used for describing business process collaborations. It offers a systematic and architecturally comprehensive synthesis of the authors’ prior work on the direct formalization of business process collaborations, the specification of their properties, and their verification and animation. The results exposed in this paper (and many others, indeed) have a direct “causal link” with what the authors learned collaborating with Rocco De Nicola; methodologies and techniques to the specification and design of complex systems and one of Rocco’s scientific career “constants”: formality
- …
