arXiv subjects

Sean Sedwards

Publications and source records attributed to Sean Sedwards.

27 records · Page 2Linked to original sources

arXiv2017

A Hierarchy of Scheduler Classes for Stochastic Automata

Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata.

cs.LO↗

arXiv2015

Distributed Verification of Rare Properties using Importance Splitting Observers

Rare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance splitting make it appealing for SMC, but optimising its performance in the standard way makes distribution inefficient. We show how it is possible to achieve equivalently good results in less time by distributing simpler algorithms. We first explore the challenges posed by importance splitting and present an algorithm optimised for distribution. We then define a specific bounded time logic that is compiled into memory-efficient observers to monitor executions. Finally, we demonstrate our framework on a number of challenging case studies.

cs.LO↗

arXiv2015

Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards

Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightweight approximative techniques that sample directly from scheduler space, bringing the prospect of scalable alternatives to standard numerical model checking algorithms. The focus so far has been on optimising the probability of a property, but many problems require quantitative analysis of rewards. In this work we therefore present lightweight statistical model checking algorithms to optimise the rewards of Markov decision processes. We consider the standard definitions of rewards used in model checking, introducing an auxiliary hypothesis test to accommodate reachability rewards. We demonstrate the performance of our approach on a number of standard case studies.

cs.LO↗

arXiv2015

Smart Sampling for Lightweight Verification of Markov Decision Processes

Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe "smart" sampling algorithms that can make substantial improvements in performance.

cs.DS↗

arXiv2014

Scalable Verification of Markov Decision Processes

Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification.

cs.DS↗

arXiv2013

Cooperation and competition in the dynamics of tissue architecture during homeostasis and tumorigenesis

The construction of a network of cell-to-cell contacts makes it possible to characterize the patterns and spatial organisation of tissues. Such networks are highly dynamic, depending on the changes of the tissue architecture caused by cell division, death and migration. Local competitive and cooperative cell-to-cell interactions influence the choices cells make. We review the literature on quantitative data of epithelial tissue topology and present a dynamical network model that can be used to explore the evolutionary dynamics of a two dimensional tissue architecture with arbitrary cell-to-cell interactions. In particular, we show that various forms of experimentally observed types of interactions can be modelled using game theory. We discuss a model of cooperative and non-cooperative cell-to-cell communication that can capture the interplay between cellular competition and tissue dynamics. We conclude with an outlook on the possible uses of this approach in modelling tumorigenesis and tissue homeostasis.

q-bio.TO↗

arXiv2012

Statistical Model Checking for Stochastic Hybrid Systems

This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We report on two applications of the resulting tool-set coming from systems biology and energy aware buildings.

cs.CE↗

arXiv2012

Cross-entropy optimisation of importance sampling parameters for statistical model checking

Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating properties from multiple executions of a system and by giving results within confidence bounds. Rare properties are often very important but pose a particular challenge for simulation-based approaches, hence a key objective under these circumstances is to reduce the number and length of simulations necessary to produce a given level of confidence. Importance sampling is a well-established technique that achieves this, however to maintain the advantages of statistical model checking it is necessary to find good importance sampling distributions without considering the entire state space. Motivated by the above, we present a simple algorithm that uses the notion of cross-entropy to find the optimal parameters for an importance sampling distribution. In contrast to previous work, our algorithm uses a low dimensional vector of parameters to define this distribution and thus avoids the often intractable explicit representation of a transition matrix. We show that our parametrisation leads to a unique optimum and can produce many orders of magnitude improvement in simulation efficiency. We demonstrate the efficacy of our methodology by applying it to models from reliability engineering and biochemistry.

cs.PF↗

arXiv2011

Prosperity is associated with instability in dynamical networks

Social, biological and economic networks grow and decline with occasional fragmentation and re-formation, often explained in terms of external perturbations. We show that these phenomena can be a direct consequence of simple imitation and internal conflicts between 'cooperators' and 'defectors'. We employ a game-theoretic model of dynamic network formation where successful individuals are more likely to be imitated by newcomers who adopt their strategies and copy their social network. We find that, despite using the same mechanism, cooperators promote well-connected highly prosperous networks and defectors cause the network to fragment and lose its prosperity; defectors are unable to maintain the highly connected networks they invade. Once the network is fragmented it can be reconstructed by a new invasion of cooperators, leading to the cycle of formation and fragmentation seen, for example, in bacterial communities and socio-economic networks. In this endless struggle between cooperators and defectors we observe that cooperation leads to prosperity, but prosperity is associated with instability. Cooperation is prosperous when the network has frequent formation and fragmentation.

q-bio.PE↗