Abstract We investigate the behaviour of population models, specified in stochastic Concurrent Constraint Programming (sCCP). In particular, we focus on models from which we can define a semantics both in terms of Continuous Time Markov Chains (CTMC) and in terms of Stochastic Hybrid Systems, in which some populations are approximated continuously, while others are kept discrete. We will prove the correctness of the hybrid semantics from the point of view of the limiting behaviour of a sequence of models for increasing population size. More specifically, we prove that, under suitable regularity conditions, the sequence of \{CTMC\} constructed from sCCP programs for increasing population size converges to the hybrid system constructed by means of the hybrid semantics. We investigate in particular what happens for sCCP models in which some transitions are guarded by boolean predicates or in the presence of instantaneous transitions.

}, keywords = {fluid approximation, Mean field, stochastic concurrent constraint programming, stochastic hybrid systems, Stochastic process algebras, Weak convergence}, issn = {0890-5401}, doi = {http://dx.doi.org/10.1016/j.ic.2015.12.001}, url = {http://www.sciencedirect.com/science/article/pii/S0890540115001297}, author = {Luca Bortolussi} } @article {315, title = {Smoothed model checking for uncertain Continuous-Time Markov Chains}, journal = {Information and Computation}, year = {In Press}, pages = {-}, abstract = {Abstract We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters under mild conditions. This enables us to devise a novel Bayesian statistical algorithm which performs model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on non-trivial case studies show that the approach is accurate and considerably faster than naive parameter exploration with standard statistical model checking methods.

}, keywords = {Continuous-Time Markov Chains, Gaussian Processes, model checking, Uncertainty}, issn = {0890-5401}, doi = {http://dx.doi.org/10.1016/j.ic.2016.01.004}, url = {http://www.sciencedirect.com/science/article/pii/S0890540116000055}, author = {Luca Bortolussi and Dimitrios Milios and Guido Sanguinetti} } @conference { 11368_2856195, title = {CARMA: Collective Adaptive Resource-sharing Markovian Agents}, booktitle = {Quantitative Aspects of Programming Languages and Systems (QAPL)}, volume = {194}, year = {2015}, pages = {16{\textendash}31}, publisher = {Open Publishing}, organization = {Open Publishing}, edition = {EPTCS}, abstract = {In this paper we present CARMA, a language recently defined to support specification and analysis of collective adaptive systems. CARMA is a stochastic process algebra equipped with linguistic constructs specifically developed for modelling and programming systems that can operate in open-ended and unpredictable environments. This class of systems is typically composed of a huge number of interacting agents that dynamically adjust and combine their behaviour to achieve specific goals. A CARMA model, termed a collective, consists of a set of components, each of which exhibits a set of attributes. To model dynamic aggregations, which are sometimes referred to as ensembles, CARMA provides communication primitives that are based on predicates over the exhibited attributes. These predicates are used to select the participants in a communication. Two communication mechanisms are provided in the CARMA language: multicast-based and unicast-based. In this paper, we first introduce the basic principles of CARMA and then we show how our language can be used to support specification with a simple but illustrative example of a socio-technical collective adaptive system.

}, keywords = {Attribute-based Process Algebras, Collective Adaptive Systems}, doi = {10.4204/EPTCS.194.2}, url = {http://arxiv.org/abs/1509.08560}, author = {Bortolussi, Luca and De Nicola, Rocco and Galpin, Vashti and Gilmore, Stephen and Hillston, Jane and Latella, Diego and Loreti, Michele and Massink, Mieke} } @article {bortolussi2015coding, title = {Coding Theory: A General Framework and Two Inverse Problems}, journal = {Fundamenta Informaticae}, volume = {141}, number = {4}, year = {2015}, pages = {297{\textendash}310}, publisher = {IOS Press}, abstract = {We put forward an ample framework for coding based on upper probabilities, or more generally on normalized monotone set-measures, and model accordingly noisy transmission channels and decoding errors. Two inverse problems are considered. In the first case, a decoder is given and one looks for channels of a specified family over which that decoder would work properly. In the second and more ambitious case, it is codes which are given, and one looks for channels over which those codes would ensure the required error correction capabilities. Upper probabilities allow for a solution of the two inverse problems in the case of usual codes based on checking Hamming distances between codewords: one can equivalently check suitable upper probabilities of the decoding errors. This soon extends to {\textquotedblleft}odd{\textquotedblright} codeword distances for DNA strings as used in DNA word design, where instead, as we prove, not even the first unassuming inverse problem admits of a solution if one insists on channel models based on {\textquotedblleft}usual{\textquotedblright} probabilities.

}, doi = {10.3233/FI-2015-1277}, author = {Bortolussi, Luca and Dinu, Liviu P and Franzoi, Laura and Sgarro, Andrea} } @conference { 11368_2856198, title = {Efficient Checking of Individual Rewards Properties in Markov Population Models}, booktitle = {Quantitative Aspects of Programming Languages and Systems (QAPL)}, volume = {194}, year = {2015}, pages = {32{\textendash}47}, publisher = {Open Publishing}, organization = {Open Publishing}, edition = {EPTCS}, abstract = {In recent years fluid approaches to the analysis of Markov populations models have been demonstrated to have great pragmatic value. Initially developed to estimate the behaviour of the system in terms of the expected values of population counts, the fluid approach has subsequently been extended to more sophisticated interrogations of models through its embedding within model checking procedures. In this paper we extend recent work on checking CSL properties of individual agents within a Markovian population model, to consider the checking of properties which incorporate rewards.

}, keywords = {Markov population models, Rewards, Stochastic Approximation, Stochastic model checking}, doi = {10.4204/EPTCS.194.3}, author = {Bortolussi, Luca and Hillston, Jane} } @proceedings {bortolussi2015efficient, title = {Efficient stochastic simulation of systems with multiple time scales via statistical abstraction}, volume = {9308}, year = {2015}, pages = {40{\textendash}51}, publisher = {Springer International Publishing}, edition = {LNCS}, abstract = {Stiffness in chemical reaction systems is a frequently encountered computational problem, arising when different reactions in the system take place at different time-scales. Computational savings can be obtained under time-scale separation. Assuming that the system can be partitioned into slow- and fast- equilibrating subsystems, it is then possible to efficiently simulate the slow subsystem only, provided that the corresponding kinetic laws have been modified so that they reflect their dependency on the fast system. We show that the rate expectation with respect to the fast subsystem{\textquoteright}s steady-state is a continuous function of the state of the slow system. We exploit this result to construct an analytic representation of the modified rate functions via statistical modelling, which can be used to simulate the slow system in isolation. The computational savings of our approach are demonstrated in a number of non-trivial examples of stiff systems.

}, doi = {10.1007/978-3-319-23401-4_5}, author = {Bortolussi, Luca and Milios, Dimitrios and Sanguinetti, Guido} } @conference {bortolussi2015fluid, title = {Fluid Model Checking of Timed Properties}, booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS)}, volume = {9268}, year = {2015}, pages = {172{\textendash}188}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, edition = {LNCS}, abstract = {We address the problem of verifying timed properties of Markovian models of large populations of interacting agents, modelled as finite state automata. In particular, we focus on time-bounded properties of (random) individual agents specified by Deterministic Timed Automata (DTA) endowed with a single clock. Exploiting ideas from fluid approximation, we estimate the satisfaction probability of the DTA properties by reducing it to the computation of the transient probability of a subclass of Time-Inhomogeneous Markov Renewal Processes with exponentially and deterministically-timed transitions, and a small state space. For this subclass of models, we show how to derive a set of Delay Differential Equations (DDE), whose numerical solution provides a fast and accurate estimate of the satisfaction probability. In the paper, we also prove the asymptotic convergence of the approach, and exemplify the method on a simple epidemic spreading model. Finally, we also show how to construct a system of DDEs to efficiently approximate the average number of agents that satisfy the DTA specification.

}, keywords = {Delay differential equations; Deterministic timed automata, fluid approximation, Fluid model checking, Stochastic model checking, Time-inhomogeneous markov renewal processes}, doi = {10.1007/978-3-319-22975-1_12}, author = {Bortolussi, Luca and Lanciani, Roberta} } @conference {292, title = {Fluid Performability Analysis of Nested Automata Models}, booktitle = {Practical Application of Stochastic Modelling (PASM14)}, volume = {310}, year = {2015}, pages = {27{\textendash}47}, publisher = {Elsevier}, organization = {Elsevier}, edition = {Electronic Notes in Theoretical Computer Science}, address = {Newcastle-upon-Tyne, UK.}, abstract = {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.

}, keywords = {fluid approximation, software performance modelling, Systems of systems}, doi = {10.1016/j.entcs.2014.12.011}, url = {http://www.sciencedirect.com/science/article/pii/S1571066114000954}, author = {Bortolussi, Luca and Hillston, Jane and Tribastone, Mirco} } @article {bodei2015impact, title = {On the impact of discreteness and abstractions on modelling noise in gene regulatory networks}, journal = {Computational biology and chemistry}, volume = {56}, year = {2015}, pages = {98{\textendash}108}, publisher = {Elsevier}, abstract = {In this paper, we explore the impact of different forms of model abstraction and the role of discreteness on the dynamical behaviour of a simple model of gene regulation where a transcriptional repressor negatively regulates its own expression. We first investigate the relation between a minimal set of parameters and the system dynamics in a purely discrete stochastic framework, with the twofold purpose of providing an intuitive explanation of the different behavioural patterns exhibited and of identifying the main sources of noise. Then, we explore the effect of combining hybrid approaches and quasi-steady state approximations on model behaviour (and simulation time), to understand to what extent dynamics and quantitative features such as noise intensity can be preserved.

}, keywords = {Discrete modeling, Gene regulatory networks, Hybrid system, Quasi-steady state approximation, Stochastic Noise}, doi = {10.1016/j.compbiolchem.2015.04.004}, author = {Bodei, Chiara and Bortolussi, Luca and Chiarugi, Davide and Guerriero, Maria Luisa and Policriti, Alberto and Romanel, Alessandro} } @article {11368_2848518, title = {Learning and designing stochastic processes from logical constraints}, journal = {LOGICAL METHODS IN COMPUTER SCIENCE}, volume = {11}, year = {2015}, pages = {1{\textendash}24}, abstract = {Stochastic processes offer a flexible mathematical formalism to model and reason about systems. Most analysis tools, however, start from the premises that models are fully specified, so that any parameters controlling the system{\textquoteright}s dynamics must be known exactly. As this is seldom the case, many methods have been devised over the last decade to infer (learn) such parameters from observations of the state of the system. In this paper, we depart from this approach by assuming that our observations are {it qualitative} properties encoded as satisfaction of linear temporal logic formulae, as opposed to quantitative observations of the state of the system. An important feature of this approach is that it unifies naturally the system identification and the system design problems, where the properties, instead of observations, represent requirements to be satisfied. We develop a principled statistical estimation procedure based on maximising the likelihood of the system{\textquoteright}s parameters, using recent ideas from statistical machine learning. We demonstrate the efficacy and broad applicability of our method on a range of simple but non-trivial examples, including rumour spreading in social networks and hybrid models of gene regulation.

}, keywords = {Computer Science (all), Machine Learning, Parameter Synthesis, Statistical Model Checking, Stochastic modelling, Temporal logics, Theoretical Computer Science}, doi = {10.2168/LMCS-11(2:3)2015}, url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1519\&layout=abstract}, author = {Bortolussi, Luca and Sanguinetti, Guido} } @conference {bortolussi2015machine, title = {Machine Learning Methods in Statistical Model Checking and System Design-Tutorial}, booktitle = {Runtime Verification (RV)}, volume = {9333}, year = {2015}, pages = {323{\textendash}341}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, edition = {LNCS}, abstract = {Recent research has seen an increasingly fertile convergence of ideas from machine learning and formal modelling. Here we review some recently introduced methodologies for model checking and system design/parameter synthesis for logical properties against stochastic dynamical models. The crucial insight is a regularity result which states that the satisfaction probability of a logical formula is a smooth function of the parameters of a CTMC. This enables us to select an appropriate class of functional priors for Bayesian model checking and system design. We give a tutorial introduction to the statistical concepts, as well as an illustrative case study which demonstrates the usage of a newly-released software tool, U-check, which implements these methodologies.

}, keywords = {Gaussian Processes, Machine Learning, Statistical Model Checking, System Design}, doi = {10.1007/978-3-319-23820-3_23}, author = {Bortolussi, Luca and Milios, Dimitrios and Sanguinetti, Guido} } @article {297, title = {Model checking single agent behaviours by fluid approximation}, journal = {Information and Computation}, volume = {242}, year = {2015}, pages = {183-226}, abstract = {In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC, which depends on the environment and on the other agents only through the solution of the fluid differential equation, and model check this process. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.

}, keywords = {fluid approximation, mean field approximation, reachability probability, Stochastic model checking, time-inhomogeneous Continuous Time Markov Chains}, issn = {0890-5401}, doi = {http://dx.doi.org/10.1016/j.ic.2015.03.002}, url = {http://www.sciencedirect.com/science/article/pii/S0890540115000176}, author = {Luca Bortolussi and Jane Hillston} } @conference {bock2015model, title = {Model-Based Whole-Genome Analysis of DNA Methylation Fidelity}, booktitle = {Hybrid Systems and Biology (HSB)}, volume = {9271}, year = {2015}, pages = {141{\textendash}155}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, edition = {LNCS}, abstract = {We consider the problem of understanding how DNA methylation fidelity, i.e. the preservation of methylated sites in the genome, varies across the genome and across different cell types. Our approach uses a stochastic model of DNA methylation across generations and trains it using data obtained through next generation sequencing. By training the model locally, i.e. learning its parameters based on observations in a specific genomic region, we can compare how DNA methylation fidelity varies genome-wide. In the paper, we focus on the computational challenges to scale parameter estimation to the whole-genome level, and present two methods to achieve this goal, one based on moment-based approximation and one based on simulation. We extensively tested our methods on synthetic data and on a first batch of experimental data.

}, keywords = {Branching processes, DNA methylation, Epigenomics, Next generation sequencing, Parameter estimation}, doi = {10.1007/978-3-319-26916-0_8}, author = {Bock, Christoph and Bortolussi, Luca and Kr{\"u}ger, Thilo and Mikeev, Linar and Wolf, Verena} } @conference {nenzi2015qualitative, title = {Qualitative and quantitative monitoring of spatio-temporal properties}, booktitle = {Runtime Verification (RV)}, volume = {9333}, year = {2015}, pages = {21{\textendash}37}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, edition = {LNCS}, abstract = {We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.

}, keywords = {Boolean semantics, Monitoring algorithms, Quantitative semantics, Signal spatio-temporal logic, Turing patterns, Weighted graphs}, doi = {10.1007/978-3-319-23820-3_2}, author = {Nenzi, Laura and Bortolussi, Luca and Ciancia, Vincenzo and Loreti, Michele and Massink, Mieke} } @conference { 11368_2861212, title = {Rule-Based Modelling and Simulation of Drug-Administration Policies}, booktitle = {Modeling and Simulation in Medicine Symposium (MSM 2015)}, year = {2015}, pages = {53{\textendash}60}, publisher = {Curran Associates, Inc.}, organization = {Curran Associates, Inc.}, abstract = {We investigate a model of drug administration in the con- text of a plaque-formation process responsible of Alzheimer{\textquoteright}s disease. This is a polymerisation process, best described by a rule-based model to counteract the intrinsic combinatorial explosion of the underlying re- action network. Furthermore, there is the additional complicancy of time- dependent rates, modelling the effect of drugs. In the paper, we provide a novel and efficient rejection-based simulation algorithm that samples exactly the trajectory space and apply it to study the efficacy of different drug administration policies.

}, keywords = {drug design, Rule based modelling, stochastic simulation, time-inhomogeneous models}, author = {Bortolussi, Luca and Kr{\"u}ger, Thilo and Wolf, Verena} } @conference {286, title = {Specifying and Monitoring Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic}, booktitle = {VALUETOOLS2014}, volume = {1}, year = {2015}, edition = {EAI ENDORSED TRANSACTIONS ON CLOUD SYSTEMS}, abstract = {We present an extension of the linear time, time-bounded, Signal Temporal Logic to describe spatio-temporal properties. We consider a discrete location/ patch-based representation of space, with a population of interacting agents evolving in each location and with agents migrating from one patch to another one. We provide both a boolean and a quantitative semantics to this logic. We then present monitoring algorithms to check the validity of a formula, or to compute its satisfaction (robustness) score, over a spatio-temporal trace, exploiting these routines to do statistical model checking of stochastic models. We illustrate the logic at work on an epidemic example, looking at the diffusion of a cholera infection among communities living along a river.

\

}, keywords = {Monitoring, Signal Temporal Logic, Spatial Logic, Spatio-Temporal Modelling}, doi = {10.4108/icst.valuetools.2014.258183}, url = {http://eudl.eu/doi/10.4108/icst.valuetools.2014.258183}, author = {Luca Bortolussi and Laura Nenzi} } @conference {bartocci2015studying, title = {Studying Emergent Behaviours in Morphogenesis Using Signal Spatio-Temporal Logic}, booktitle = {Hybrid Systems and Biology (HSB)}, volume = {9271}, year = {2015}, pages = {156{\textendash}172}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, edition = {LNCS}, abstract = {Pattern formation is an important spatio-temporal emergent behaviour in biology. Mathematical models of pattern formation in the stochastic setting are extremely challenging to execute and analyse. Here we propose a formal analysis of the emergent behaviour of stochastic reaction diffusion systems in terms of Signal Spatio-Temporal Logic, a recently proposed logic for reasoning on spatio-temporal systems. We present a formal analysis of the spatio-temporal dynamics of the Bicoid morphogen in Drosophila melanogaster, one of the most important proteins in the formation of the horizontal segmentation in the development of the fly embryo. We use a recently proposed framework for statistical model checking of stochastic systems with uncertainty on parameters to characterise the parametric dependence and robustness of the French Flag pattern, highlighting non-trivial correlations between the parameter values and the emergence of the patterning.

}, keywords = {model checking, Parameter estimation, Pattern Formation, Spatio-temporal logic, System Design}, doi = {10.1007/978-3-319-26916-0_9}, author = {Bartocci, Ezio and Bortolussi, Luca and Milios, Dimitrios and Nenzi, Laura and Sanguinetti, Guido} } @article {298, title = {System design of stochastic models using robustness of temporal properties}, journal = {Theoretical Computer Science}, volume = {587}, year = {2015}, pages = {3-25}, abstract = {Abstract Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem, i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to maintain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness degrees. By discussing three examples, we show how to approximate the distribution of the robustness degree and the average robustness. Secondly, we show how to exploit this notion to address the system design problem, where the goal is to optimise some control parameters of a stochastic model in order to maximise robustness of the desired specifications.

}, keywords = {Robustness degree, Stochastic models, System Design, Temporal Logic}, issn = {0304-3975}, doi = {http://dx.doi.org/10.1016/j.tcs.2015.02.046}, url = {http://www.sciencedirect.com/science/article/pii/S0304397515002224}, author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi and Guido Sanguinetti} } @conference {bortolussi2015u, title = {U-Check: model checking and parameter synthesis under uncertainty}, booktitle = {Quantitative Evaluation of Systems (QEST)}, volume = {9259}, year = {2015}, pages = {89{\textendash}104}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, edition = {LNCS}, abstract = {Novel applications of formal modelling such as systems biology have highlighted the need to extend formal analysis techniques to domains with pervasive parametric uncertainty. Consequently, machine learning methods for parameter synthesis and uncertainty quantification are playing an increasingly significant role in quantitative formal modelling. In this paper, we introduce a toolbox for parameter synthesis and model checking in uncertain systems based on Gaussian Process emulation and optimisation. The toolbox implements in a user friendly way the techniques described in a series of recent papers at QEST and other primary venues, and it interfaces easily with widely used modelling languages such as PRISM and Bio-PEPA. We describe in detail the architecture and use of the software, demonstrating its application on a case study.

}, keywords = {Gaussian Processes, Statistical Model Checking, Uncertain Continuous-Time Markov chains}, doi = {10.1007/978-3-319-22264-6_6}, author = {Bortolussi, Luca and Milios, Dimitrios and Sanguinetti, Guido} } @conference {287, title = {Data-Driven Statistical Learning of Temporal Logic Properties}, booktitle = {12th International Conference on Formal Modeling and Analysis of Timed Systems, {FORMATS} 2014.}, volume = {8711}, year = {2014}, pages = {23{\textendash}37}, publisher = {Springer}, organization = {Springer}, edition = {Lecture Notes in Computer Science}, address = {Firenze, Italy.}, abstract = {We present a novel approach to learn logical formulae characterising the emergent behaviour of a dynamical system from system observations. At a high level, the approach starts by devising a data-driven statistical abstraction of the system. We then propose general optimisation strategies for selecting formulae with high satisfaction probability, either within a discrete set of formulae of bounded complexity, or a parametric family of formulae. We illustrate and ap- ply the methodology on two real world case studies: characterising the dynamics of a biological circadian oscillator, and discriminating different types of cardiac malfunction from electro-cardiogram data. Our results demonstrate that this approach provides a statistically principled and generally usable tool to logically characterise dynamical systems in terms of temporal logic formulae.

}, doi = {10.1007/978-3-319-10512-3_3}, url = {http://dx.doi.org/10.1007/978-3-319-10512-3_3}, author = {Ezio Bartocci and Luca Bortolussi and Guido Sanguinetti} } @article {290, title = {Hybrid Systems and Biology}, journal = {Information and Computation}, volume = {236}, year = {2014}, pages = {1{\textendash}2}, type = {Preface}, doi = {10.1016/j.ic.2014.01.008}, url = {http://dx.doi.org/10.1016/j.ic.2014.01.008}, author = {Ezio Bartocci and Luca Bortolussi and Scott A. Smolka} } @conference {280, title = {Mean-Field approximation and Quasi-Equilibrium reduction of Markov Population Models}, booktitle = {11th International Conference on Quantitative Evaluation of SysTems, QEST 2014}, volume = {8657}, year = {2014}, pages = {106-121}, publisher = {Springer}, organization = {Springer}, edition = {Lecture Notes in Computer Science}, address = {Firenze, Italy}, abstract = {Markov Population Model is a commonly used framework to describe stochastic systems. Their exact analysis is unfeasible in most cases because of the state space explosion. Approximations are usually sought, often with the goal of reducing the number of variables. Among them, the mean field limit and the quasi-equilibrium approximations stand out. We view them as techniques that are rooted in independent basic principles. At the basis of the mean field limit is the law of large numbers. The principle of the quasi-equilibrium reduction is the separation of temporal scales. It is common practice to apply both limits to an MPM yielding a fully reduced model. Although the two limits should be viewed as completely independent options, they are applied almost invariably in a fixed sequence: MF limit first, QE reduction second. We present a framework that makes explicit the distinction of the two reductions, and allows an arbitrary order of their application. By inverting the sequence, we show that the double limit does not commute in general: the mean field limit of a time-scale reduced model is not the same as the time-scale reduced limit of a mean field model. An example is provided to demonstrate this phenomenon. Sufficient conditions for the two operations to be freely exchangeable are also provided.

}, isbn = {978-3-319-10695-3}, doi = {10.1007/978-3-319-10696-0_9}, url = {http://dx.doi.org/10.1007/978-3-319-10696-0_9}, author = {Bortolussi, Luca and Paskauskas, Rytis} } @proceedings {281, title = {Proceedings 12th International Workshop on Quantitative Aspects of Programming Languages and Systems}, volume = {EPTCS 155}, year = {2014}, publisher = {Open publishing association}, edition = {Electronic Proceedings in Theoretical Computer Science}, keywords = {programming languages, quantitative analysis}, doi = {10.4204/EPTCS.154}, author = {Nathalie Bertrand and Luca Bortolussi} } @article {277, title = {Smoothed Model Checking for Uncertain Continuous Time Markov Chains}, number = {1402.1450}, year = {2014}, month = {02/2014}, abstract = {We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters. We then propose a novel statistical algorithm which performs statistical model checking by leveraging the smoothness of the satisfaction probability in a Bayesian hierarchical modelling framework. In this way, our approach is able to provide an analytical approximation to the satisfaction probability of a formula, yielding an estimate of the satisfaction probability at all values of the parameters from observations of truth values over a small number of individual simulations of the system. Empirical results on non-trivial case studies show that the approach is accurate and several orders of magnitude faster than standard statistical model checking methods.

}, doi = {http://arxiv.org/abs/1402.1450}, url = {http://arxiv.org/abs/1402.1450}, author = {Luca Bortolussi and Dimitrios Milios and Guido Sanguinetti} } @proceedings {279, title = {A statistical approach for computing reachability of non-linear and stochastic dynamical systems}, volume = {8657}, year = {2014}, note = {Matlab code available on request from the author. Mail me!

We present a novel approach to compute reachable sets of dynamical systems with uncertain initial conditions or parameters, leveraging state-of-the-art statistical techniques. From a small set of samples of the true reachable function of the system, expressed as a function of initial conditions or parameters, we emulate such function using a Bayesian method based on Gaussian Processes. Uncertainty in the reconstruction is reflected in confidence bounds which, when combined with template polyhedra ad optimised, allow us to bound the reachable set with a given statistical confidence. We show how this method works straightforwardly also to do reachability computations for uncertain stochastic models.

}, issn = {978-3-319-10695-3}, doi = {10.1007/978-3-319-10696-0_5}, url = {http://dx.doi.org/10.1007/978-3-319-10696-0_5}, author = {Bortolussi, Luca and Sanguinetti, Guido} } @conference {289, title = {Stochastic Approximation of Global Reachability Probabilities of Markov Population Models}, booktitle = { 11th European Workshop on Computer Performance Engineering - {EPEW} 2014 }, volume = {8721}, year = {2014}, pages = {224{\textendash}239}, publisher = {Springer}, organization = {Springer}, edition = {Lecture Notes in Computer Science}, address = {Florence, Italy}, abstract = {Complex computer systems, from peer-to-peer networks to the spreading of computer virus epidemics, can often be described as Markovian models of large populations of interacting agents. Many properties of such systems can be rephrased as the computation of time bounded reachability probabilities. However, large population models suffer severely from state space explosion, hence a direct computation of these probabilities is often unfeasible. In this paper we present some results in estimating these probabilities using ideas borrowed from Fluid and Central Limit approximations. We consider also an empirical improvement of the basic method leveraging higher order stochastic approximations. Results are illustrated on a peer-to-peer example.

}, keywords = {central limit approximation, fluid approximation, hitting times, linear noise approximation., reachability, Stochastic model checking}, isbn = {978-3-319-10884-1}, doi = {10.1007/978-3-319-10885-8_16}, url = {http://dx.doi.org/10.1007/978-3-319-10885-8_16}, author = {Luca Bortolussi and Roberta Lanciani}, editor = {Andr{\'a}s Horv{\'a}th and Katinka Wolter} } @article {291, title = {Stochastic HYPE: Flow-based modelling of stochastic hybrid systems}, number = {arXiv:1411.4433}, year = {2014}, abstract = {Stochastic HYPE is a novel process algebra that models stochastic, instantaneous and continuous behaviour. It develops the flow-based approach of the hybrid process algebra HYPE by replacing non-urgent events with events with exponentially-distributed durations and also introduces random resets. The random resets allow for general stochasticity, and in particular allow for the use of event durations drawn from distributions other than the exponential distribution. To account for stochasticity, the semantics of stochastic HYPE target piecewise deterministic Markov processes (PDMPs), via intermediate transition-driven stochastic hybrid automata (TDSHA) in contrast to the hybrid automata used as semantic target for HYPE. Stochastic HYPE models have a specific structure where the controller of a system is separate from the continuous aspect of this system providing separation of concerns and supporting reasoning. A novel equivalence is defined which captures when two models have the same stochastic behaviour (as in stochastic bisimulation), instantaneous behaviour (as in classical bisimulation) and continuous behaviour. These techniques are illustrated via an assembly line example.

}, url = {http://arxiv.org/abs/1411.4433}, author = {Bortolussi, Luca and Galpin, Vashti and Hillston, Jane} } @conference {288, title = {Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients}, booktitle = {6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - ISoLA 2014. }, volume = {8803}, year = {2014}, pages = {391{\textendash}403}, publisher = {Springer}, organization = {Springer}, edition = {Lecture Notes in Computer Science}, address = {Corfu, Greece}, abstract = {We introduce a novel approach to automatically detect ineffective breathing efforts in patients in intensive care subject to assisted ventilation. The method is based on synthesising from data temporal logic formulae which are able to discriminate between normal and ineffective breaths. The learning procedure consists in first constructing statistical models of normal and abnormal breath signals, and then in looking for an optimally discriminating formula. The space of formula structures, and the space of parameters of each formula, are searched with an evolutionary algorithm and with a Bayesian optimisation scheme, respectively. We present here our preliminary results and we discuss our future research directions.

\

}, isbn = {978-3-662-45230-1}, doi = {10.1007/978-3-662-45231-8}, url = {http://dx.doi.org/10.1007/978-3-662-45231-8}, author = {Sara Bufo and Ezio Bartocci and Guido Sanguinetti and Massimo Borelli and Umberto Lucangelo and Luca Bortolussi}, editor = {Tiziana Margaria and Bernhard Steffen} } @article {256, title = {Bounds on the deviation of discrete-time Markov chains from their mean-field model}, journal = {Performance Evaluation}, volume = {70}, year = {2013}, note = {Proceedings of the 31st International Symposium on Computer Performance, Modeling, Measurements and Evaluation 2013, PERFORMANCE 2013

}, pages = {736-749}, abstract = {We consider a generic mean-field scenario, in which a sequence of population models, described by discrete- time Markov chains (DTMCs), converges to a deterministic limit in discrete time. Under the assumption that the limit has a globally attracting equilibrium, the steady states of the sequence of DTMC models converge to the point-mass distribution concentrated on this equilibrium. In this paper we provide explicit bounds in probability for the convergence of such steady states, combining stochastic bounds on the local error with control-theoretic tools used in the stability analysis of perturbed dynamical systems to bound the global accumulation of error. We also adapt this method to compute bounds on the transient dynamics. The approach is illustrated by a wireless sensor network example.

}, keywords = {Markov population models, mean field approximation, Steady state error bounds for mean field, Steady state mean field approximation, Transient error bounds for mean field}, doi = {10.1016/j.peva.2013.08.012}, url = {http://www.sciencedirect.com/science/article/pii/S0166531613000904}, author = {Luca Bortolussi and Richard Hayden} } @inbook {154, title = {Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation}, booktitle = {Formal Methods for Dynamical Systems}, series = {Lecture Notes in Computer Science}, volume = {7938}, year = {2013}, pages = {113{\textendash}149}, publisher = {Springer}, organization = {Springer}, address = {Berlin Heidelberg}, abstract = {In this chapter, we will describe, in a tutorial style, recent work on the use of fluid approximation techniques in the context of stochastic model checking. We will discuss the theoretical background and the algorithms working out an example. This approach is designed for population models, in which a (large) number of individual agents interact, which give rise to continuous time Markov chain (CTMC) models with a very large state space. We then focus on properties of individual agents in the system, specified by Continuous Stochastic Logic (CSL) formulae, and use fluid approximation techniques (specifically, the so called fast simulation) to check those properties. We will show that verification of such CSL formulae reduces to the computation of reachability probabilities in a special kind of time-inhomogeneous CTMC with a small state space, in which both the rates and the structure of the CTMC can change (discontinuously) with time. In this tutorial, we will discuss only briefly the theoretical issues behind the approach, like the decidability of the method and the consistency of the approximation scheme.

}, keywords = {fluid approximation, mean field approximation, reachability probability, Stochastic model checking, time-inhomogeneous Continuous Time Markov Chains}, doi = {10.1007/978-3-642-38874-3_4}, author = {Luca Bortolussi and Jane Hillston} } @article {156, title = {Continuous approximation of collective system behaviour: A tutorial}, journal = {Performance Evaluation}, volume = {70}, year = {2013}, pages = {317{\textendash}349}, abstract = {In this paper we present an overview of the field of deterministic approximation of Markov processes, both in discrete and continuous times. We will discuss mean field approximation of discrete time Markov chains and fluid approximation of continuous time Markov chains, considering the cases in which the deterministic limit process lives in continuous time or discrete time. We also consider some more advanced results, especially those relating to the limit stationary behaviour. We assume a knowledge of modelling with Markov chains, but not of more advanced topics in stochastic processes.

}, keywords = {Deterministic approximation, fluid approximation, Markov chains, mean field approximation, Stochastic process algebras}, doi = {10.1016/j.peva.2013.01.001}, url = {http://dx.doi.org/10.1016/j.peva.2013.01.001}, author = {Luca Bortolussi and Jane Hillston and Diego Latella and Mieke Massink} } @conference {274, title = {Differential Analysis of Interacting Automata with Immediate Actions}, booktitle = {7th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2013}, year = {2013}, pages = {49-58}, publisher = {ACM}, organization = {ACM}, edition = {Proceedings of the ACM}, address = {Torino, Italy}, abstract = {The stochastic modelling of software systems with activities of du- rations that are separated by many orders of magnitude typically leads to numerical complications, due to stiffness. To avoid explicit state-space generation---a prerequisite to tackle this problem via suitable manipulations or aggregations---in this paper we present an accurate and scalable fluid approximation. It is expressed as a compact piecewise linear system of ordinary differential equations, which have discontinuous right-hand sides as a result of the incorporation of immediateness. We study the nature of this approximation in a general high-level framework of interacting automata. On a case study of client/server interaction, our approach is ca two times faster than the analysis conducted on the stiff equations where immediate actions are explicitly modelled.

}, keywords = {Differential Equations, Immediate actions, time-scale separation}, isbn = {978-1-936968-48-0}, doi = {10.4108/icst.valuetools.2013.254364}, url = {http://doi.acm.org/10.4108/icst.valuetools.2013.254364}, author = {Bortolussi, Luca and Tribastone, Mirco} } @article {172, title = {(Hybrid) Automata and (Stochastic) Programs. The hybrid automata lattice of a stochastic program}, journal = {Journal Of Logic And Computation}, volume = {23}, year = {2013}, pages = {761-798}, chapter = {761}, abstract = {We define a semantics for stochastic Concurrent Constraint Programming (sCCP), a stochastic process algebra, in terms of stochastic hybrid automata with piecewise deterministic continuous dynamics. To each program we associate a lattice of hybrid models, parameterized with respect to the degree of discreteness left. We study some properties of this lattice, presenting also an alternative semantics in which the degree of discreteness can be dynamically changed.

}, keywords = {Hybrid Semantics, Stochastic Hybrid Automata, Stochastic Process Algebra, Stochastic Process Algebra Approximation}, doi = {10.1093/logcom/exr045}, url = {http://logcom.oxfordjournals.org/content/early/2011/12/06/logcom.exr045.short?rss=1}, author = {Luca Bortolussi and Alberto Policriti} } @article {157, title = {HYPE: Hybrid modelling by composition of flows}, journal = {Formal Aspects Of Computing}, volume = {25}, year = {2013}, pages = {503{\textendash}541}, abstract = {Hybrid systems are manifest in both the natural and the engineered world, and their complex nature, mixing discrete control and continuous evolution, make it difficult to predict their behaviour. In recent years several process algebras for modelling hybrid systems have appeared in the literature, aimed at addressing this problem. These all assume that continuous variables in the system are modelled monolithically, often with differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of flows. In this paper we give a detailed account of the HYPE process algebra, its semantics, and its use for verification of systems. We establish both syntactic conditions (well-definedness) and operational restrictions (well-behavedness) to ensure reasonable behaviour in HYPE models. Furthermore we consider how the equivalence relation defined for HYPE relates to other relations previously proposed in the literature, demonstrating that our fine-grained approach leads to a more discriminating notion of equivalence. We present the HYPE model of a standard hybrid system example, both establishing that our approach can reproduce the previously obtained results and demonstrating how our compositional approach supports variations of the problem in a straightforward and flexible way.

}, keywords = {Bisimulation, Compositionality, Flows, Hybrid Systems, process algebra}, doi = {10.1007/s00165-011-0189-0}, author = {Vashti Galpin and Luca Bortolussi and Jane Hillston} } @conference {254, title = {Learning and designing stochastic processes from logical constraints}, booktitle = {10th International Conference on Quantitative Evaluation of SysTems, QEST 2013}, volume = {8054}, year = {2013}, note = {**Best paper award**

Continuous time Markov Chains (CTMCs) are a convenient mathematical model for a broad range of natural and computer systems. As a result, they have received considerable attention in the theoretical computer science community, with many important techniques such as model checking being now mainstream. However, most methodologies start with an assumption of complete specification of the CTMC, in terms of both initial conditions and parameters. While this may be plausible in some cases (e.g. small scale engineered systems) it is certainly not valid nor desirable in many cases (e.g. biological systems), and it does not lead to a constructive approach to rational design of systems based on specific requirements. Here we consider the problems of learning and designing CTMCs from observations/ requirements formulated in terms of satisfaction of temporal logic formulae. We recast the problem in terms of learning and maximising an unknown function (the likelihood of the parameters) which can be numerically estimated at any value of the parameter space (at a non-negligible computational cost). We adapt a recently proposed, provably convergent global optimisation algorithm developed in the machine learning community, and demonstrate its efficacy on a number of non-trivial test cases.

}, isbn = {978-3-642-40195-4}, doi = {10.1007/978-3-642-40196-1_7}, url = {http://link.springer.com/chapter/10.1007\%2F978-3-642-40196-1_7}, author = {Luca Bortolussi and Guido Sanguinetti} } @conference {255, title = {Model Checking Markov Population Models by Central Limit Approximation}, booktitle = {10th International Conference on Quantitative Evaluation of SysTems, QEST 2013}, volume = {8054}, year = {2013}, pages = {123-138}, publisher = {Springer Verlag}, organization = {Springer Verlag}, edition = {Lecture Notes in Computer Science}, address = {Buenos Aires, Argentina}, abstract = {In this paper we investigate the use of Central Limit Approximation of Continuous Time Markov Chains to verify collective properties of large population models, describing the interaction of many similar individual agents. More precisely, we specify properties in terms of individual agents by means of deterministic timed automata with a single global clock (which cannot be reset), and then use the Central Limit Approximation to estimate the probability that a given fraction of agents satisfies the local specification.

}, isbn = {978-3-642-40195-4 }, doi = {10.1007/978-3-642-40196-1_9}, url = {http://link.springer.com/chapter/10.1007\%2F978-3-642-40196-1_9}, author = {Luca Bortolussi and Roberta Lanciani} } @proceedings {155, title = {Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems}, volume = {EPTCS 117}, year = {2013}, publisher = {Open publishing association}, edition = {Electronic Proceedings in Theoretical Computer Science}, keywords = {programming languages, quantitative analysis}, doi = {10.4204/EPTCS.117}, author = {Luca Bortolussi and Herbert Wiklicky} } @proceedings {266, title = {Proceedings Third International Workshop on Hybrid Autonomous Systems}, volume = {EPTCS 124}, year = {2013}, publisher = {Open Access Publishing}, edition = {Electronic Proceedings in Theoretical Computer Science}, address = {Rome, March 17, 2013}, doi = {10.4204/EPTCS.124}, url = {http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?HAS2013}, author = {Luca Bortolussi and Manuela L Bujorianu and Giordano Pola} } @conference {272, title = {On the Robustness of Temporal Properties for Stochastic Models}, booktitle = {Proceedings Second International Workshop on Hybrid Systems and Biology}, volume = {125}, year = {2013}, pages = {3-19}, publisher = {Open Publishing Association}, organization = {Open Publishing Association}, edition = {Electronic Proceedings in Theoretical Computer Science}, address = {Taormina, Italy, 2nd September 2013}, abstract = {Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem. i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to mantain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness scores. By discussing two examples, we show how to approximate the distribution of the robustness score and its key indicators: the average robustness and the conditional average robustness. Secondly, we show how to combine these indicators with the satisfaction probability to address the system design problem, where the goal is to optimize some control parameters of a stochastic model in order to best maximize robustness of the desired specifications.

}, doi = {10.4204/EPTCS.125.1}, url = {http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?HSB2013.1}, author = {Bartocci, Ezio and Bortolussi, Luca and Nenzi, Laura and Sanguinetti, Guido}, editor = {Dang, Thao and Piazza, Carla} } @conference {153, title = {Stochastic Process Algebra and Stability Analysis of Collective Systems}, booktitle = {Coordination Models and Languages}, series = {Lecture Notes In Computer Science}, volume = {7890}, year = {2013}, pages = {1{\textendash}15}, publisher = {Springer Berlin Heidelberg}, organization = {Springer Berlin Heidelberg}, edition = {Lecture Notes in Computer Science}, abstract = {Collective systems consist of large numbers of agents that coordinate through local behaviour, adapt to their environment and possibly give rise to emergent phenomena. Their formal analysis requires advanced scalable mathematical approximation techniques. We show how Stochastic Process Algebra (SPA) can be combined with numeric analysis tools for the analysis of emergent behavioural aspects of such systems. The approach is based on an automatic transformation of SPA models into ordinary differential equations in a format in which numeric and symbolic computing environments can be used to perform stability analysis of the system. The potential of the approach is illustrated by a crowd dynamics scenario in which various forms of behavioural and topological asymmetry are introduced. These are cases in which analytical approaches to stability analysis are in general not feasible.The analysis also shows some surprising aspects of the crowd model itself.

}, keywords = {crowd dynamics, Fluid flow, process algebra, self-organisation}, doi = {10.1007/978-3-642-38493-6_1}, author = {Luca Bortolussi and Diego Latella and Mieke Massink}, editor = {Rocco De Nicola and Christine Julien} } @article {152, title = {A temporal logic approach to modular design of synthetic biological circuits}, volume = {abs/1306.4493}, year = {2013}, institution = {ArXiv}, abstract = {We present a new approach for the design of a synthetic biological circuit whose behaviour is specified in terms of signal temporal logic (STL) formulae. We first show how to characterise with STL formulae the input/output behaviour of biological modules miming the classical logical gates (AND, NOT, OR). Hence, we provide the regions of the parameter space for which these specifications are satisfied. Given a STL specification of the target circuit to be designed and the networks of its constituent components, we propose a methodology to constrain the behaviour of each module, then identifying the subset of the parameter space in which those constraints are satisfied, providing also a measure of the robustness for the target circuit design. This approach, which leverages recent results on the quantitative semantics of Signal Temporal Logic, is illustrated by synthesising a biological implementation of an half-adder.}, keywords = {Parameter Synthesis, Synthetic Biology, Temporal Logic}, url = {http://arxiv.org/abs/1306.4493}, author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi} } @conference {257, title = {A temporal logic approach to modular design of synthetic biological circuits}, booktitle = {11th Conference on Computational Methods in Systems Biology, CMSB 2013 }, volume = {8130}, year = {2013}, pages = {164-177}, publisher = {Springer}, organization = {Springer}, edition = {Lecture Notes in Computer Science}, address = {Vienna, September 2013}, abstract = {We present a new approach for the design of a synthetic biological circuit whose behaviour is specified in terms of signal temporal logic (STL) formulae. We first show how to characterise with STL formulae the input/output behaviour of biological modules miming the classical logical gates (AND, NOT, OR). Hence, we provide the regions of the parameter space for which these specifications are satisfied. Given a STL specification of the target circuit to be designed and the networks of its constituent components, we propose a methodology to constrain the behaviour of each module, then identifying the subset of the parameter space in which those constraints are satisfied, providing also a measure of the robustness for the target circuit design. This approach, which leverages recent results on the quantitative semantics of Signal Temporal Logic, is illustrated by synthesising a biological implementation of an half-adder.

}, keywords = {Parameter Synthesis, Synthetic Biology, Temporal Logic}, isbn = {978-3-642-40707-9}, doi = {10.1007/978-3-642-40708-6_13}, url = {http://link.springer.com/chapter/10.1007/978-3-642-40708-6_13}, author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi} } @conference {158, title = {Don{\textquoteright}t Just Go with the Flow: Cautionary Tales of Fluid Flow Approximation}, booktitle = {9th European Workshop on Computer Performance Engineering, EPEW 2012, and 28th UK Workshop on Computer Performance Engineering, UKPEW 2012}, series = {Lecture Notes in Computer Science}, volume = {7587}, year = {2012}, pages = {156{\textendash}171}, publisher = {Springer}, organization = {Springer}, abstract = {Fluid flow approximation allows efficient analysis of large scale PEPA models. Given a model, this method outputs how the mean, variance, and any other moment of the model{\textquoteright}s stochastic behaviour evolves as a function of time. We investigate whether the method{\textquoteright}s results, i.e. moments of the behaviour, are sufficient to capture system{\textquoteright}s actual dynamics. We ran a series of experiments on a client-server model. For some parametrizations of the model, the model{\textquoteright}s behaviour can accurately be characterized by the fluid flow approximations of its moments. However, the experiments show that for some other parametrizations, these moments are not sufficient to capture the model{\textquoteright}s behaviour, highlighting a pitfall of relying only on the results of fluid flow analysis. The results suggest that the sufficiency of the fluid flow method for the analysis of a model depends on the model{\textquoteright}s concrete parametrization. They also make it clear that the existing criteria for deciding on the sufficiency of the fluid flow method are not robust.}, keywords = {fluid approximation, PEPA, Stochastic process algebras}, doi = {10.1007/978-3-642-36781-6_11}, author = {Alireza Pourranjbar and Jane Hillston and Luca Bortolussi}, editor = {Mirco Tribastone and Stephen Gilmore} } @conference {159, title = {Fluid Approximation of CTMC with Deterministic Delays}, booktitle = {Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012}, year = {2012}, note = {Supplementary online material is attached at the end of the pdf file or available as a stand-alone pdf here.

}, pages = {53{\textendash}62}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, abstract = {We compare population models in terms of Continuous Time Markov Chains with embedded deterministic delays (delayed CTMC), in which an exponential timed transition can only update the state of the system after a deterministic delay, and delay differential equations (DDE). We prove a fluid approximation theorem, showing that, when the size of the population goes to infinity, the delayed CTMC converges to a solution of the DDE.

}, keywords = {Delay Differential Equations, fluid approximation, Markov Processes with Delays}, doi = {10.1109/QEST.2012.13}, url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6354633}, author = {Luca Bortolussi and Jane Hillston}, editor = {G. Casale and L. Cherkasova and H. Hermanns} } @conference {162, title = {Fluid limit of an asynchronous optical packet switch with shared per link full range wavelength conversion}, booktitle = {ACM SIGMETRICS/PERFORMANCE}, year = {2012}, month = {15, 2012}, pages = {113{\textendash}124}, publisher = {ACM}, organization = {ACM}, abstract = {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 sigma= C/N remains fixed). More specifically, for sigma\<lambda^ 2 the loss probability tends to (lambda^2-sigma)/lambda(1+lambda), while for sigma \> lambda^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.

}, keywords = {Fluid limit, optical packet switch, wavelength conversion}, doi = {10.1145/2254756.2254772}, author = {B. V. Houdt and Luca Bortolussi}, editor = {Peter G. Harrison and Martin F. Arlitt and Giuliano Casale} } @conference {166, title = {Fluid limits of queueing networks with batches}, booktitle = {ICPE 2012}, year = {2012}, month = {25, 2012}, pages = {45{\textendash}56}, publisher = {ACM}, organization = {ACM}, abstract = {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.

}, keywords = {Batch Queues, Fluid Limits, Hybrid Limits, mean field approximation}, doi = {10.1145/2188286.2188296}, url = {http://dl.acm.org/citation.cfm?doid=2188286.2188296}, author = {Luca Bortolussi and Mirco Tribastone}, editor = {David R. Kaeli and Jerry Rolia and Lizy K. John and Diwakar Krishnamurthy} } @article {167, title = {Fluid Model Checking}, number = {abs/1203.0920}, year = {2012}, institution = {ArXiv}, abstract = {In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC which depends on the environment and on the other agents only through the solution of the fluid differential equation. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae and of reachability probabilities. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.

}, keywords = {Continuous Stochastic Logic, fluid approximation, mean field approximation, Stochastic model checking, time-inhomogeneous Continuous Time Markov Chains}, url = {http://arxiv.org/abs/1203.0920}, author = {Luca Bortolussi and Jane Hillston} } @conference {161, title = {Fluid Model Checking}, booktitle = {22th International Conference on Concurrency Theory, CONCUR 2012}, series = {Lecture Notes In Computer Science}, volume = {7454}, year = {2012}, pages = {333{\textendash}347}, publisher = {Springer}, organization = {Springer}, address = {Berlin Heidelberg}, abstract = {In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a limit result known also as fast simulation. In particular, we will approximate the behaviour of a single agent with a time-inhomogeneous CTMC which depends on the environment and on the other agents only through the solution of the fluid differential equation. We will prove the asymptotic correctness of our approach in terms of satisfiability of CSL formulae and of reachability probabilities. We will also present a procedure to model check time-inhomogeneous CTMC against CSL formulae.

}, keywords = {fluid approximation, mean field approximation, reachability probability, Stochastic model checking}, doi = {10.1007/978-3-642-32940-1_24}, url = {http://dx.doi.org/10.1007/978-3-642-32940-1_24}, author = {Luca Bortolussi and Jane Hillston}, editor = {Koutny, Maciej and Ulidowski, Irek} } @article {252, title = {Hybrid Behaviour of Markov Population Models}, number = {abs/1211.1643}, year = {2012}, institution = {ArXiv}, abstract = {We investigate the behaviour of population models written in Stochastic Concurrent Constraint Programming (sCCP), a stochastic extension of Concurrent Constraint Programming. In particular, we focus on models from which we can define a semantics of sCCP both in terms of Continuous Time Markov Chains (CTMC) and in terms of Stochastic Hybrid Systems, in which some populations are approximated continuously, while others are kept discrete. We will prove the correctness of the hybrid semantics from the point of view of the limiting behaviour of a sequence of models for increasing population size. More specifically, we prove that, under suitable regularity conditions, the sequence of CTMC constructed from sCCP programs for increasing population size converges to the hybrid system constructed by means of the hybrid semantics. We investigate in particular what happens for sCCP models in which some transitions are guarded by boolean predicates or in the presence of instantaneous transitions.

}, keywords = {Hybrid Fluid Limit, Hybrid Mean Field, Hybrid Systems, stochastic concurrent constraint programming, Stochastic process algebras}, url = {http://arxiv.org/abs/1211.1643}, author = {Luca Bortolussi} } @conference {163, title = {Hybrid performance modelling of opportunistic networks}, booktitle = {QAPL 2012}, series = {Electronic Proceedings In Theoretical Computer Science}, volume = {85}, year = {2012}, month = {April 1, 2012}, pages = {106{\textendash}121}, publisher = {Open Publishing Association}, organization = {Open Publishing Association}, abstract = {We demonstrate the modelling of opportunistic networks using the process algebra stochastic HYPE. Network traffic is modelled as continuous flows, contact between nodes in the network is modelled stochastically, and instantaneous decisions are modelled as discrete events. Our model describes a network of stationary video sensors with a mobile ferry which collects data from the sensors and delivers it to the base station. We consider different mobility models and different buffer sizes for the ferries. This case study illustrates the flexibility and expressive power of stochastic HYPE. We also discuss the software that enables us to describe stochastic HYPE models and simulate them.}, keywords = {HYPE, opportunistic networks, stochastic hybrid systems}, doi = {10.4204/EPTCS.85.8}, url = {http://eptcs.org/paper.cgi?QAPL2012.8}, author = {Luca Bortolussi and Vashti Galpin and Jane Hillston}, editor = {Herbert Wiklicky and Mieke Massink} } @proceedings {160, title = {Proceedings First International Workshop on Hybrid Systems and Biology}, volume = {92}, year = {2012}, pages = {1{\textendash}166}, publisher = {Open Publishing Association}, keywords = {Computational Systems Biology, Hybrid Systems}, doi = {10.4204/EPTCS.92}, url = {http://rvg.web.cse.unsw.edu.au/eptcs/content.cgi?HSB2012$\#$EPTCS92.0}, author = {Ezio Bartocci and Luca Bortolussi} } @article {165, title = {Spearman Permutation Distances and Shannon{\textquoteright}s Distinguishability}, journal = {Fundamenta Informaticae}, volume = {118}, year = {2012}, pages = {245{\textendash}252}, abstract = {Spearman distance is a permutation distance which might be used for codes in permutations beside Kendall distance. However, Spearman distance gives rise to a geometry of strings, which is rather unruly from the point of view of error correction and error detection. Special care has to be taken to discriminate between the two notions of codeword distance and codeword distinguishability. This stresses the importance of rejuvenating the latter notion, extending it from Shannon{\textquoteright}s zero-error information theory to the more general setting of metric string distances.}, keywords = {codeword distinguishability, rank distance, Shannon theory, Spearman footrule distance}, doi = {10.3233/FI-2012-712}, url = {http://iospress.metapress.com/content/824rm66046167l62/}, author = {Luca Bortolussi and Liviu P. Dinu and Andrea Sgarro} } @article {168, title = {Statistics and histopathology: a mixed-effects model approach to digital image analysis}, journal = {Pathologica}, volume = {104}, year = {2012}, pages = {161{\textendash}162}, abstract = {In quantitative histology several image analysis software are avaible with good results in detecting objects both on morphometrical side (perimeter, diameter, area, shape factor) and densitometrical features (RGB or gray density). Classification usually is performed by estracting overall information y low-level features (relationships between pixels and objects) and high level features (histological textures/structures). In thi communication we ficus the possibility to exploit random effects approach in histopathological analisys (abstract only).}, keywords = {histopathological image analysis, mixed-effect model}, url = {www.pacinieditore.it/pathologica}, author = {Massimo Borelli and F. Zanconati and Luca Bortolussi and F. Giudici and G. Barbati and Lucio Torelli} } @article {164, title = {Studying cancer-cell populations by programmable models of networks}, journal = {Network Modeling Analysis In Health Informatics And Bioinformatics}, volume = {1}, year = {2012}, note = {Supplementary material available here.

}, pages = {117{\textendash}133}, abstract = {We draw the basic lines for an approach to build mathematical and programmable network 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{\textemdash}together with interactions with different kinds of hormone therapy{\textemdash}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.

}, keywords = {Computational Systems Biology, Prostate tumor, Stochastic process algebras, Tumor growth modeling}, doi = {10.1007/s13721-012-0010-x}, url = {http://dx.doi.org/10.1007/s13721-012-0010-x}, author = {Luca Bortolussi and Alberto Policriti} } @conference {178, title = {Geometry of strings and possibilistic coding}, booktitle = {14th Conference on Applied Stochastic Models and Data Analysis (ASMDA2011)}, year = {2011}, month = {10 June 2011}, pages = {na{\textendash}na}, publisher = {Ets}, organization = {Ets}, address = {Roma}, keywords = {Possibilistic coding, possibilistic information theory, rank distance}, author = {Luca Bortolussi and Liviu P. Dinu and Andrea Sgarro}, editor = {Ongaro A. and Migliorati S. and Monti G.S.} } @inbook {184, title = {How Many Possible Languages Are There?}, booktitle = {Biology, Computation and Linguistics - New Interdisciplinary Paradigms}, year = {2011}, pages = {168{\textendash}179}, publisher = {IOS Press}, organization = {IOS Press}, address = {Amsterdam, Berlin, Tokyo, Washington DC}, abstract = {We adopt a description of natural languages in terms of strings of crosslinguistically variable syntactic features (parameters), complying with a specified hypothesis of {\quotesinglbase}universal grammar{\quotesinglbase} and we deal with two problems: first, assessing the statistical significance of language distances calculated on the basis of such features and recently used to reconstruct phylogenetic trees; second, counting the minimal overall number of possible human languages, i.e. of strings satisfying the implicational rules which describe dependencies between parameters of the specified universal grammar. In order to accomplish these tasks, we had to develop a sampling algorithm capable of dealing correctly with such rules. The potential significance of these results for historical and theoretical linguistics is then briefly highlighted.

}, keywords = {Language Phylogeny, Montecarlo sampling, Universal Grammar}, doi = {10.3233/978-1-60750-762-8-168}, url = {http://www.booksonline.iospress.nl/Content/View.aspx?piid=20097}, author = {Luca Bortolussi and Andrea Sgarro and Giuseppe Longobardi and Cristina Guardiano}, editor = {G Bel-Enguix and V Dahl and M D Jimenez-Lopez} } @conference {177, title = {Hybrid Limits of Continuous Time Markov Chains}, booktitle = {8th International Conference on Quantitative Evaluation of SysTems, QEST 2011}, year = {2011}, note = {}, keywords = {Continuous Time Markov Chains, fluid approximation, limit theorems, mean field approximation, piecewise smooth dynamical systems., Stochastic modelling}, doi = {10.1109/QEST.2011.10}, author = {Luca Bortolussi}, editor = {C Palamidessi and A Riska} } @conference {180, title = {HYPE with stochastic events}, booktitle = {QAPL 2011}, volume = {57}, year = {2011}, month = {3, 2011}, pages = {120{\textendash}133}, publisher = {Open Publishing Association}, organization = {Open Publishing Association}, abstract = {The process algebra HYPE was recently proposed as a fine-grained modelling approach for capturing the behaviour of hybrid systems. In the original proposal, each flow or influence affecting a variable is modelled separately and the overall behaviour of the system then emerges as the composition of these flows. The discrete behaviour of the system is captured by instantaneous actions which might be urgent, taking effect as soon as some activation condition is satisfied, or non-urgent meaning that they can tolerate some (unknown) delay before happening. In this paper we refine the notion of non-urgent actions, to make such actions governed by a probability distribution. As a consequence of this we now give HYPE a semantics in terms of Transition-Driven Stochastic Hybrid Automata, which are a subset of a general class of stochastic processes termed Piecewise Deterministic Markov Processes.}, keywords = {hybrid modelling languages, Hybrid Systems, HYPE, Stochastic Hybrid Automata}, doi = {10.4204/EPTCS.57.9}, url = {http://arxiv.org/abs/1107.1233v1}, author = {Luca Bortolussi and Vashti Galpin and Jane Hillston}, editor = {Massink, Mieke and Norman, Gethin} } @article {181, title = {Language Sampling for Universal Grammars}, journal = {Rendiconti dell{\textquoteright}Istituto di Matematica dell{\textquoteright}Universit{\`a} di Trieste}, volume = {43}, year = {2011}, pages = {95{\textendash}110}, keywords = {Language Phylogeny, Monte-Carlo Sampling, Universal Grammars}, url = {http://www.dmi.units.it/~rimut/volumi/43/060.pdf}, author = {Luca Bortolussi and Andrea Sgarro} } @conference {183, title = {Programmable models of growth and mutation of cancer-cell populations}, booktitle = {COMPMOD 2011}, volume = {67}, year = {2011}, pages = {19--33}, publisher = {Open Publishing Association}, organization = {Open Publishing Association}, edition = {Electronic Proceedings In Theoretical Computer Science}, abstract = {In this paper we propose a systematic approach to construct mathematical models describing populations of cancer-cells at different stages of disease development. The methodology we propose is based on stochastic Concurrent Constraint Programming, a flexible stochastic modelling language. The methodology is tested on (and partially motivated by) the study of prostate cancer. In particular, we prove how our method is suitable to systematically reconstruct different mathematical models of prostate cancer growth{\quotesinglbase} together with interactions with different kinds of hormone therapy{\quotesinglbase} at different levels of refinement.}, keywords = {Computational Systems Biology, Prostate Tumour, Stochastic process algebras, Tumour Growth Modelling}, doi = {10.4204/EPTCS.67.4}, url = {http://arxiv.org/abs/1109.1364v1}, author = {Luca Bortolussi and Alberto Policriti}, editor = {Ion Petre and Erik de Vink} } @conference {171, title = {A Rough guide to Hybrid Limits of Continuous Time Markov Chains}, booktitle = {PASTA 2011}, year = {2011}, pages = {74{\textendash}79}, publisher = {Consorzio Universitario della Provinci di Ragusa}, organization = {Consorzio Universitario della Provinci di Ragusa}, address = {Ragusa}, abstract = {We discuss several situations in which sequences of Continuous-Time Markov Chain population models exhibit a limit behaviour in terms of hybrid systems, having a mixed discrete and continuous dynamics.}, keywords = {Approximation Theorems, Continuous Time Markov Chains, stochastic hybrid systems}, url = {http://pastaworkshop.org/}, author = {Luca Bortolussi} } @article {190, title = {Hybrid Dynamics of Stochastic Programs}, journal = {Theoretical Computer Science}, volume = {411/20}, year = {2010}, pages = {2052{\textendash}2077}, abstract = {

We provide Stochastic Concurrent Constraint Programming (sCCP), a stochastic process algebra based on CCP, with a semantics in terms of hybrid automata. We associate with each sCCP program both a stochastic and a non-deterministic hybrid automaton. Then, we compare such automata with the standard stochastic semantics (given by a Continuous Time Markov Chain) and the one based on ordinary differential equations, obtained by a fluid-flow approximation technique. We discuss in detail two case studies: Repressilator and the Circadian Clock, with particular regard to the robustness exhibited by the different semantic models and to the effect of discreteness in dynamical evolution of such systems.

}, keywords = {Dynamical Systems, Hybrid Automata, Piecewise Deterministic Markov Processes, Robustness, stochastic concurrent constraint programming}, doi = {10.1016/j.tcs.2010.02.008}, url = {http://dx.doi.org/10.1016/j.tcs.2010.02.008}, author = {Luca Bortolussi and Alberto Policriti} } @conference {186, title = {Hybrid Semantics for PEPA}, booktitle = {Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010)}, year = {2010}, month = {September 18}, pages = {181{\textendash}190}, publisher = {IEEE computer society}, organization = {IEEE computer society}, address = {Los Alamitos, CA, USA}, abstract = {In order to circumvent the problem of state-space explosion of large-scale Markovian models, the stochastic process algebra PEPA has been given a fluid semantics based on ordinary differential equations, treating all entities as continuous. However, low numbers of instances and/or relatively slow dynamics may make such approximation too coarse for some parts of the system. To deal with such situations, we propose an hybrid semantics lying between these two extremes, treating parts of the system as discrete and stochastic and others as continuous and deterministic. The underlying mathematical object for the quantitative evaluation is a stochastic hybrid automaton. A case study of a client/server system with breakdowns and repairs is used to discuss the accuracy and the cost of this hybrid analysis.

}, keywords = {Fluid Semantics., Hybrid Approximation, Hybrid Automata, Stochastic process algebras}, doi = {10.1109/QEST.2010.31}, author = {Luca Bortolussi and Vashti Galpin and Jane Hillston and Tribastone M.}, editor = {n.a.} } @conference {187, title = {Limit behavior of the hybrid approximation of Stochastic Process Algebras}, booktitle = {17th International Conference on Analytical and Stochastic Modeling Techniques and Applications (ASMTA 2010)}, year = {2010}, note = {Supplementary material is avaiable as an appendix in the pdf of the paper.

}, month = {16, 2010}, pages = {367{\textendash}381}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, abstract = {We investigate the limit behavior of a class of stochastic hybrid systems obtained by hybrid approximation of Stochastic Concurrent Constraint Programming (sCCP). We prove that a sequence of Continuous Time Markov Chain (CTMC), constructed from sCCP programs parametrically with respect to a notion of system size, converges a.s., in the limit of divergent size, to the hybrid approximation.

}, keywords = {limit theorems, Piecewise Deterministic Markov Processes, stochastic concurrent constraint programming, stochastic hybrid systems, Stochastic process algebras}, doi = {10.1007/978-3-642-13568-2_26}, url = {http://www.springerlink.com/content/e866lj737n011l42/}, author = {Luca Bortolussi}, editor = {K. Al-Begain and D. Fiems and W.J. Knottenbelt} } @conference {185, title = {Modeling Hybrid Systems with Stochastic Events in HYPE}, booktitle = {PASTA 2010}, year = {2010}, pages = {24{\textendash}28}, publisher = {Department of Computing, Imperial College}, organization = {Department of Computing, Imperial College}, address = {London UK}, abstract = {The process algebra HYPE was recently proposed as a fine-grained modelling approach for capturing the behaviour of hybrid systems. In the original proposal, the semantics of HYPE was defined in terms of (non)deterministic hybrid systems. Here we extend the language adding stochastic events, hence obtaining a semantics in terms of Transition Driven Stochastic Hybrid Automata, a subset of a general class of stochastic process termed Piecewise Deterministic Markov Processes. The definition of stochastic HYPE is discussed by means of an example of a delay tolerant network.}, keywords = {hybrid process algebras, stochastic hybrid systems}, author = {Luca Bortolussi and Vashti Galpin and Jane Hillston} } @conference {189, title = {Perspectives on Constraints, Process Algebras, and Hybrid Systems.}, booktitle = {WCB 2010}, year = {2010}, pages = {69{\textendash}75}, publisher = {n.a.}, organization = {n.a.}, address = {Edinburgh}, abstract = {Building on a technique for associating Hybrid Systems (HS) to stochastic programs written in a stochastic extension of Concurrent Constraint Programming (sCCP), we will discuss several aspects of performing such association. In particular, as we proved an sCCP program can be mapped in a HS varying in a lattice at a level depending on the amount of actions to be simulated continuously, we will discuss what are the problems involved in a semi-automatic choice of such level. Decidability, semantic, and efficiency issues will be taken into account, with special emphasis on their links with biological applications. We will also discuss about the role of constraints and of the constraint store in this construction.

}, keywords = {Hybrid Systems, stochastic concurrent constraint programming, Systems Biology}, url = {http://wcb10.dimi.uniud.it/WCB10_proc.pdf}, author = {Luca Bortolussi and Alberto Policriti} } @conference {188, title = {Possibilistic coding: error detection vs. error correction}, booktitle = {Combining Soft Computing and Statistical Methods in Data Analysis}, series = {Advances in Intelligent and Soft Computing}, volume = {77}, year = {2010}, month = {October 2010}, pages = {41{\textendash}48}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, address = {Heidelberg}, abstract = {Possibilistic information theory is a flexible approach to old and new forms of coding; it is based on possibilities and patterns, rather than pointwise probabilities and traditional statistics. Here we fill up a gap of the possibilistic approach, and extend it to the case of error detection, while so far only error correction had been considered.

}, keywords = {error detection, Possibilistic coding, possibility theory, zero error information theory}, author = {Luca Bortolussi and Andrea Sgarro}, editor = {C. Borgerlt et al.} } @conference {196, title = {CoBiC: Context-dependent Bioambient Calculus}, booktitle = {QAPL 2009}, volume = {253}, year = {2009}, month = {March}, pages = {187{\textendash}201}, publisher = {Elsevier Science Publisher}, organization = {Elsevier Science Publisher}, 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.

}, keywords = {Functional rates, Markov Processes, Stochastic process algebras, Systems Biology}, doi = {10.1016/j.entcs.2009.10.012}, url = {http://www.sciencedirect.com/science/article/pii/S1571066109004320}, author = {Luca Bortolussi and Maria G Vigliotti}, editor = {Alessandra Di Pierro and Christel Baier} } @conference {192, title = {Dynamical Compartments in stochastic Concurrent Constraint Programming.}, booktitle = {Fifth Workshop on Constraint Based Methods for Bioinformatics, WBC2009}, year = {2009}, pages = {9{\textendash}18}, publisher = {CP}, organization = {CP}, author = {Luca Bortolussi and Alberto Policriti} } @article {197, title = {Dynamical Systems and Stochastic Programming - From Ordinary Differential Equations and Back.}, journal = {Transactions On Computational Systems Biology}, volume = {11}, year = {2009}, pages = {216{\textendash}267}, abstract = {In this paper we focus on the relation between models of biological systems consisting of ordinary differential equations (ODE) and models written in a stochastic and concurrent paradigm (sCCP - stochastic Concurrent Constraint Programming). In particular, we define a method to associate a set of ODEs to an sCCP program and a method converting ODEs into sCCP programs. Then we study the properties of these two translations. Specifically, we show that the mapping from sCCP to ODEs preserves rate semantics for the class of biochemical models (i.e. chemical kinetics is maintained) and we investigate the invertibility properties of the two mappings. Finally, we concentrate on the question of behavioral preservation, i.e if the models obtained applying the mappings have the same dynamics. We give a convergence theorem in the direction from ODEs to sCCP and we provide several well-known examples in which this property fails in the inverse direction, discussing them in detail.

}, keywords = {Computational Systems Biology, Continuous-Time Markov Chains, Differential Equations, fluid approximation, stochastic concurrent constraint programming}, doi = {10.1007/978-3-642-04186-0_11}, author = {Luca Bortolussi and Alberto Policriti} } @article {198, title = {Hybrid Dynamics of Stochastic pi-calculus}, journal = {Mathematics In Computer Science}, volume = {2}, number = {3}, year = {2009}, pages = {465{\textendash}491}, author = {Luca Bortolussi and Alberto Policriti} } @conference {193, title = {Hybrid Semantics of Stochastic Programs with Dynamic Reconfiguration.}, booktitle = {COMPMOD 2009}, series = {Electronic Proceedings In Theoretical Computer Science}, volume = {6}, year = {2009}, pages = {63{\textendash}76}, publisher = {Open Publishing Association}, organization = {Open Publishing Association}, abstract = {We begin by reviewing a technique to approximate the dynamics of stochastic programs {\textendash}written in a stochastic process algebra{\textendash} by a hybrid system, suitable to capture a mixed discrete/continuous evolution. In a nutshell, the discrete dynamics is kept stochastic while the continuous evolution is given in terms of ODEs, and the overall technique, therefore, naturally associates a Piecewise Deterministic Markov Process with a stochastic program. The specific contribution in this work consists in an increase of the flexibility of the translation scheme, obtained by allowing a dynamic reconfiguration of the degree of discreteness/continuity of the semantics. We also discuss the relationships of this approach with other hybrid simulation strategies for biochemical systems.}, keywords = {Computational Systems Biology, Hybrid Approximation, Hybrid Simulation Strategies, stochastic concurrent constraint programming, stochastic hybrid systems}, doi = {10.4204/EPTCS.6.5}, url = {http://arxiv.org/abs/0910.1406v1}, author = {Luca Bortolussi and Alberto Policriti}, editor = {Back, Ralph-Johan and Petre, Ion and Vink, Erik de} } @conference {194, title = {HYPE: a Process Algebra for Compositional Flows and Emergent Behavior.}, booktitle = {20th International Conference on Concurrency Theory}, year = {2009}, month = {April 2009}, pages = {305{\textendash}320}, publisher = {Springer Verlag}, organization = {Springer Verlag}, abstract = {Several process algebras for modelling hybrid systems have appeared in the literature in recent years. These all assume that continuous variables in the system are modelled monolithically, often with the differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of these flows. This approach is supported by an operational semantics which distinguishes states as collections of flows and which is supported by an equivalence which satisfies the property that bisimilar HYPE models give rise to the same sets of continuous behaviours.}, keywords = {Bisimulation, Compositional Modelling, Hybrid Automata, hybrid process algebras}, doi = {10.1007/978-3-642-04081-8_21}, author = {Vashti Galpin and Luca Bortolussi and Jane Hillston}, editor = {M. Bravetti and G. Zavattaro} } @conference {199, title = {The importance of being (a little bit) discrete}, booktitle = {Second Workshop From Biology to Concurrency and Back (FBTC 2008)}, series = {Electronic Notes In Theoretical Computer Science}, volume = {229}, year = {2009}, pages = {75{\textendash}92}, publisher = {Elsevier}, organization = {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.}, keywords = {Biological Modeling, Discreteness, Hybrid Systems, Robustness, Stochastic Noise}, doi = {10.1016/j.entcs.2009.02.006}, url = {http://www.sciencedirect.com/science/article/pii/S1571066109000115}, author = {Luca Bortolussi and Alberto Policriti}, editor = {N. Cannata and E. Merelli and I. Ulidowski} } @conference {195, title = {Stochastic Programs and Hybrid Automata for (Biological) Modeling.}, booktitle = {Computability in Europe, CiE 2009}, series = {Lecture Notes In Computer Science}, volume = {5635}, year = {2009}, month = {24, 2009}, pages = {37{\textendash}48}, publisher = {Springer}, organization = {Springer}, abstract = {We present a technique to associate to stochastic programs written in stochastic Concurrent Constraint Programming a semantics in terms of a lattice of hybrid automata. The aim of this construction is to provide a framework to approximate the stochastic behavior by a mixed discrete/continuous dynamics with a variable degree of discreteness.

}, keywords = {Hybrid Automata, Hybrid Semantics of Programming Languages, stochastic concurrent constraint programming}, doi = {10.1007/978-3-642-03073-4_5}, url = {http://www.springerlink.com/content/026g745267581425/}, author = {Luca Bortolussi and Alberto Policriti}, editor = {Klaus Ambos-Spies and Benedikt Lowe and Wolfgang Merkle} } @conference {191, title = {Tales of Spatiality in stochastic Concurrent Constraint Programming}, booktitle = {Bio Logical 2009}, year = {2009}, pages = {42{\textendash}52}, publisher = {AI*IA}, organization = {AI*IA}, abstract = {Stochastic Concurrent Constraint Programming (sCCP) extends CCP with a stochastic semantics in continuous time. As such, it can be used to model biological systems. The characterizing feature of sCCP is its flexibility, given by the computational and reasoning capabilities of the constraint store. In this paper we discuss how such features can be used to model biological systems involving different notions of spatiality, from compartmentalization to the position of each molecule.

}, keywords = {Computational Systems Biology, Dynamical compartments modelling, stochastic concurrent constraint programming}, author = {Luca Bortolussi and Alberto Policriti}, editor = {AA.VV.} } @conference {207, title = {On the Approximation of Stochastic Concurrent Constraint Programming by Master Equation}, booktitle = {Sixth International Workshop on Quantitative Aspects of Programming Languages, QAPL 2008)}, series = {Electronic Notes In Theoretical Computer Science}, volume = {220}, year = {2008}, pages = {161{\textendash}175}, publisher = {Academic Press, Elsevier}, organization = {Academic Press, 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.}, keywords = {biological systems, fluid-flow approximation, ordinary differential equations, stochastic concurrent constraint programming}, doi = {10.1016/j.entcs.2008.11.025}, url = {http://www.sciencedirect.com/science/article/pii/S1571066108004623}, author = {Luca Bortolussi}, editor = {A. Aldini and C. Baier} } @book {202, title = {Computational Systems Biology With Constraints. Stochastic modeling of biological systems with concurrent constraint programming.}, year = {2008}, publisher = {VDM Verlag Dr. Mueller e.K.}, organization = {VDM Verlag Dr. Mueller e.K.}, author = {Luca Bortolussi} } @article {201, title = {A Criterion for the Stochasticity of Matrices with Specified Order Relations}, journal = {Rendiconti dell{\textquoteright}Istituto di Matematica dell{\textquoteright}Universit{\`a} di Trieste}, volume = {40}, year = {2008}, pages = {55{\textendash}64}, abstract = {We tackle the following problem: can one replace a real matrix by a stochastic matrix without altering the order relations between entries? We state a general criterion and a convenient necessary condition. The motivation for this work resides in applications to DNA word design.}, url = {http://www.dmi.units.it/~rimut/volumi/40/04Sgarro.pdf}, author = {Luca Bortolussi and Andrea Sgarro} } @conference {205, title = {Hybrid approximation of stochastic process algebras for systems biology}, booktitle = {17th IFAC World Congress}, series = {IFAC Proceedings Volumes}, volume = {17}, year = {2008}, month = {11 July 2008}, pages = {n/a{\textendash}n/a}, publisher = {IFAC WC}, organization = {IFAC WC}, abstract = {We present a technique to approximate models of biological systems written in a "distilled" version of stochastic Concurrent Constraint Programming (sCCP), a stochastic programming methodology based on logic programming. Our technique automatically associates to a stochastic model an hybrid automaton, i.e. a dynamical system where continuous and discrete dynamics coexist. The hybrid automata generated in this way are, in certain cases, capable of capturing aspects of the dynamics of stochastic processes that are lost in approximations based solely on ordinary differential equations. In particular, they work better for those systems whose sCCP model contains explicit logical mechanisms of control. In the paper we outline the general technique to perform this association and we discuss some issues related to its applicability.}, keywords = {Approximate analysis, Computational Systems Biology, Computer simulation, Hybrid Systems, Stochastic programming}, doi = {10.3182/20080706-5-KR-1001.2419}, url = {http://www.ifac-papersonline.net/Detailed/37815.html}, author = {Luca Bortolussi and Alberto Policriti}, editor = {M J Chung and P Misra} } @conference {209, title = {Hybrid Semantics for Stochastic π-calculus}, booktitle = {Algebraic Biology, AB2008}, series = {Lecture Notes in Computer Science}, volume = {5147}, year = {2008}, month = {August 2, 2008}, pages = {40{\textendash}57}, publisher = {Heidelberg: Springer-Verlag.}, organization = {Heidelberg: Springer-Verlag.}, abstract = {We put forward a method to map stochastic pi-calculus processes in chemical ground form into hybrid automata, a class of dynamical systems with both discrete and continuous evolution. The key ingredient is the separation of control and molecular terms, which turns out to be related to the conservation properties of the system.}, keywords = {Hybrid Semantics of Programming Languages, Hybrid Systems, Stochastic pi-calculus}, doi = {10.1007/978-3-540-85101-1_4}, url = {http://www.springerlink.com/content/w30825q00815t203/}, author = {Luca Bortolussi and Alberto Policriti}, editor = {Katsuhisa Horimoto and Georg Regensburger and Markus Rosenkranz and Hiroshi Yoshida} } @inbook {208, title = {Hybrid Systems and Biology.Continuous and Discrete Modeling for Systems Biology}, booktitle = {Formal Methods For Computational System Biology}, series = {Lecture Notes in Computer Science}, volume = {5016}, year = {2008}, pages = {424{\textendash}448}, publisher = {Springer}, organization = {Springer}, author = {Luca Bortolussi and Alberto Policriti}, editor = {Bernardo M. and Degano P. and Zavattaro G.} } @conference {204, title = {HYPE Applied to the Modelling of Hybrid Biological Systems}, booktitle = {24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV)}, series = {Electronic Notes In Theoretical Computer Science}, volume = {218}, year = {2008}, pages = {33{\textendash}51}, publisher = {Elsevier}, organization = {Elsevier}, abstract = {HYPE is a process algebra developed to model hybrid systems{\quotesinglbase} 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.}, keywords = {Hybrid Systems, process algebra, Systems Biology}, doi = {10.1016/j.entcs.2008.10.004}, url = {http://www.sciencedirect.com/science/article/pii/S1571066108003988}, author = {Vashti Galpin and Luca Bortolussi and Jane Hillston}, editor = {A Bauer and M Mislove} } @conference {206, title = {Measures of fuzzy disarray in linguistic typology}, booktitle = {12th conference on Information Processing and Management of Uncertainty in Knowledge-Based Systems, IPMU 2008}, year = {2008}, month = {27 June 2008}, pages = {167{\textendash}172}, publisher = {IPMU}, organization = {IPMU}, address = {Malaga}, abstract = {We extend crisp measures of disarray to the vaguely defined context of natural languages, so as to tackle problems of linguistic typology related to the order of words. We deal both with short abstract structure of the type {\quotesinglbase}subject verb object{\quotesinglbase} and with texts in the original language and in a translation. Preliminary experimental results are provided.}, keywords = {bubble distance, fuzzy permutations, Measures of disarray, rank distance, Spearman footrule}, url = {http://www.gimac.uma.es/ipmu08/proceedings/html/023.html}, author = {Luca Bortolussi and Liviu P. Dinu and Andrea Sgarro}, editor = {L Magdalena and M Ojeda-Aciego and J L Verdegay} } @article {210, title = {Modeling Biological Systems in Stochastic Concurrent Constraint Programming}, journal = {Constraints}, volume = {13(1)}, year = {2008}, pages = {66{\textendash}90}, abstract = {We present an application of stochastic Concurrent Constraint Programming (sCCP) for modeling biological systems. We provide a library of sCCP processes that can be used to describe straightforwardly biological networks. In the meanwhile, we show that sCCP proves to be a general and extensible framework, allowing to describe a wide class of dynamical behaviours and kinetic laws.}, keywords = {Computational Modelling of Biological Systems, Continuous Time Markov Chains, stochastic concurrent constraint programming}, doi = {10.1007/s10601-007-9034-8}, url = {http://www.springerlink.com/content/pxq8473186375631/}, author = {Luca Bortolussi and Alberto Policriti} } @mastersthesis {253, title = {Constraint-based approaches to stochastic dynamics of biological systems}, volume = {PhD in Computer Science}, year = {2007}, month = {04/2007}, school = {University of Udine}, address = {Udine}, author = {Luca Bortolussi} } @conference {211, title = {Constraint-based simulation of biological systems described by Molecular Interaction Maps}, booktitle = {IEEE BIBM 2007}, year = {2007}, month = {4 november 2007}, pages = {288{\textendash}293}, publisher = {IEEE computer society}, organization = {IEEE computer society}, author = {Luca Bortolussi and Simone Fonda and Alberto Policriti} } @conference {216, title = {Constraint-based simulation of biological systems described by Molecular Interaction Maps}, booktitle = {CILC 2007}, year = {2007}, author = {Luca Bortolussi and Simone Fonda and Alberto Policriti}, editor = {G. Fiumara and M. Marchi and A. Provetti} } @conference {219, title = {Constraint-based simulation of biological systems described by Molecular Interaction Maps}, booktitle = {WCB 2007}, year = {2007}, pages = {1{\textendash}9}, author = {Luca Bortolussi and Simone Fonda and Alberto Policriti}, editor = {Rolf Backofen and Alessandro Dal Palu and Sebastian Will} } @article {213, title = {Hamming-like distances for ill-defined strings in linguistic classification}, journal = {Rendiconti dell{\textquoteright}Istituto di Matematica dell{\textquoteright}Universit{\`a} di Trieste}, volume = {39}, year = {2007}, pages = {105{\textendash}118}, abstract = {Ill-defined strings often occur in soft sciences, e.g. in linguistics or in biology. In this paper we consider l-length strings which have in each position one of the three symbols 0 or false, 1 or true, b or irrelevant. We tackle some generalisations of the usual Hamming distance between binary crisp strings which were recently used in computational linguistics. We comment on their metric properties, since these should guide the selection of the clustering algorithm to be used for language classification. The concluding section is devoted to future work, and the string approach, as currently pursued, is compared to alternative approaches.}, keywords = {Computational Linguistics, Fuzzy Distances, Hamming Distances}, url = {http://rendiconti.dmi.units.it/volumi/39/06.pdf}, author = {Luca Bortolussi and Andrea Sgarro} } @conference {215, title = {Hybrid approximation of Stochastic Concurrent Constraint Programming}, booktitle = {PASTA 2007}, year = {2007}, pages = {39{\textendash}42}, author = {Luca Bortolussi and Alberto Policriti}, editor = {A. Argent-Katwalwa} } @conference {217, title = {Maximum possibility vs. maximum likelihood decisions}, booktitle = {Linz Seminar 2007}, year = {2007}, pages = {12{\textendash}17}, author = {Luca Bortolussi and Massimo Borelli and Andrea Sgarro}, editor = {D. Dubois and E. P. Klement and R. Mesiar} } @article {220, title = {Multi-Agent Protein Structure Prediction}, journal = {Multiagent And Grid Systems}, volume = {3}, number = {2}, year = {2007}, author = {Luca Bortolussi and Agostino Dovier and Federico Fogolari} } @article {221, title = {Scoring predictive models using a reduced representation of proteins: model and energy definition}, journal = {BMC Structural Biology}, volume = {7}, number = {1}, year = {2007}, author = {Federico Fogolari and Lidia Pieri and Agostino Dovier and Luca Bortolussi and Gilberto Giuliarelli and Alessandra Corazza and Gennaro Esposito and Paolo Viglino} } @conference {214, title = {Stochastic Concurrent Constraint Programming and Differential Equations}, booktitle = {Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL 2007)}, series = {Electronic Notes In Theoretical Computer Science}, volume = {190}, year = {2007}, pages = {27{\textendash}42}, publisher = {Academic Press, Elsevier}, organization = {Academic Press, 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 ODEs 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}, keywords = {biological systems, ordinary differential equations, stochastic concurrent constraint programming, stochastic modeling}, doi = {10.1016/j.entcs.2007.07.003}, url = {http://www.sciencedirect.com/science/article/pii/S1571066107005567}, author = {Luca Bortolussi and Alberto Policriti}, editor = {A. Aldini and F. van Breugel} } @conference {231, title = {BuST-Bundled Suffix Trees}, booktitle = {IFIP conference on Theoretical Computer Science, IFIP-TCS 2006}, series = {IFIP Series}, volume = {209}, year = {2006}, month = {24 Agosto 2006}, pages = {91{\textendash}102}, publisher = {Springer Verlag}, organization = {Springer Verlag}, abstract = {We introduce a data structure, the Bundled Suffix Tree (BUST), that is a generalization of a Suffix Tree (ST). To build a BuST we use an alphabet Sigma together with a non-transitive relation R among its letters. Following the path of a substring p within a BUST, constructed over a text t of length n, not only the positions of the exact occurrences of p in t are found (as in a ST), but also the positions of all the substrings p1, p2, p3, ... that are related with p via the relation R among the characters of Sigma, for example strings at a certain distance from p. A BuST contains O(n^(1+m)) additional nodes (m < 1) in probability, and is constructed in O(n^(1+m)) steps. In the worst case it contains O(n^2) nodes.}, keywords = {Algorithms for approximate string matching, bioinformatics, data structures, Suffix Trees}, doi = {10.1007/978-0-387-34735-6_11}, url = {http://www.springerlink.com/content/c36x8230n44516u5/}, author = {Luca Bortolussi and Francesco Fabris and Alberto Policriti}, editor = {Gonzalo Navarro and Leopoldo Bertossi and Yoshiharu Kohayakawa} } @conference {225, title = {Channel Models for DNA Word Design}, booktitle = {SIMAI 2006}, year = {2006}, month = {26 May 2006}, pages = {34{\textendash}34}, publisher = {L Puccio and A Agreste and A Guido and A Vocaturo}, organization = {L Puccio and A Agreste and A Guido and A Vocaturo}, author = {Luca Bortolussi and Andrea Sgarro} } @article {230, title = {Codeword Distinguishability in Minimum Diversity Decoding}, journal = {Journal Of Discrete Mathematical Sciences And Cryptography}, volume = {9}, number = {3}, year = {2006}, pages = {487{\textendash}502}, abstract = {We 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 and codeword confusabilities. The operational meaning of codewoord distinguishability is made clear by a reliability criterion, which generalises the well-known criterion on minimum Hamming distance for error-correcting 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.}, keywords = {codeword distinguishability, Coding theory, possibility theory}, author = {Andrea Sgarro and Luca Bortolussi} } @conference {229, title = {Connecting Process Algebras and Differential Equations for Systems Biology}, booktitle = {PASTA 2006}, year = {2006}, pages = {1{\textendash}17}, publisher = {Department of Computing, Imperial College}, organization = {Department of Computing, Imperial College}, keywords = {Differential Equations, S-Systems, Stochastic process algebras}, author = {Luca Bortolussi and Alberto Policriti}, editor = {J. Bradley} } @conference {222, title = {Fuzzy Codebooks for DNA Word Design}, booktitle = {IPMU 2006}, year = {2006}, publisher = {B Bouchon-Meunier et al.}, organization = {B Bouchon-Meunier et al.}, author = {Luca Bortolussi and Andrea Sgarro} } @conference {227, title = {Modeling Biological Systems in Stochastic Concurrent Constraint Programming}, booktitle = {WCB 2006}, year = {2006}, pages = {6{\textendash}29}, publisher = {Alessandro Dal Palu and Agostino Dovier and Sebastian Will}, organization = {Alessandro Dal Palu and Agostino Dovier and Sebastian Will}, author = {Luca Bortolussi and Alberto Policriti} } @conference {226, title = {Possibilistic channels for DNA word design}, booktitle = {Soft Methods for Integrated Uncertainty Modelling}, series = {Advances in Soft Computing Series} pages = {327{\textendash}335}, year = {2006}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, author = {Luca Bortolussi and Andrea Sgarro} } @conference {224, title = {A statistical empirical energy function for proteins}, booktitle = {BITS 2006}, year = {2006}, publisher = {Societa Italiana di Bioinformatica}, organization = {Societa Italiana di Bioinformatica}, keywords = {Energy Function for Proteins, Protein Structure Prediction}, author = {Federico Fogolari and Lidia Pieri and Luca Bortolussi and Agostino Dovier}, editor = {R Casadio et al.} } @conference {228, title = {Stochastic Concurrent Constraint Programming}, booktitle = {4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006)}, series = {Electronic Notes In Theoretical Computer Science}, volume = {164}, year = {2006}, pages = {65{\textendash}80}, publisher = {Academic Press, Elsevier}, organization = {Academic Press, Elsevier}, 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.}, keywords = {Concurrent Constraint Programming, Continuous Time Markov Chains, Probabilistic Semantics, Stochastic Languages}, doi = {10.1016/j.entcs.2006.07.012}, url = {http://www.sciencedirect.com/science/article/pii/S1571066106004919}, author = {Luca Bortolussi}, editor = {A Di Pierro and H Wiklicky} } @article {244, title = {Agent-based Protein Folding Simulation}, journal = {Intelligenza Artificiale}, year = {2005}, author = {Luca Bortolussi and Alessandro Dal Palu and Agostino Dovier and Federico Fogolari} } @conference {236, title = {Bundled Suffix Trees}, booktitle = {BITS 2005}, year = {2005}, month = {19 March 2005}, publisher = {Societa Italiana di Bioinformatica}, organization = {Societa Italiana di Bioinformatica}, keywords = {String Algorithms, Suffix Trees}, author = {Luca Bortolussi and Francesco Fabris and Alberto Policriti}, editor = {L Milanesi et al.} } @conference {242, title = {Concurrent Methodologies for Global Optimization}, booktitle = {21st International Conference Logic Programming (ICLP 2005)}, series = {Lecture Notes In Computer Science}, volume = {3368}, year = {2005}, month = {5, 2005}, pages = {441{\textendash}443}, publisher = {Heidelberg: Springer-Verlag.}, organization = {Heidelberg: Springer-Verlag.}, keywords = {Multi agent Optimization, Optimization Metaheuristic, Protein Structure Prediction}, doi = {10.1007/11562931_47}, url = {http://www.springerlink.com/content/bc53eek18y979axn/}, author = {Luca Bortolussi}, editor = {Maurizio Gabbrielli and Gopal Gupta} } @conference {240, title = {Constraint Satisfaction Problems on DNA Strings}, booktitle = {WCB 2005}, year = {2005}, pages = {11{\textendash}18}, publisher = {Rolf Backofen and Agostino Dovier}, organization = {Rolf Backofen and Agostino Dovier}, author = {Luca Bortolussi and Andrea Sgarro} } @conference {241, title = {A Distributed and Probabilistic Concurrent Constraint Programming Language}, booktitle = {21st International Conference Logic Programming (ICLP 2005)}, series = {Lecture Notes In Computer Science}, volume = {3368}, year = {2005}, month = {5, 2005.}, pages = {143{\textendash}158}, publisher = {Heidelberg: Springer-Verlag.}, organization = {Heidelberg: Springer-Verlag.}, abstract = {We present a version of the CCP paradigm, which is both distributed and probabilistic. We consider networks with a fixed number of nodes, each of them possessing a local and independent constraint store. While locally the computations evolve asynchronously, following the usual rules of (probabilistic) CCP, the communications among different nodes are synchronous. There are channels, and through them different objects can be exchanged: constraints, agents and channel themselves. In addition, all this activities are embedded in a probabilistic scheme based on a discrete model of time, both locally and globally. Finally we enhance the language with the capability of performing an automatic remote synchronization of variables belonging to different constraint stores.}, keywords = {Concurrent Constraint Programming, Distributed Programming Languages, Probabilistic Languages}, doi = {10.1007/11562931_13}, url = {http://www.springerlink.com/content/1g26vvlujfm0neua/}, author = {Luca Bortolussi and Herbert Wiklicky}, editor = {Maurizio Gabbrielli and Gopal Gupta} } @conference {239, title = {Multi-Agent Simulation of Protein Folding}, booktitle = {MAS-BIOMED 2005}, year = {2005}, pages = {91{\textendash}106}, publisher = {G Armano et al.}, organization = {G Armano et al.}, author = {Luca Bortolussi and Agostino Dovier and Federico Fogolari} } @conference {233, title = {Constraint-based tools for protein folding}, booktitle = {CILC 2004}, year = {2004}, month = {17 June 2004}, pages = {365{\textendash}367}, publisher = {Universita di Parma}, organization = {Universita di Parma}, keywords = {Constraint Programming, Protein Structure Prediction}, author = {Luca Bortolussi and Alessandro Dal Palu and Agostino Dovier}, editor = {E Panegai and G Rossi} } @conference {232, title = {Fuzzy Integrals and Error Correction in a Telephone Network with Sensitive Users}, booktitle = {IPMU 2004}, year = {2004}, pages = {1503{\textendash}1508}, publisher = {B Bouchon-Meunier et al.}, organization = {B Bouchon-Meunier et al.}, author = {Luca Bortolussi and Andrea Sgarro} } @article {243, title = {Fuzzy Possibilities as Upper Previsions}, journal = {International Journal Of Uncertainty, Fuzziness And Knowledge Based Systems}, volume = {12}, number = {5}, year = {2004}, pages = {559{\textendash}574}, author = {Luca Bortolussi and Paolo Vicig} } @conference {238, title = {Protein Folding Simulation in CCP}, booktitle = {2nd Workshop On Concurrent Models In Molecular Biology, BIOCONCUR 2004}, year = {2004}, pages = {110{\textendash}123}, publisher = {A Ingolfsfottir and H Riis Nielson}, organization = {A Ingolfsfottir and H Riis Nielson}, author = {Luca Bortolussi and Alessandro Dal Palu and Agostino Dovier and Federico Fogolari} } @conference {237, title = {Protein Folding Simulation in CCP}, booktitle = {AI*IA 2004}, year = {2004}, month = {17 September 2004}, pages = {86{\textendash}86}, publisher = {Morlacchi Editore}, organization = {Morlacchi Editore}, author = {Luca Bortolussi and Alessandro Dal Palu and Agostino Dovier and Federico Fogolari} } @booklet {234, title = {Fuzzy Possibilities as Upper Previsions}, volume = {4}, year = {2003}, pages = {1{\textendash}18}, abstract = {Tech Report}, keywords = {Fuzzy Possibilities, Fuzzy Sets, Possiblity Theory}, author = {Luca Bortolussi and Paolo Vicig} } @conference {258, title = {On the Robustness of Temporal Properties for Stochastic Models}, booktitle = {2nd International Workshop on Hybrid Systems and Biology, HSB 2013}, volume = {125}, year = {2003}, pages = {3-19}, publisher = {Open Publishing Association}, organization = {Open Publishing Association}, edition = {EPTCS}, address = {Taormina, Italy}, abstract = {Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem. i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to mantain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification com- munity have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness scores. By discussing two examples, we show how to approximate the distribution of the robustness score and its key indicators: the average robustness and the conditional average robustness. Secondly, we show how to combine these indicators with the satisfaction probability to address the system design problem, where the goal is to optimize some control parameters of a stochastic model in order to best maximize robustness of the desired specifications.

}, keywords = {Computational Systems Biology, Continuous Time Markov Chains, Gaussian Process Optimisation, Robust Semantics, Signal Temporal Logic, stochastic hybrid systems, System Design}, doi = {10.4204/EPTCS.125.1}, url = {http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?HSB2013.1}, author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi and Guido Sanguinetti} }