Jeremy Bradley: Selected Publications with Abstracts


Journal Articles
Distributed Computation of Transient State Distributions and Passage Time Quantiles in Large Semi-Markov Models
Reference: J T Bradley, N J Dingle, P G Harrison, W J Knottenbelt. Distributed Computation of Transient State Distributions and Passage Time Quantiles in Large Semi-Markov Models. Future Generation Computer Systems, 22(7), pp. 828-837, Elsevier, August, 2006.
Abstract: Semi-Markov processes (SMPs) are expressive tools for modelling parallel and distributed systems; they are a generalisation of Markov processes that allow for arbitrarily distributed sojourn times. This paper presents an iterative technique for transient and passage time analysis of large structurally unrestricted semi-Markov processes. Our method is based on the calculation and subsequent numerical inversion of Laplace transforms and is amenable to a highly scalable distributed implementation. Results for a distributed voting system model with up to 1.1 million states are presented and validated against simulation.
Paper: 2006-bradley-1.ps.gz 290456 bytes
Iterative Convergence of Passage-time Densities in Semi-Markov Performance Models
Reference: J T Bradley, H J Wilson. Iterative Convergence of Passage-time Densities in Semi-Markov Performance Models. Performance Evaluation, 60(1-4), pp. 237-254, Elsevier, April, 2005.
Abstract: Passage-time densities are important for the detailed performance analysis of distributed computer and communicating systems. We provide a proof and demonstration of a practical iterative algorithm for extracting complete passage-time densities from expressive semi-Markov systems. We end by showing its application to a distributed web-server cluster model of 15.9 million states.
Paper: 2004-bradley-3.ps.gz 257763 bytes
Semi-Markov PEPA: Modelling with Generally Distributed Actions
Reference: J T Bradley. Semi-Markov PEPA: Modelling with Generally Distributed Actions. International Journal of Simulation, 6(3-4), pp. 43-51, February, 2005.
Abstract: Since the advent of Markovian Process Algebras, users have requested the ability to employ a greater variety of action distribution. We present a conservative extension to the popular Markovian process algebra, PEPA, which incorporates generally distributed sojourn-times for action duration. Just as a PEPA model generates a Markov chain for analysis purposes, so semi-Markov PEPA produces a semi-Markov chain. We discuss how semi-Markov PEPA models are analysed through Dingle and Knottenbelt's semi-Markov DNAmaca tool and present a small example for passage time analysis.
Paper: 2005-bradley-0.ps.gz 566093 bytes
Stochastic Analysis of Scheduling Strategies in a Grid-based Resource Model
Reference: N A Thomas, J T Bradley, W J Knottenbelt. Stochastic Analysis of Scheduling Strategies in a Grid-based Resource Model. IEE Software Engineering, 151(5), pp. 232-239, IEE, September, 2004.
Abstract: In this paper, we consider a model inspired by a scenario found in Grid-based scheduling systems. Scheduling is performed remotely without access to up-to-date resource availability and usage information. We model this system as a collection of queues where servers break down and are subsequently repaired. There is a delay before the scheduler learns of failures, as such requests may continue to arrive into a resource queue for some time after active service has ceased. We consider the queues to be persistent under failure, however these queues have finite capacity; therefore there is the possibility that queues become full, causing job-loss. We use stochastic process algebra and stochastic probes to analyse this model to find steady state measures and passage time distributions. The effect of the duration of any delay on information propagation on the system response time and job loss is investigated and evaluated numerically.
Paper: 2004-thomas-1.ps.gz 62231 bytes
Hypergraph-based Parallel Computation of Passage Time Densities in Large Semi-Markov Models
Reference: J T Bradley, N J Dingle, W J Knottenbelt, H J Wilson. Hypergraph-based Parallel Computation of Passage Time Densities in Large Semi-Markov Models. Linear Algebra and its Applications, vol. 386, pp. 311-334, Elsevier, July, 2004.
Abstract: Passage time densities and quantiles are important performance and quality of service metrics, but their numerical derivation is, in general, computationally expensive. We present an iterative algorithm for the calculation of passage time densities in semi-Markov models, along with a theoretical analysis and empirical measurement of its convergence behaviour. In order to implement the algorithm efficiently in parallel, we use hypergraph partitioning to minimise communication between processors and to balance workloads. This enables the analysis of models with very large state spaces which could not be held within the memory of a single machine. We produce passage time densities and quantiles for very large semi-Markov models with over 15 million states and validate the results against simulation.
Paper: 2004-bradley-1.pdf 522860 bytes
An approximate solution of PEPA models using component substitution
Reference: N Thomas, J T Bradley, D J Thornley. An approximate solution of PEPA models using component substitution. Computers and Digital Techniques, 150(2), pp. 67-74, IEE, March, 2003.
Abstract: Performance models specified using compositional algebra suffer the well-known state space explosion problem, where a relatively small definition leads to a Markov chain with a large state space that is problematic to solve. As a result it is widely recognised that the development of techniques to solve performance models efficiently is of particular practical importance. Recently the notion of behavioural independence was introduced to exploit the structure of Markovian process algebra models in order to solve models in a compositional manner. The opposite property, namely control, is now used to solve models by substituting components in the model with simpler versions. The approach is validated through two examples and by deriving a variety of performance measures.
Paper: 2003-thomas-0.pdf 1866089 bytes
Countless Simson Line Configurations
Reference: C J Bradley, J T Bradley. Countless Simson Line Configurations. The Mathematical Gazette, 80(488), pp. 314-321, July, 1996.
Abstract: The Simson line property is normally associated with points on the circumcircle of a triangle. It is embodied by the following theorem. Given any triangle ABC and a point P in the plane of the triangle, if perpendiculars from P on to the sides BC, CA, AB meet those sides at L, M, N respectively then L, M, N are collinear if and only if P lies on the circumcircle of triangle ABC. The line LMN is then known as the Simson line of P. It is the word perpendicular that gives the impression that this type of configuration is somehow particular and that the Simson line property is not therefore capable of generalization. In this article we show that this is not the case and we demonstrate that the above theorem is simply one case of a more general theorem. Indeed it turns out that every transversal of a triangle is a Simson line in a more general sense, and we show how to associate these transversals with different configurations.
Paper: 1996-bradley-0.ps.gz 171536 bytes
International Conferences
Performance Trees: A New Approach to Quantitative Performance Specification
Reference: T Suto, J T Bradley W J Knottenbelt. Performance Trees: A New Approach to Quantitative Performance Specification. In MASCOTS'06, Proceedings of the 14th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunications Systems, IEEE Computer Society, Monterey, September, 2006.
Abstract: We introduce Performance Trees, a novel representation formalism for the specification of model-based performance queries. Traditionally,stochastic logics have been the prevalent means of performance requirement expression; however, in practice, their use amongst system designers is limited on account of their inherent complexity and restricted expressive power. Performance Trees are a more accessible alternative, in which performance queries are represented by hierarchical tree structures. This allows for the convenient visual composition of complex performance questions, and enables not only the verification of stochastic requirements, but also the direct extraction of performance measures. In addition, Performance Trees offer a superset of the expressiveness of Continuous Stochastic Logic (CSL) since all CSL formulae can be translated into our representation. Performance Trees can be used to represent passage time, transient,steady-state and higher order queries of varying levels of sophistication. While they are conceptually independent of the underlying stochastic modelling formalism, in many cases the tree operators we use are already backed up by good algorithmic and tool support for both stochastic verification and performance measure extraction. We do not therefore perceive major barriers to the integration of Performance Trees into existing stochastic model checking tools. Indeed, we illustrate how semi-Markov passage time computation algorithms, based on numerical Laplace transform inversion,can be directly applied to the resolution of a case study Performance Tree query.
Paper: not available
Functional Performance Specification with Stochastic Probes
Reference: A Argent-Katwala, J T Bradley. Functional Performance Specification with Stochastic Probes. In EPEW'06, Proceedings of the 3rd European Performance Evaluation Workshop, Miklos Telek (Ed.), Lecture Notes in Computer Science, vol. 4054, pp. 31-46, Springer-Verlag, Budapest, June, 2006.
Abstract: In this paper, we introduce FPS, a mechanism to define performance measures for stochastic process algebra models. FPS is a functional performance specification language which describes passage-time, transient, steady-state and continuous state space performance questions. We present a generalisation of stochastic probes, a formalism-independent specification of behaviour in stochastic process algebra models. Stochastic probes select the performance-critical paths for which the measures are required; increasing their expressiveness in turn gives us greater expressive power to represent performance questions. We end by demonstrating these tools on an RSS syndication architecture of up to 1.5 x 10^51 states.
Paper: 2006-argent-katwala-0.pdf 263730 bytes
Performance analysis of Stochastic Process Algebra models using Stochastic Simulation
Reference: J T Bradley, S T Gilmore, N A Thomas. Performance analysis of Stochastic Process Algebra models using Stochastic Simulation. In PMEO-PDS'06, Proceedings of Performance Modelling, Evaluation and Optimization of Parallel and Distributed Systems 2006, M Ould-Khaoua, G Min (Eds.), pp. 321, IEEE Computer Society Press, Rhodes, April, 2006.
Abstract: We present a translation of a generic stochastic process algebra model into a form suitable for stochastic simulation. By systematically generating rate equations from a process description, we can use tools developed for chemical and biochemical reaction analysis to provide time-series output for models with state spaces of O(10^10000) and beyond. We apply these techniques to a significant case study: that of a secure electronic voting protocol.
Paper: 2006-bradley-3.ps.gz 86865 bytes
Slides: 2006-bradley-3.slides.pdf 233224 bytes
Observing Internet Worm and Virus Attacks with a Small Network Telescope
Reference: U Harder, M W Johnson, J T Bradley, W J Knottenbelt. Observing Internet Worm and Virus Attacks with a Small Network Telescope. In PASM'05, Proceedings of the 2nd Workshop on Practical Applications of Stochastic Modelling, Nigel Thomas (Ed.), pp. 113-126, Newcastle, July, 2005.
Abstract: A network telescope is a portion of the IP address space which is devoted to observing inbound internet traffic. The purpose of a network telescope is to detect and log malicious traffic which originates from internet worms and viruses. In this paper, we investigate the statistical properties of observed traffic from a Class C telescope over a total of 3 months. We observe that only a few IP sources and destination ports are responsible for the majority of the traffic. We also demonstrate various ways to visualise the traffic profile from a telescope. We show that specific profiles can identify and distinguish portscans, hostscans and distributed denial-of-service (DDOS) attacks. Looking at the inter-arrival time of packets, the power spectrum and the detrended fluctuation analysis of the observed traffic, we show that there is very little sign of long range dependence. This is in stark contrast to other network traffic and presents exciting possibilities for identifying malicious traffic purely from its traffic profile.
Paper: 2005-harder-0.ps.gz 356084 bytes
Stochastic simulation methods applied to a secure electronic voting model
Reference: J T Bradley, S T Gilmore. Stochastic simulation methods applied to a secure electronic voting model. In PASM'05, Proceedings of the 2nd Workshop on Practical Applications of Stochastic Modelling, Nigel Thomas (Ed.), pp. 127-149, Newcastle, July, 2005.
Abstract: We demonstrate a novel simulation technique for analysing large stochastic process algebra models, applying this to a secure electronic voting system example. By approximating the discrete state space of a PEPA model by a continuous equivalent, we can draw on rate equation simulation techniques from both chemical and biological modelling to avoid having to directly enumerate the huge state spaces involved. We use stochastic simulation techniques to provide traces of course-of-values time series representing the number of components in a particular state. Using such a technique we can get simulation results for models exceeding 10^10000 states within only a few seconds.
Paper: 2005-bradley-2.ps.gz 288576 bytes
Hypergraph Partitioning for Faster Parallel PageRank Computation
Reference: J T Bradley, D de Jager, W J Knottenbelt, A Trifunovic. Hypergraph Partitioning for Faster Parallel PageRank Computation. In EPEW'05, Proceedings of the 2nd European Performance Evaluation Workshop, Leila Kloul (Ed.), Lecture Notes in Computer Science, vol. 3670, pp. 155-171, Springer-Verlag, September, 2005.
Abstract: The PageRank algorithm is used by search engines such as Google to order web pages. It uses an iterative numerical method to compute the maximal eigenvector of a transition matrix derived from the web's hyperlink structure and a user-centred model of web-surfing behaviour. As the web has expanded and as demand for user-tailored web page ordering metrics has grown, scalable parallel computation of PageRank has become a focus of considerable research effort. In this paper, we seek a scalable problem decomposition for parallel PageRank computation, through the use of state-of-the-art hypergraph-based partitioning schemes. These have not been previously applied in this context. We consider both one and two-dimensional hypergraph decomposition models. Exploiting the recent availability of the Parkway 2.1 parallel hypergraph partitioner, we present empirical results on a gigabit PC cluster for three publicly available web graphs. Our results show that hypergraph-based partitioning substantially reduces communication volume over conventional partitioning schemes (by up to three orders of magnitude), while still maintaining computational load balance. They also show a halving of the per-iteration runtime cost when compared to the most effective alternative approach used to date.
Paper: 2005-bradley-1.ps.gz 91864 bytes
The ipc/HYDRA Tool Chain for the Analysis of PEPA Models
Reference: J T Bradley, W J Knottenbelt. The ipc/HYDRA Tool Chain for the Analysis of PEPA Models. In QEST'04, Proceedings of the 1st IEEE Conference on the Quantitative Evaluation of Systems, Boudewijn Haverkort et al (Ed.), pp. 334-335, IEEE Computer Society Press, University of Twente, Enschede, September, 2004.
Abstract: PEPA is a popular stochastic process algebra and a powerful formalism for describing performance models of communication and computer systems. We augment the current state-of-the-art in the analysis of PEPA models by presenting a tool set that can not only perform steady-state and transient analysis, but also response time analysis. Response time densities and quantiles are important performance metrics which are used to specify service level agreements (SLAs) and benchmarks. HYDRA is a tool specialising in response time analysis of large Markov systems based on stochastic Petri nets. By using the Imperial PEPA compiler (\ipc), we can generate a HYDRA model from a PEPA model and obtain steady-state, transient and response time measures based on the original PEPA description.
Paper: 2004-bradley-5.ps.gz 47130 bytes
Slides: 2004-bradley-5.slides.pdf 448470 bytes
How Synchronisation Strategy Approximation in PEPA Implementations affects Passage Time Performance Results
Reference: J T Bradley, S T Gilmore, N A Thomas. How Synchronisation Strategy Approximation in PEPA Implementations affects Passage Time Performance Results. In EPEW'04, Proceedings of the European Performance Evaluation Workshop, Manuel Nunez et al (Ed.), Lecture Notes in Computer Science, vol. 3236, pp. 128-142, Springer-Verlag, October, 2004.
Abstract: Passage time densities are useful performance measurements in stochastic systems. With them the modeller can extract probabilistic quality-of-service guarantees such as: the probability that the time taken for a network header packet to travel across a heterogeneous network is less than 10ms must be at least 0.95. In this paper, we show how new tools can extract passage time densities and distributions from stochastic models defined in PEPA, a stochastic process algebra. In stochastic process algebras, the synchronisation policy is important for defining how different system components interact. We also show how these passage time results can vary according to which synchronisation strategy is used. We compare results from two popular strategies.
Paper: 2004-bradley-4.ps.gz 65468 bytes
Slides: 2004-bradley-4.slides.pdf 637143 bytes
Expressing Performance Requirements using Regular Expressions to specify Stochastic Probes over Process Algebra Models
Reference: A Argent-Katwala, J T Bradley, N J Dingle. Expressing Performance Requirements using Regular Expressions to specify Stochastic Probes over Process Algebra Models. In WOSP'04, Proceedings of the 4th International Workshop on Software and Performance, Virigilio Almeida, Doug Lea (Eds.), pp. 49-58, ACM, Redwood City, California, January, 2004.
Abstract: This paper describes how soft performance bounds can be expressed for software systems using stochastic probes over stochastic process algebra models. These stochastic probes are specified using a regular expression syntax that describes the behaviour that must be observed in a model before a performance measurement can be started or stopped. We demonstrate the use of stochastic probes on a 661,960 state parallel, redundant web server model to verify its passage-time performance characteristics.
Paper: 2004-bradley-0.ps.gz 116669 bytes
Slides: 2004-bradley-0.slides.ps.gz 1277511 bytes
Derivation of Passage-time Densities in PEPA Models using ipc: the Imperial PEPA Compiler
Reference: J T Bradley, N J Dingle, S T Gilmore, W J Knottenbelt. Derivation of Passage-time Densities in PEPA Models using ipc: the Imperial PEPA Compiler. In MASCOTS'03, Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunications Systems, Gabriele Kotsis (Ed.), pp. 344-351, IEEE Computer Society Press, University of Central Florida, October, 2003.
Abstract: We present a technique for defining and extracting passage-time densities from high-level stochastic process algebra models. Our high-level formalism is PEPA, a popular Markovian process algebra for expressing compositional performance models. We introduce ipc, a tool which can process PEPA-specified passage-time densities and models by compiling the PEPA model and passage specification into the DNAmaca formalism. DNAmaca is an established modelling language for the low-level specification of very large Markov and semi-Markov chains. We provide performance results for ipc/DNAmaca and comparisons with another tool which supports PEPA, PRISM. Finally, we generate passage-time densities and quantiles for a case study of a high-availability web server.
Paper: 2003-bradley-6.ps.gz 54280 bytes
Slides: 2003-bradley-6.slides.ps.gz 3514188 bytes
Hypergraph-based Parallel Computation of Passage Time Densities in Large Semi-Markov Models
Reference: J T Bradley, N J Dingle, W J Knottenbelt, H J Wilson. Hypergraph-based Parallel Computation of Passage Time Densities in Large Semi-Markov Models. In NSMC'03, Proceedings of the 4th International Workshop on Numerical Solutions of Markov Chains, Amy N Langville, William J Stewart (Eds.), pp. 99-120, University of Illinois at Urbana-Champaign, September, 2003.
Abstract: Passage time densities and quantiles are important performance and quality of service metrics, but their numerical derivation is, in general, computationally expensive. We present an iterative algorithm for the calculation of passage time densities in structurally unrestricted semi-Markov models, along with a theoretical analysis and empirical measurement of its convergence behaviour. In order to implement the algorithm efficiently in parallel, we use hypergraph partitioning to minimise communication between processors and to balance workloads. This enables the analysis of models with very large state spaces which could not be held within the memory of a single machine. We produce passage time densities and quantiles for very large semi-Markov models with over 15 million states and validate the results against simulation.
Paper: 2003-bradley-4.ps.gz 379297 bytes
Slides: 2003-bradley-4.slides.pdf 3714806 bytes
Performance Queries on Semi-Markov Stochastic Petri Nets with an Extended Continuous Stochastic Logic
Reference: J T Bradley, N J Dingle, W J Knottenbelt, P G Harrison. Performance Queries on Semi-Markov Stochastic Petri Nets with an Extended Continuous Stochastic Logic. In PNPM'03, Proceedings of Petri Nets and Performance Models, Gianfranco Ciardo, William Sanders (Eds.), pp. 62-71, IEEE Computer Society, University of Illinois at Urbana-Champaign, September, 2003.
Abstract: Semi-Markov Stochastic Petri Nets (SM-SPNs) are a high-level formalism for defining semi-Markov processes. We present an extended Continuous Stochastic Logic (eCSL) which provides an expressive way to articulate performance queries at the SM-SPN model level. eCSL supports queries involving steady-state, transient and passage time measures. We demonstrate this by formulating and answering eCSL queries on an SM-SPN model of a distributed voting system with up to 10^7 states.
Paper: 2003-bradley-3.ps.gz 244042 bytes
Slides: 2003-bradley-3.slides.ps.gz 1392004 bytes
Strategies for Exact Iterative Aggregation of Semi-Markov Performance Models
Reference: J T Bradley, N J Dingle, W J Knottenbelt. Strategies for Exact Iterative Aggregation of Semi-Markov Performance Models. In SPECTS'03, Proceedings of International Symposium on Performance Evaluation of Computer and Telecommunication Systems, M S Obaidat (Ed.), pp. 755-762, SCS, Montreal, July, 2003.
Abstract: Semi-Markov models provide the modeller with more expressive distribution-types with which to describe their model. However, state-space growth is as much a problem in this paradigm as with Markovian modelling. This paper describes an exact iterative aggregation process for semi-Markov models. We discover that the computational complexity of the aggregation method critically depends on the order in which the states are aggregated. We further investigate different state-ordering strategies and find one that delays the computational explosion until late in the process. This gives us the opportunity to aggregate a large proportion of the state-space at minimal cost and leave us with a significantly smaller model to analyse for performance-related quantities such as passage-time quantiles and transient distributions. Ultimately, we demonstrate the practicality of the aggregation technique on several examples: including a 540,000 state model which reduces to a model of 170,000 states after aggregation.
Paper: 2003-bradley-2.ps.gz 339705 bytes
Slides: 2003-bradley-2.slides.ps.gz 1615283 bytes
Distributed Computation of Passage Time Quantiles and Transient State Distributions in Large Semi-Markov Models
Reference: J T Bradley, N J Dingle, P G Harrison, W J Knottenbelt. Distributed Computation of Passage Time Quantiles and Transient State Distributions in Large Semi-Markov Models. In PMEO-PDS'03, Proceedings of Performance Modelling, Evaluation and Optimization of Parallel and Distributed Systems 2003, Mohamed Ould-Khaoua (Ed.), pp. 281, IPDPS 2003 Workshops, IEEE Computer Society Press, Nice, April, 2003.
Abstract: Semi-Markov processes (SMPs) are expressive tools for modelling concurrent systems; they are a generalisation of Markov processes that allow for arbitrarily distributed sojourn times. This paper presents an iterative technique for passage time and transient analysis of large structurally unrestricted semi-Markov processes. Our method is based on the calculation and subsequent numerical inversion of Laplace transforms and is amenable to a highly scalable distributed implementation. Results for a distributed voting system model with up to 1.1 million states are presented and compared against simulation.
Paper: 2003-bradley-0.ps.gz 277449 bytes
A Passage-time Preserving Equivalence for Semi-Markov Processes
Reference: J T Bradley. A Passage-time Preserving Equivalence for Semi-Markov Processes. In TOOLS'02, Proceedings of Computer Performance Evaluation: Modelling Techniques and Tools, Field, A J et al (Ed.), Lecture Notes in Computer Science, vol. 2324, pp. 178-187, Springer-Verlag, Imperial College, London, April, 2002.
Abstract: An equivalence for semi-Markov processes is presented which preserves passage-time distributions between pairs of states in a given set. The equivalence is based upon a state-based aggregation procedure which is O(n^2) per state in the worst case.
Paper: 2002-bradley-1.ps.gz 193092 bytes
Putting Quality of Service into a Network by making the Traffic Markovian
Reference: J T Bradley, N Thomas. Putting Quality of Service into a Network by making the Traffic Markovian. In ESM'01, Proceedings of the Fifteenth European Simulation Multiconference, E J H Kerckhoffs, M Snorek (Eds.), pp. 746-750, SCS, Prague, June, 2001.
Abstract: In this paper we examine an existing model of composable internet switches from which statistical guarantees of service can be obtained. We then present some small analysis to show how the model can be implemented so that its assumptions, in this case about Markovian traffic streams, are in fact properties of the implementation. In order to achieve this we need to construct a box which makes the traffic streams Markovian.
Paper: 2001-bradley-0.ps.gz 236159 bytes
Two Solution Methods for Models of Parallel Queues
Reference: N Thomas, J T Bradley. Two Solution Methods for Models of Parallel Queues. In ESM'01, Proceedings of the Fifteenth European Simulation Multiconference, E J H Kerckhoffs, M Snorek (Eds.), pp. 741-745, SCS, Prague, July, 2001.
Abstract: A class of queueing models is considered here which in general do not give rise to a product from solution but can nevertheless be decomposed into their components, subject to a property referred to as quasi-separability. Such a decomposition gives rise to expressions for marginal probabilities which may be used to derive potentially interesting system performance measures,such as average number of jobs in a system. In this paper a simple approximation for the variance of a state of a system of quasi-separable components is presented and compared with an alternative method of approximate solution.
Paper: 2001-thomas-0.pdf 209423 bytes
A Matrix-based Method for Analysing Stochastic Process Algebras
Reference: J T Bradley, N J Davies. A Matrix-based Method for Analysing Stochastic Process Algebras. In PAPM'00, Proceedings of the 8th International Workshop on Process Algebra and Performance Modelling, J D P Rolim (Ed.), pp. 579-590, ICALP Workshops, Carleton Scientific, Geneva, July, 2000.
Abstract: This paper demonstrates how three stochastic process algebras can be mapped on to a generally-distributed stochastic transition system. We demonstrate an aggregation technique on these stochastic transition systems and show how this can be implemented as a matrix-analysis method for finding steady-state distributions. We verify that the time complexity of the algorithm is a considerable improvement upon a previous method and discuss how the technique can be used to generate partial steady-state distributions for SPA systems.
Paper: 2000-bradley.ps.gz 94080 bytes
Approximating variance in non-product form decomposed models
Reference: N Thomas, J T Bradley. Approximating variance in non-product form decomposed models. In PAPM'00, Proceedings of the 8th International Workshop on Process Algebra and Performance Modelling, J D P Rolim (Ed.), pp. 607-619, ICALP Workshops, Carleton Scientific, Geneva, July, 2000.
Abstract: A class of models is considered here which do not give rise to a product from solution but can nevertheless be decomposed into their components, subject to a property referred to as quasi-separability. Such a decomposition gives rise to expressions for marginal probabilities which may be used to derive potentially interesting system performance measures, such as the average state of the system. It is very important that some degree of confidence in such measures can also be given, however, we show here that it is not generally possible to calculate the variance exactly from the marginal probabilities. In this paper a simple approximation for the variance of the state a system of quasi-separable components is presented and evaluated.
Paper: 2000-thomas.ps 85611 bytes
Decomposing Models of Parallel Queues
Reference: N Thomas, J T Bradley. Decomposing Models of Parallel Queues. In QNETS'00, Proceedings of the Fourth International Workshop on Queueing Networks with Finite Capacity, pp. 381-388, Ilkley, July, 2000.
Abstract: A class of queueing models is considered here which in general do not give rise to a product from solution but can nevertheless be decomposed into their components, subject to a property referred to as quasi-separability. Such a decomposition gives rise to expressions for marginal probabilities which may be used to derive potentially interesting system performance measures, such as the average number of jobs in the system. It is very important that some degree of confidence in such measures can also be given, however, we show here that it is not generally possible to calculate the variance exactly from the marginal probabilities. In this paper a simple approximation for the variance of the state a system of quasi-separable components is presented and evaluated.
Paper: 2000-thomas-0.ps 111743 bytes
Reliable Performance Modelling with Approximate Synchronisations
Reference: J T Bradley, N J Davies. Reliable Performance Modelling with Approximate Synchronisations. In PAPM'99, Proceedings of the 7th International Workshop on Process Algebra and Performance Modelling, Jane Hillston, Manuel Silva (Eds.), pp. 99-118, Prensas Universitarias de Zaragoza, Zaragoza, September, 1999.
Abstract: Markovian Process Algebras approximate their model of synchronisation events in order to preserve their Markovian nature. This paper investigates synchronisation models in a stochastic context and focuses on how the Markovian approximation of synchronisation affects the accuracy of the performance model. TIPP and PEPA are used as specific cases throughout,and their different methods of synchronisation are compared for effectiveness in performance modelling. The paper ends with a generally distributed example of real-world synchronisation, which we are able to solve analytically and then approximately with four Markovian Process Algebra models. From the results of this analysis, we show how such approximation affects the accuracy of the performance model of TIPP and PEPA.
Paper: 1999-bradley-3.ps.gz 277948 bytes
Book Chapter
Response time Densities and Quantiles in Large Markov and Semi-Markov Models
Reference: J T Bradley, N J Dingle, U Harder, P G Harrison, W J Knottenbelt. Response time Densities and Quantiles in Large Markov and Semi-Markov Models. In Performance Evaluation of Parallel, Distributed and Emergent Systems, Nova Science, 2006.
Abstract: Response time quantiles reflect user-perceived quality of service more accurately than mean or average response time measures. Consequently,on-line transaction processing benchmarks, telecommunications Service Level Agreements and emergency services legislation all feature stringent 90th percentile response time targets. This chapter describes a range of techniques for extracting response time densities and quantiles from large-scale Markov and semi-Markov models of real-life systems. We describe a method for the computation of response time densities or cumulative distribution functions which centres on the calculation and subsequent numerical inversion of their Laplace transforms. This can be applied to both Markov and semi-Markov models. We also review the use of uniformization to calculate such measures more efficiently in purely Markovian models. We demonstrate these techniques by using them to generate response time quantiles in a semi-Markov model of a high-availability web-server. We show how these techniques can be used to analyse models with state spaces of O(10^7) states and above.
Paper: 2006-bradley-2.pdf 467848 bytes
Edited Journal Issues
Modelling Techniques and Tools for Computer Performance Evaluation
Reference: Modelling Techniques and Tools for Computer Performance Evaluation. A J Field, P G Harrison, J T Bradley, U Harder (Eds.). Performance Evaluation, 54(2), pp. 77-206, Elsevier, October, 2003.
Abstract: Editors' Preface: The argument for performance engineering methods to be employed in computer-communication systems has always been that such systems cannot be designed or modified efficiently without recourse to some form of predictive model, just as in other fields of engineering. This argument has never been more valid than it is with today's highly complex combination of communication and computer technologies. These have created the Internet, the Grid and diverse types of parallel and distributed computer systems. To be practical, performance engineering relies on tools to render its use accessible to the non-performance specialist, and in turn these depend on sound techniques that include analytical methods, stochastic models and simulation. Tools and techniques also need to be parameterised and validated against real world observations, requiring sophisticated measurement techniques in this picosecond cyber-world. The series of International Conferences on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS) has provided a forum for this community of performance engineers with all their diverse interests. TOOLS 2002 was held in London in April 2002 and was a successful and stimulating forum for modellers and practitioners alike. This volume represents the very best of the 57 submissions that were originally submitted to TOOLS in November 2001. Of these, 10 were selected to be full papers, 10 to be shorter submissions and there were four practical tool papers. The authors of full papers and invited speakers were given the option of submitting extended versions for this special issue. These were further refereed and, after lengthy consideration, the final five were selected:
  1. PEPA nets: A structured performance modelling formalism, by Stephen Gilmore, Jane Hillston, Leila Kloul and Marina Ribaudo,combines stochastic process algebras with Petri nets to give a high level abstraction for modelling mobile agents.
  2. The Mobius State-level Abstract Functional Interface, by Salem Derisavi, Peter Kemper, William Sanders and Tod Courtney,presents a state-level functional interface for Markov models. It incorporates several Markovian modelling formalisms and connection methods with formal solution techniques.
  3. A Simulation-Based Methodology and Tool for Automating the Modelling and Analysis of Voice-over-IP Perceptual Quality, by Adrian Conway and Yali Zhu,describes a simulation testbed for evaluating the end-to-end quality of service of voice-over-IP services.
  4. Modelling IP Traffic using the Batch Markovian Arrival Process, by Alexander Klemm, Christoph Lindemann and Marco Lohmann,models IP traffic with BMAPs using an algorithm for their numerical parameter estimation.
  5. The impact of the service discipline on delay asymptotics, by S.C. Borst, O.J. Boxma, R. Nunez-Queija and A.P. Zwart,surveys recent work and gives a new generalisation on tails of waiting time distributions in M/G/1 queues under various queueing disciplines.
Finally, the editors would like to thank the TOOLS 2002 Programme Committee and the many referees who helped make this conference and special issue such a success.
Tony Field, Peter Harrison, Jeremy Bradley and Uli Harder,Imperial College, London, April 2003
Link: Elsevier Science Direct: Performance Evaluation
Edited Proceedings
Proceedings of Practical Applications of Stochastic Modelling
Reference: Proceedings of Practical Applications of Stochastic Modelling. J T Bradley, W J Knottenbelt (Eds.). The Royal Society, London, September, 2004.
Abstract: Recent years have seen not only significant theoretical advances in stochastic modelling and associated formalisms but also the increasing availability of high-powered computing facilities in academia and industry alike. The workshop on Practical Applications of Stochastic Modelling (PASM) was created out of a desire to harness these developments by encouraging the application of stochastic modelling formalisms to large-scale real-world systems.

We are, therefore, pleased to showcase in the very first workshop proceedings some excellent examples of how formalisms such as stochastic Petri nets, stochastic process algebras, queueing networks and SANs can be applied to diverse topical systems of practical interest such as peer-to-peer (P2P) file sharing networks, security protocols,electronic voting systems, parallel programming environments and RAID arrays.

It takes a great deal of effort and imagination to tackle the problems inherent in complex systems. We would like to thank everyone who submitted a paper~-- accepted or not~-- for taking on this challenge and for helping to contribute to a vibrant workshop.

We would also like to thank our invited speaker, Joost-Pieter Katoen, not to mention the programme committee who put in a stalwart effort to ensure a high quality refereeing process (with every submission receiving at least four reviews):

Paper: 2004-bradley-6.ps.gz 1008657 bytes
Proceedings of Computer Performance Evaluation: Modelling Techniques and Tools
Reference: Proceedings of Computer Performance Evaluation: Modelling Techniques and Tools. A J Field, P G Harrison, J T Bradley, U Harder (Eds.). Lecture Notes in Computer Science, vol. 2324, Springer-Verlag, Imperial College, London, April, 2002.
Link: LNCS 2324 Contents and Abstracts
Proceedings of the 16th Annual UK Performance Engineering Workshop
Reference: Proceedings of the 16th Annual UK Performance Engineering Workshop. N Thomas, J T Bradley (Eds.). Department of Computer Science, University of Durham, July, 2000.
Link: UKPEW'00 Online Proceedings
Proceedings of the 15th Annual UK Performance Engineering Workshop
Reference: Proceedings of the 15th Annual UK Performance Engineering Workshop. J T Bradley, N J Davies (Eds.). Tech. Report, CSTR-99-007, ISBN 0 9524027 8 5, Department of Computer Science, University of Bristol, Research Press, July, 1999.
Link: UKPEW'99 Online Proceedings
Tutorials
Reliability Modelling in Software with Random Processes
Reference: J T Bradley, N Thomas. Reliability Modelling in Software with Random Processes. In WOSP'00, Tutorials of the Second International Workshop on Software and Performance, R J Pooley (Ed.), ACM, Ottawa, September, 2000.
Abstract: [This tutorial was presented at WOSP 2000 in Ottawa - it consists of the annotated slide presentation] Modelling reliability in software is complicated by having to understand operating environment effects like virtual memory, garbage collection, dynamic linking, and so on. Often apparently constant-time events have probabilistic or random-time features as a result. We use stochastic process algebras (SPA) to capture these random effects and then show how reliability figures can be obtained from SPA models. From an SPA point of view, we also address the modelling of deterministic events, if-then-else-like branches and other software features in stochastic process algebras.
Paper: not available
Slides: 2000-bradley-1.ps 586593 bytes
Seminars
Why I'm always late!: using stochastic process algebras to model the Circadian clock
Reference: J T Bradley. Why I'm always late!: using stochastic process algebras to model the Circadian clock. In Verification and Simulation Worshop, Dagstuhl seminar series, Dagstuhl Schloss, 20 April, 2006.
Abstract: Many biological systems make use of a Circadian clock to keep track of the passage of time. The Circadian clock has evolved to create periodic concentrations of chemicals, in such a way that cells can regulate their behaviour according to the time of day or season of the year. With recent innovations in the quantitative analysis of stochastic process algebras to generate systems of ODEs or simulation models with huge unerlying state spaces, we will use the model of the Circadian clock to compare the biological modelling process in two such languages: PEPA and stochastic pi-calculus.
Paper: not available
Slides: 2006-bradley-4.slides.pdf 662132 bytes
The Future is Collaborative Performance Engineering!
Reference: J T Bradley. The Future is Collaborative Performance Engineering!. In UKPEW 2005, Invited talk, University of Newcastle, 1 June, 2005.
Abstract: Performance engineering is a hard task involving not only a large portion of concurrency theory, but also incorporating stochastic,deterministic and probabilistic concepts of time and choice at the modelling end. More widely performance engineering incorporates the gathering of instrumentation of real systems, the simulation of models of such systems and the real challenge is to have the modelling and simulation results match the performance experiments on the target system. We are working on a performance engineering environment called Perform-db which has at its core the notion that performance engineers need to collaborate in order to maximise the reuse of performance models, analysis, simulations, experiments and structural results. We believe that only in making use of formal modelling results that others have derived or in spotting patterns in experimental data that was produced from other related systems can the overall goal of a performance engineering lifecycle be achieved.
Paper: not available
Slides: 2005-bradley-3.slides.pdf 693205 bytes
Internet Worm Attacks and Stochastic Agent Models
Reference: J T Bradley. Internet Worm Attacks and Stochastic Agent Models. In From Many-Particle Physics to Multi-Agent Systems, Max Planck Institute for the Physics of Complex Systems, Dresden, 2 September, 2004.
Abstract: Recent malicious Internet worms such as Code Red (July 2001), Nimbda (September 2001) and most recently MS Blaster (August 2003) have been very successful in shutting down large sections of the Internet. Nicol et al have shown that most of a worm's worst effects are experienced by the Internet routers that link the major backbone networks together, which are completely overwhelmed by the explosion in particular types of Internet traffic. Nicol et al have taken the approach of modelling such a worm attack using simple epidemiological models: i.e. looking at the current number of computers that are infected, the number of computers susceptible to infection, and those that are removed from the system due to worm infection. These epidemiological models, once parameterised, are very good at producing average predictions of infection growth but quite poor when it comes to describing early-onset behaviour (especially possible early-extinction events). This project seeks to transfer and automate a technique, originally used to model ant and bee colony behaviour by Sumpter, to generate and verify macroscopic models of Internet worm infection. By building a stochastic agent model of the worm, we will be able either to justify and explain the use of global epidemiological models, or alternatively to suggest modifications to the model which would better describe the worm's infection behaviour. We also hope to shed light on crucial early-onset behaviour which would aid enormously in being able to spot the early stages of worm infection, even if an infection attempt has failed (i.e. become extinct).
Paper: not available
Slides: 2004-bradley-7.pdf 660413 bytes
Measuring Uncertainty with Stochastic Probes
Reference: J T Bradley. Measuring Uncertainty with Stochastic Probes. In LFCS Seminar Series, School of Informatics, University of Edinburgh, 28 October, 2003.
Abstract: Having constructed a process algebra model of a communicating system the next challenge is to ask useful questions of it. Usually one might use a logic to interrogate the model but unless the query is automatically generated this requires the user to learn another formalism. Our interest is in stochastic process algebra models and in particular PEPA models. Here the questions that can be asked extend beyond the functional to ones involving time and probability as well. In some recent work, we've looked at using regular expressions to specify so-called stochastic probes, which take the form of PEPA components. These are then used to set up a variety of stochastic queries on a PEPA model, such as: will my system recover from a failure mode within 1.7 seconds with probability 0.9995 or better? In the presentation, I'll look at the specification and construction of the stochastic probes, along with model/query analysis using the Imperial PEPA Compiler and the DNAmaca Markovian analyser.
Paper: not available
Slides: 2003-bradley-7.ps.gz 4558880 bytes
National Conferences
Semi-Markov PEPA: Compositional Modelling and Analysis with Generally Distributed Actions
Reference: J T Bradley. Semi-Markov PEPA: Compositional Modelling and Analysis with Generally Distributed Actions. In UKPEW'04, Proceedings of 20th Annual UK Performance Engineering Workshop, Irfan Awan (Ed.), pp. 266-275, University of Bradford, July, 2004.
Paper: 2004-bradley-2.ps.gz 62737 bytes
Slides: 2004-bradley-2.slides.pdf 455752 bytes
Semi-blind Scheduling in a Finite Capacity System
Reference: N A Thomas, J T Bradley, W J Knottenbelt. Semi-blind Scheduling in a Finite Capacity System. In UKPEW'04, Proceedings of 20th Annual UK Performance Engineering Workshop, Irfan Awan (Ed.), pp. 38-47, University of Bradford, July, 2004.
Abstract: In this paper a class of queueing model is studied where servers break down but the information regarding breakdowns is not immediately available. As such, jobs continue to arrive into a queue for some period after service has ceased. These queues have finite capacity, therefore there is also the possibility that queues become full causing job-loss. The effect of the duration of any delay on information propagation on the system response time and job loss is investigated and evaluated numerically.
Paper: 2004-thomas-0.ps.gz 235698 bytes
Extracting Passage Times from PEPA models with the HYDRA Tool: a Case Study
Reference: J T Bradley, N J Dingle, S T Gilmore, W J Knottenbelt. Extracting Passage Times from PEPA models with the HYDRA Tool: a Case Study. In UKPEW'03, Proceedings of 19th Annual UK Performance Engineering Workshop, S A Jarvis (Ed.), pp. 79-90, University of Warwick, July, 2003.
Abstract: Passage time densities and quantiles are important performance metrics which are increasingly used in specifying service level agreements (SLAs) and benchmarks. PEPA is a popular stochastic process algebra and a powerful formalism for describing performance models of communication and computer systems. We present a case study passage time analysis of an 82,944 state PEPA model using the HYDRA tool. HYDRA specialises in passage time analysis of large Markov systems based on stochastic Petri nets. By using the new Imperial PEPA compiler (ipc), we can construct a HYDRA model from a PEPA model and obtain passage time densities based on the original PEPA description.
Paper: 2003-bradley-1.ps.gz 73642 bytes
Slides: 2003-bradley-1.slides.ps.gz 3334556 bytes
Semi-Markov PEPA: a contradiction in terms?
Reference: J T Bradley. Semi-Markov PEPA: a contradiction in terms?. In PASTA'03, Proceedings of 2nd Int. Workshop on Process Algebras and Stochastically Timed Activities, S T Gilmore (Ed.), pp. 1-6, LFCS, Edinburgh, June, 2003.
Abstract: In this report, we consider a semi-Markov version of PEPA. In particular, we discuss the seeming conflict between semi-Markov modelling,which appears to be sequential and lacking in concurrency, and process algebraic modelling, which whole raison d'etre is to model concurrency.
Paper: 2003-bradley-5.ps.gz 44110 bytes
Slides: 2003-bradley-5.slides.pdf 3612727 bytes
Ants and Agents: Global Complexity from Local Simplicity
Reference: J T Bradley. Ants and Agents: Global Complexity from Local Simplicity. In PASTA'02, Proceedings of Int. Workshop on Process Algebras and Stochastically Timed Activities, S T Gilmore (Ed.), Edinburgh, June, 2002.
Abstract: This presentation discusses some of the process algebra oriented techniques that Dave Sumpter derived in his thesis and subsequent publications. His focus was to use process models to describe local agent behaviour of ants, bees and other colonial insects in order to derive explanations for observed and simulated global ant colony behaviour. The work uses Mean Field Analysis techniques on the component descriptions themselves to derive approximate transient behaviour for the global system. The strength of this approach in its component-oriented nature and the fact that it can handle enormous global state spaces. This work is particularly prescient today with the current focus on e-science and cross-disciplinary research. Further research is clearly needed for both the automation of MFA equation generation and in generalising the types of process model that can be analysed.
Paper: not available
Slides: 2002-bradley-2.slides.ps.gz 843268 bytes
An Approximate Solution of PEPA Models Using Component Substitution
Reference: N Thomas, J T Bradley, D J Thornley. An Approximate Solution of PEPA Models Using Component Substitution. In UKPEW'02, Proceedings of 18th Annual UK Performance Engineering Workshop, M Ould-Khaoua (Ed.), pp. 223-234, Glasgow, July, 2002.
Abstract: Performance models specified using compositional algebra suffer the well-known state space explosion problem, where a relatively small definition leads to a Markov chain with a large state space that is problematic to solve. As a result it is widely recognised that the development of techniques to solve performance models efficiently is of particular practical importance. Recently the notion of behavioural independence was introduced to exploit the structure of Markovian process algebra models in order to solve models in a compositional manner. In this paper the opposite property, namely control, is used to solve models by substituting components in the model with simpler versions.
Paper: 2002-thomas-0.ps.gz 107699 bytes
Transient and Passage-time Distributions in Semi-Markov Processes
Reference: J T Bradley, W J Knottenbelt, P G Harrison, C J Vowden. Transient and Passage-time Distributions in Semi-Markov Processes. In UKPEW'02, Proceedings of 18th Annual UK Performance Engineering Workshop, M Ould-Khaoua (Ed.), pp. 153-162, Glasgow, July, 2002.
Abstract: We discuss passage-time and transient analysis for a particular class of non-Markovian model---the semi-Markov process. We present definitions of first passage-time distributions between clusters of states in a semi-Markov process. The paper then investigates an algorithm for approximating the passage-time distribution which is potentially O(n^2). Finally we touch on how this might be applied to reducing the complexity of transient analysis of SMPs.
Paper: 2002-bradley-3.ps.gz 87932 bytes
Slides: 2002-bradley-3.slides.ps.gz 297751 bytes
Terminating Processes in PEPA
Reference: N Thomas, J T Bradley. Terminating Processes in PEPA. In UKPEW'01, Proceedings of 17th Annual UK Performance Engineering Workshop, K Djemame, M Kara (Eds.), pp. 143-154, Leeds, July, 2001.
Abstract: In this paper we introduce the concept of a null component into the Markovian process algebra PEPA. The null component allows us explicitly to define models which have components that cease to execute. By implication this allows us to formally define a notion of a successfully terminating model and hence enhanced concepts of deadlock and livelock in transient PEPA models.
Paper: 2001-bradley-1.ps.gz 70720 bytes
Constructing a Partial Order for Performance Measures
Reference: J T Bradley, N Thomas. Constructing a Partial Order for Performance Measures. In UKPEW'00, Proceedings of 16th Annual UK Performance Engineering Workshop, N Thomas, J Bradley (Eds.), pp. 177-186, Durham, July, 2000.
Paper: 2000-bradley-0.ps 155328 bytes
Measuring Improved Reliability in Stochastic Systems
Reference: J T Bradley, N J Davies. Measuring Improved Reliability in Stochastic Systems. In UKPEW'99, Proceedings of the 15th Annual UK Performance Engineering Workshop, J T Bradley, N J Davies (Eds.), Tech. Report, CSTR-99-007, pp. 121-130, Bristol, July, 1999.
Abstract: In this paper, we examine reliability of stochastic systems with specific application to Stochastic Process Algebras. We look at variance as a possible reliability metric and show how it can be reduced across different Stochastic Process Algebra combinators, thus giving more deterministic and reliable systems. We apply these techniques to analyse and improve a searching algorithm.
Paper: 1999-bradley-2.ps.gz 88570 bytes
Theses
Towards Reliable Modelling with Stochastic Process Algebras
Reference: J T Bradley. Towards Reliable Modelling with Stochastic Process Algebras. PhD Thesis, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, October, 1999.
Abstract: In this thesis, we investigate reliable modelling within a stochastic process algebra framework. Primarily, we consider issues of variance in stochastic process algebras as a measure of model reliability. This is in contrast to previous research in the field which has tended to centre around mean behaviour and steady-state solutions. We present a method of stochastic aggregation for analysing generally-distributed processes. This allows us more descriptive power in representing stochastic systems and thus gives us the ability to create more accurate models. We improve upon two well-developed Markovian process algebras and show how their simpler paradigm can be brought to bear on more realistic synchronisation models. Now, reliable performance figures can be obtained for systems, where previously only approximations of unknown accuracy were possible. Finally, we describe reliability definitions and variance metrics in stochastic models and demonstrate how systems can be made more reliable through careful combination under stochastic process algebra operators.
Paper: 1999-bradley-4.ps.gz 1708633 bytes
The SSL Reference Implementation Project
Reference: J T Bradley. The SSL Reference Implementation Project. MSc Thesis, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, October, 1995.
Abstract: Information is now the most valuable resource in the world. Whether it is a personal letter or an industrial secret, all information has a worth to someone. This thesis considers issues of security and privacy for such information. It discusses the reasons for wishing to protect data and the methods available for doing so. Specifically, the project concerns cryptography and secure communications, in particular the Secure Sockets Layer (SSL) protocol. It contains a communications and security analysis of SSL as well as details of the construction of a secure reference implementation of the protocol.
Paper: 1995-bradley-0.ps.gz 365866 bytes
Technical Reports
Convergence and Correctness of an Iterative Scheme for Calculating Passage Times in Semi-Markov Processes
Reference: H J Wilson. Convergence and Correctness of an Iterative Scheme for Calculating Passage Times in Semi-Markov Processes. Tech. Rep., 2004/1, Department of Applied Maths, University of Leeds, Woodhouse Lane, Leeds, LS2 9JT, UK, February, 2004.
Abstract: An iterative scheme was introduced [Bradley, Dingle, Knottenbelt and Wilson,LAA 2003] using matrix-vector multiplication to calculate first passage times in semi-Markov processes. We show that the spectral radius of the matrix in question is at most 1, and prove that the method converges even when eigenvalues exist with modulus exactly 1. We also demonstrate correctness of the converged result.
Paper: 2004-wilson-0.ps.gz 54284 bytes
Report on Extracting Transient Distributions from Semi-Markov Processes
Reference: J T Bradley, C J Vowden. Report on Extracting Transient Distributions from Semi-Markov Processes. CS Tech. Rep., 2001(8), Department of Computer Science, University of Durham, South Road, Durham, DH1 3LE, UK, July, 2001.
Abstract: We present an analytic derivation of transient distributions in semi-Markov processes. We show how a closed form solution of a transient probability can be obtained in terms of solely the Laplace transforms of the outgoing distribution and that of the response-time or return distribution. Using this information a transient distribution can be built up progressively as required for each state. We briefly introduce two traditional techniques and discuss a possible problem with the Cox and Miller method.
Paper: 2001-bradley-4.ps.gz 201436 bytes
Constructing a Residual Density Operator
Reference: J T Bradley. Constructing a Residual Density Operator. CS Tech. Rep., 2001(9), Department of Computer Science, University of Durham, South Road, Durham, DH1 3LE, UK, July, 2001.
Abstract: We derive an operator for expressing the residual density function--that left over when one random variable is pre-empted by another. We show how it can be used to describe the state space of queueing systems and use it to highlight a duality between M/G/1/K queues and a blocked arrival flavour of G/M/1/K queues. Unfortunately the definition of this operator poses some questions with regard to variance in particular situations and this is discussed.
Paper: 2001-bradley-5.ps.gz 329821 bytes
Report on the Numerical Inversion of Laplace Transforms of Probabilistic Functions: A Haskell Implementation
Reference: J T Bradley. Report on the Numerical Inversion of Laplace Transforms of Probabilistic Functions: A Haskell Implementation. CS Tech. Rep., 2001(6-7), Department of Computer Science, University of Durham, South Road, Durham, DH1 3LE, UK, July, 2001.
Abstract: We investigate different numerical techniques (by Abate, Whitt and Choudhury) for inverting Laplace transforms with probabilistic applications in mind. We suggest different parameter sets for some of the algorithms which improve the accuracy of Euler and Post-Widder methods. A Haskell implementation of the algorithms is included.
Paper: 2001-bradley-2.ps.gz 177173 bytes
Slides: 2001-bradley-2.slides.ps.gz 154959 bytes
A Note on the Proof of Reduction of Biconnected Digraphs to Normal Forms
Reference: H J Wilson, J T Bradley. A Note on the Proof of Reduction of Biconnected Digraphs to Normal Forms. Tech. Report, CSTR-99-009, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, September, 1999.
Abstract: We present a proof method for reducing biconnected digraphs to a normal form and demonstrate its convergence for a general biconnected digraph.
Paper: 1999-wilson-0.ps.gz 236041 bytes
An Aggregation Technique for Analysing Some Generally Distributed Stochastic Processes
Reference: J T Bradley, N J Davies. An Aggregation Technique for Analysing Some Generally Distributed Stochastic Processes. Tech. Report, CSTR-99-003, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, March, 1999.
Abstract: A stochastic aggregation technique is developed and used to reduce generally distributed stochastic transition systems to a soluble example. By aggregating carefully, we can derive the entire stationary distribution for the original stochastic transition system. This paper examines the possibility of constructing a solution technique for generally distributed process algebras. Further, we demonstrate that by creating a stochastic transition system, we can solve G/G/1/2 queues and, more generally, Markovian Process Algebras without the use of Markov Chains.
Paper: 1999-bradley-0.ps.gz 616470 bytes
Reliable Performance Modelling with Approximate Synchronisations
Reference: J T Bradley, N J Davies. Reliable Performance Modelling with Approximate Synchronisations. Tech. Report, CSTR-99-002, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, February, 1999.
Abstract: Markovian Process Algebras approximate their model of synchronisation events in order to preserve their Markovian nature. This paper investigates synchronisation models in a stochastic context and focuses on how the Markovian approximation of synchronisation affects the accuracy of the performance model. TIPP and PEPA are used as specific cases throughout, and their different methods of synchronisation are compared for effectiveness in performance modelling. The paper ends with a generally distributed example of real-world synchronisation, which we are able to solve analytically and then approximately with four Markovian Process Algebra models. From the results of this analysis, we are able to suggest other Markovian synchronisation models which complement and improve on those presented by TIPP and PEPA.
Paper: 1999-bradley.ps.gz 292417 bytes
Compositional BDD Construction: A Lazy Algorithm
Reference: J T Bradley, N J Davies. Compositional BDD Construction: A Lazy Algorithm. Tech. Report, CSTR-98-005, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, April, 1998.
Abstract: The efficient Binary Decision Diagram algorithm presented in Brace, Rudell and Bryant 1990 is modified to operate in a lazy or demand-driven fashion. We show how this new approach benefits the area of symbolic model checking by reducing the amount of state-space that needs to be evaluated. The need for a lazy or "delayed" BDD-based manipulation system, specifically to aid the reasoning about symbolic systems, was identified in Bryant 1992 as a method of tackling the state-space explosion problem. Often the model checking of systems only uses a very small part of the BDD (Bryant 1992). This is especially true for the generation of model checking counter-examples (Clarke et al 1994). However the strict nature of traditional BDD algorithms means that the whole BDD-representation of a system has to be evaluated. Since this new technique only evaluates the nodes of the BDD that are required, it can potentially manipulate significantly larger and more complex systems than could be represented before. We give space and time complexity comparisons between the traditional and lazy algorithms and show how it affects the practical evaluation of state-space especially for model checking purposes.
Paper: 1998-bradley-0.ps.gz 113914 bytes
Analysis of the SSL Protocol
Reference: J T Bradley, N J Davies. Analysis of the SSL Protocol. Tech. Report, CSTR-95-021, Department of Computer Science, University of Bristol, Bristol BS8 1UB, UK, June, 1995.
Abstract: SSL, as a proposed secure communications protocol, is set to become an international standard. As such it is importan t to have a full discussion of the technical and practical issues behind the protocol before the onset of commercial and industry acceptance. The protocol goes in front of an IETF BOF in July of this year and it is hoped that this document will be one of many to provide a small discussion point for that meeting. This report analyses the communications structure of the SSL Handshake Protocol and suggests alterations based on such analysis. Other recommendations cover issues of general security, as well as some of the administrative points associated with certification.
Paper: 1995-bradley.ps.gz 223832 bytes

Last updated by awk: Thu 29 Jun 09:57 BST 2006