Search

We introduce a novel learning-based approach to synthesize safe and robust controllers for autonomous Cyber-Physical Systems and, at the same time, to generate challenging tests. This procedure combines formal methods for model verification with Generative Adversarial Networks. The method learns two Neural Networks: the first one aims at generating troubling scenarios for the controller, while the second one aims at enforcing the safety constraints. We test the proposed method on a variety of case studies.

In this paper we present a class of nested automata for the modelling of performance, availability, and reliability of software systems with hierarchical structure, which we call systems of systems . Quantitative modelling provides valuable insight into the dynamic behaviour of software systems, allowing non-functional properties such as performance, dependability and availability to be assessed. However, the complexity of many systems challenges the feasibility of this approach as the required mathematical models grow too large to afford computationally efficient solution. In recent years it has been found that in some cases a fluid, or mean field, approximation can provide very good estimates whilst dramatically reducing the computational cost. The systems of systems which we propose are hierarchically arranged automata in which influence may be exerted between siblings, between parents and children, and even from children to parents, allowing a wide range of complex dynamics to be captured. We show that, under mild conditions, systems of systems can be equipped with fluid approximation models which are several orders of magnitude more efficient to run than explicit state representations, whilst providing excellent estimates of performability measures. This is a significant extension of previous fluid approximation results, with valuable applications for software performance modelling. [ABSTRACT FROM AUTHOR]

We draw the basic lines for an approach to build mathematical and programmablenetwork models, to be applied in the study of populations of cancer-cells at different stages of disease development. The methodology we propose uses a stochastic Concurrent Constraint Programming language, a flexible stochastic modelling language employed to code networks of agents. It is applied to (and partially motivated by) the study of differently characterized populations of prostate cancer cells. In particular, we prove how our method is suitable to systematically reconstruct and compare different mathematical models of prostate cancer growth—together with interactions with different kinds of hormone therapy—at different levels of refinement. Moreover, we show our technique at work in analysing the nature of noise and in the possible presence of competing mechanisms in the models proposed.We draw the basic lines for an approach to build mathematical and programmablenetwork models, to be applied in the study of populations of cancer-cells at different stages of disease development. The methodology we propose uses a stochastic Concurrent Constraint Programming language, a flexible stochastic modelling language employed to code networks of agents. It is applied to (and partially motivated by) the study of differently characterized populations of prostate cancer cells. In particular, we prove how our method is suitable to systematically reconstruct and compare different mathematical models of prostate cancer growth—together with interactions with different kinds of hormone therapy—at different levels of refinement. Moreover, we show our technique at work in analysing the nature of noise and in the possible presence of competing mechanisms in the models proposed.

We consider an asynchronous all optical packet switch (OPS) where each link consists of N wavelength channels and a pool of C ≤ N full range tunable wavelength converters. Under the assumption of Poisson arrivals with rate λ (per wavelength channel) and exponential packet lengths, we determine a simple closed-form expression for the limit of the loss probabilities Ploss(N) as N tends to infinity (while the load and conversion ratio σ=C/N remains fixed). More specifically, for σ ≤ λ2 the loss probability tends to (λ2-σ)/λ(1+λ), while for σ > λ2 the loss tends to zero. We also prove an insensitivity result when the exponential packet lengths are replaced by certain classes of phase-type distributions. A key feature of the dynamical system (i.e., set of ODEs) that describes the limit behavior of this OPS switch, is that its right-hand side is discontinuous. To prove the convergence, we therefore had to generalize some existing result to the setting of piece-wise smooth dynamical systems.

Abstract: In biological phenomena like osmosis, the rate of flow of water molecules in or out of biological compartments depends on the solute concentration and on other forces, like hydrostatic pressure. A similar example is the passive transport of ions in and out the cell membrane. In this paper, we address the problem of faithfully modelling these kind of phenomena with an adequate process calculus. We enhance the ambient calculus stochastic semantics with functional rates, which are calculated by taking into account the volume of ambients and the surrounding environment. A model of osmosis in plant cells will be used as an example to show the new features of our calculus. [Copyright &y& Elsevier]

Abstract: We compare the hybrid, stochastic, and differential semantics for stochastic Concurrent Constraint Programming, focussing on the exhibited behavior of models and their robustness. By investigating in detail two case studies, a circadian clock model and the Repressilator, we comment on the effect of the introduction of a limited amount of discreteness in the description of biological systems with hybrid automata. Experimental evidence suggests that discreteness increases robustness of the models. [Copyright &y& Elsevier]

Abstract: We explore the relation between the stochastic semantic associated to stochastic Concurrent Constrain Programming (sCCP) and its fluid-flow approximation. Writing the master equation for a sCCP model, we can show that the fluid flow equation is a first-order approximation of the true equation for the average. Moreover, we introduce a second-order correction and first-order equations for the variance and the covariance. [Copyright &y& Elsevier]

Abstract: HYPE is a process algebra developed to model hybrid systems – systems that show both continuous and discrete behaviour. It is novel because it allows for the modelling of individual flows which means that subcomponents can be modelled in terms of these flows and do not need to be described monolithically. Biological systems display discrete behaviour inherently, but modellers may choose to model systems in a hybrid fashion, often to deal with differences in scale. We demonstrate how HYPE can be used to model the Repressilator. [Copyright &y& Elsevier]

Abstract: We tackle the problem of relating models of systems (mainly biological systems) based on stochastic process algebras (SPA) with models based on differential equations. We define a syntactic procedure that translates programs written in stochastic Concurrent Constraint Programming (sCCP) into a set of Ordinary Differential Equations (ODE), and also the inverse procedure translating ODE''s into sCCP programs. For the class of biochemical reactions, we show that the translation is correct w.r.t. the intended rate semantics of the models. Finally, we show that the translation does not generally preserve the dynamical behavior, giving a list of open research problems in this direction. [Copyright &y& Elsevier]

AbstractWe re-take a coding-theoretic notion which goes back to Cl. Shannon: codeword distinguishability. This notion is standard in zero-error information theory, but its bearing is definitely wider and it may help to better understand new forms of coding, e.g., DNA word design. In our approach, the underlying decoding principle is very simple and very general: one decodes by trying to minimise the diversity (in the simplest case the Hamming distance) between a codeword and the output sequence observed at the end of the noisy transmission channel. Symmetrically and equivalently, one may use maximum-similarity decoders and codeword confusabilities. The operational meaning of codeword distinguishability is made clear by a reliability criterion, which generalises the well-known criterion on minimum Hamming distances for error-correction codes. We investigate the formal properties of distinguishabilities versus diversities; these two notions are deeply related, and yet essentially different. An encoding theorem is put forward; as a case study, we examine a channel of cryptographic interest.

Abstract: We present a stochastic version of Concurrent Constraint Programming (CCP), where we associate a rate to each basic instruction that interacts with the constraint store. We give an operational semantic that can be provided either with a discrete or a continuous model of time. The notion of observables is discussed, both for the discrete and the continuous version, and a connection between the two is given. Finally, a possible application for modeling biological networks is presented. [Copyright &y& Elsevier]

Mean field approximation is a powerful tool to study the performance of large stochastic systems that is known to be exact as the system's size N goes to infinity. Recently, it has been shown that, when one wants to compute expected performance metric in steady-state, mean field approximation can be made more accurate by adding a term in 1/N to the original approximation. This is called the refined mean field approximation in [7]. In this paper, we show how to obtain the same result for the transient regime and we provide a further refinement by expanding the term in 1/N2 (both for transient and steady-state regime). Our derivations are inspired by moment-closure approximation. We provide a number of examples that show this new approximation is usable in practice for systems with up to a few tens of dimensions.