8,726 research outputs found
Fluid analysis of spatio-temporal properties of agents in a population model
No full textWe consider large stochastic population models in which heterogeneous agents are interacting locally and moving in space. These models are very common, e.g. in the context of mobile wireless networks, crowd dynamics, traffic management, but they are typically very hard to analyze, even when space is discretized in a grid. Here we consider individual agents and look at their properties, e.g. quality of service metrics in mobile networks. Leveraging recent results on the combination of stochastic approximation with formal verification, and of fluid approximation of spatio-temporal population processes, we devise a novel mean-field based approach to check such behaviors, which requires the solution of a low-dimensional set of Partial Differential Equation, which is shown to be much faster than simulation. We prove the correctness of the method and validate it on a mobile peer-to-peer network example
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
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
Accompanying material for 'Lumpability for Uncertain Continuous-Time Markov Chains'
No full textThis is the accompanying material for the draft
Luca Cardelli, Radu Grosu, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Lumpability for Uncertain Continuous-time Markov Chains, submitted at TACAS 2020.
This archive contains information on how to replicate the experiments presented in the draft.</p
Forward and Backward Bisimulations for Chemical Reaction Networks
Full text linkWe present two quantitative behavioral equivalences over species of a chemical reaction network(CRN) with semantics based on ordinary differential equations.Forward CRN bisimulationiden-tifies a partition where each equivalence class represents the exact sum of the concentrations ofthe species belonging to that class. Backward CRN bisimulationrelates species that have theidentical solutions at all time points when starting from the same initial conditions. Both notionscan 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 bisimulationsin polynomial time. Further, we give algorithms to compute quotient CRNs induced by a bisim-ulation. As an application, we find significant reductions in a number of models of biologicalprocesses from the literature. In two cases we allow the analysis of benchmark models whichwould be otherwise intractable due to their memory requirements
Reducing Boolean Networks with Backward Boolean Equivalence
Full text linkBoolean Networks (BNs) are established models to qualitatively describe biological systems. The analysis of BNs might be infeasible for medium to large BNs due to the state-space explosion problem. We propose a novel reduction technique called Backward Boolean Equivalence (BBE), which preserves some properties of interest of BNs. In particular, reduced BNs provide a compact representation by grouping variables that, if initialized equally, are always updated equally. The resulting reduced state space is a subset of the original one, restricted to identical initialization of grouped variables. The corresponding trajectories of the original BN can be exactly restored. We show the effectiveness of BBE by performing a large-scale validation on the whole GINsim BN repository. In selected cases, we show how our method enables analyses that would be otherwise intractable. Our method complements, and can be combined with, other reduction methods found in the literature
EGAC: a genetic algorithm to compare chemical reaction networks
No full textDiscovering 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
Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods
Full text linkWe 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
Exact maximal reduction of stochastic reaction networks by species lumping
Full text linkMOTIVATION: 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
Enseñanza de la escritura de Max Aub: comprensión y memoria
No full textEste texto analiza a obra testimonial de Max Aub sobre su experiencia en los campos de concentración en Francia desde una perspectiva de discursos comparados. Para destacar las estrategias de la escritura del autor recuperables por otros proyectos discursivos que persigan la sensibilización y la denuncia a través del cruce entre la comunicación y la éticaThis text analyses the testimonial work of Max Aub about his experience in the French concentration camps in France from comparative discourses approach. It emphasizes the writing strategies used by the author useful for other awareness and denounce discourses through the dialogue among communication and ethic
- …
