Marta Kwiatkowska

Xu Wang, Marta Kwiatkowska

Replace (2008)

this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be found at the ENTCS Macro Home Page. Compositional state space reduction using untangled actions

Part I Probabilistic Model Checking Overview (2008)

Fundamenta Informaticae XXX (200?) 0–27 0 IOS Press On process-algebraic verification of asynchronous circuits ∗ (2008)

− Discrete-time Markov chains, Markov decision processes, temporal logic (PCTL), model checking algorithms, probabilistic timed automata

ABSTRACT (2008)

L. F. Perrone, F. P. Wiel, J. Liu, B. G. Lawson, D. M. Nicol, R. M. Fujimoto, ...

Systems Biology is aimed at analyzing the behavior and interrelationships of biological systems and is characterized by combining experimentation, theory, and computation. Dedicated to exploring...

Xu Wang, Marta Kwiatkowska

Abstract. Asynchronous circuits have received much attention recently due to their potential for energy savings. Process algebras have been extensively used in the modelling, analysis and synthesis...

Formal Aspects of Computing (2005) Formal Aspects of Computing (2008)

Gethin Norman, David Parker, Marta Kwiatkowska, Eep Shukla, Rajesh Gupta

Using probabilistic model checking for dynamic power management

Automated Veri (2008)

Cation Of Randomized, Marta Kwiatkowska, Gethin Norman, Roberto Segala

We consider the randomized consensus protocol of Aspnes and Herlihy for achieving agreement among N asynchronous processes that communicate via read/write shared registers. The algorithm guarantees...

Possible and Guaranteed Concurrency in CSP (2007)

Marta Kwiatkowska, Iain Phillips

As part of an effort to give a "truly concurrent" semantics to process algebra, we propose a framework of refinements of the failures model for CSP with concurrency, conflict and causality...

On Topological Hierarchies of Temporal Properties (2007)

Solving Infinite Stochastic Process Algebra Models through Matrix-Geometric Methods (2007)

. The classification of properties of concurrent programs into safety and liveness was first proposed by Lamport [22]. Since then several characterizations of hierarchies of properties have been...

Amani El-Rayes, Marta Kwiatkowska, Gethin Norman

. We introduce a Stochastic Process Algebra called PEPA 1 ph , based on Hillston's PEPA. PEPA 1 ph is suitable for describing and analysing the performance of certain kinds of queues, such as...

Duality and the Completeness of the Modal µ-Calculus (2007)

Simon Ambler, Leicester Le Rh, Marta Kwiatkowska, Nicholas Measor

We consider the modal ¯-calculus due to Kozen, which is a finitary modal logic with least and greatest fixed points of monotone operators. We extend the existing duality between the category of...

On Topological Hierarchies of Temporal Properties (2007)

Possible and Guaranteed Concurrency in CSP (2007)

. The classification of properties of concurrent programs into safety and liveness was first proposed by Lamport [20]. Since then several characterizations of hierarchies of properties have been...

Marta Kwiatkowska, Iain Phillips

As part of an effort to give a "truly concurrent" semantics to process algebra, we propose a framework of refinements of the failures model for CSP with concurrency, conflict and causality...

Concurrency, Fairness and Logical Complexity (2007)

Marta Kwiatkowska, Also Visiting

We consider a connection between fairness and \Pi 0 3 sets of functions made recently by Darondeau, Nolte, Priese and Yoccoz, and extend their work to cater for effective asynchronous transition...

and ANT (2007)

Abstract. We introduce a Stochastic Process Algebra called PEPA (2007)

Abstract { In this paper we extend CSL (Continuous Stochastic Logic) with an expected time and an expected reward operator, both of which are parameterized by a random terminal time. With the help of...

Amani El-rayes, Marta Kwiatkowska, Gethin Norman

ph,

Automated Verication of a Randomized Byzantine Agreement Protocol (2007)

Joost-pieter Katoen, Marta Kwiatkowska, Gethin Norman, David Parker

We consider the randomized protocol of Cachin, Kursawe and Shoup [CKS00] for solving the asynchronous Byzantine agreement problem. The protocol is of practical interest since it forms the core of a...

b (2007)

Abstract. This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties...

b (2007)

Holger Hermanns, Marta Kwiatkowska, Gethin Norman, David Parker, Markus Siegle

On the use of MTBDDs for performability analysis and verification of stochastic systems

Automated Verication of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM (2007)

Marta Kwiatkowska, Gethin Norman, Roberto Segala

Abstract. We consider the randomized consensus protocol of Aspnes and Herlihy for achieving agreement among N asynchronous processes that communicate via read/write shared registers. The algorithm...

Automated Verication of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM (2007)

Marta Kwiatkowska, Gethin Norman, Roberto Segala

We consider the randomized consensus protocol due to Aspnes and Herlihy [1] for achieving agreement among N asynchronous processes that communicate via read/write shared registers. The algorithm...

Under consideration for publication in Formal Aspects of Computing Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol (2007)

An Ecient Symbolic Out-of-Core Solution Method for Markov Models (2007)

a;b

Rashid Mehmood, David Parker, Marta Kwiatkowska

Abstract. In recent years, disk-based approaches to the analysis of Markov models have proved to be an eective method of combating the state space explosion problem. Coupled with parallel and...

1 (2007)

Marta Kwiatkowska, David Parker, Jeremy Sproston

Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a specication formalism suitable for describing both nondeterministic and probabilistic...

1 (2007)

Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

Abstract. Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare...

and (2007)

Symbolic model checking for purely probabilistic processes using MTBDDs [12] was introduced in [4] and further developed in [20, 3]. In this paper we consider models for concurrent probabilistic...

1 (2007)

Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang

Abstract. Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We...

b (2007)

Joost-pieter Katoen, Marta Kwiatkowska, Gethin Norman, David Parker

Abstract. This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties...

Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach (2007)

Symbolic Computation of Minimal Probabilistic (2007)

The date of receipt and acceptance will be inserted by the editor Abstract. In this paper we present ecient symbolic techniques for probabilistic model checking. These have been implemented in PRISM,...

Reachability Marta Kwiatkowska, Marta Kwiatkowska, Gethin Norman, Jeremy Sproston

systems featuring both nondeterministic and probabilistic choice. In an earlier paper we de ned symbolic probabilistic systems, an extension of the framework of symbolic transition systems due to...

Contents (2007)

Users' Guide Dave, Dave Parker, Gethin Norman, Marta Kwiatkowska

Contents 1 Overview 1 2 Background Material 2 2.1 Probabilistic models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Specification of properties . . . . . . . . . . . . . . ....

PCTL model checking of symbolic probabilistic (2007)

Systems Marta Kwiatkowska, Marta Kwiatkowska, Gethin Norman, Jeremy Sproston

Probabilistic model checking is a method for automatically verifying that a probabilistic system satis es a property with a given likelihood, with the probabilistic temporal logic Pctl being a common...

PRISM: A tool for automatic verification of probabilistic systems (2006)

Andrew Hinton, Marta Kwiatkowska, Gethin Norman, David Parker

Abstract. Probabilistic model checking is an automatic formal verification technique for analysing quantitative properties of systems which exhibit stochastic behaviour. PRISM is a probabilistic...

Game-based abstraction for markov decision processes (2006)

D.: Symmetry reduction for probabilistic model checking (2006)

In this paper we present a novel abstraction technique for Markov decision processes (MDPs), which are widely used for modelling systems that exhibit both probabilistic and nondeterministic...

Compositional state space reduction using untangled actions (2006)

Abstract. We present an approach for applying symmetry reduction techniques to probabilistic model checking, a formal verification method for the quantitative analysis of systems with stochastic...

Xu Wang, Marta Kwiatkowska

actions

Discussion on Robin Milner's First Computer Journal Lecture: Ubiquitous Computing: Shall We Understand It? (2006)

Sloman, Morris, Thomas, Martyn, Sparck-Jones, Karen, Crowcroft, Jon, Kwiatkowska, Marta, Garner, Paul, ...

Stochastic transition systems for continuous state spaces and non-determinism (2005)

Stefano Cattani, Roberto Segala, Marta Kwiatkowska, Gethin Norman

Abstract. We study the interaction between non-deterministic and probabilistic behaviour in systems with continuous state spaces, arbitrary probability distributions and uncountable branching. Models...

An MTBDD-based implementation of forward reachability for probabilistic timed automata (2005)

Fuzhi Wang, Marta Kwiatkowska

Abstract. Multi-Terminal Binary Decision Diagrams (MTBDDs) have been successfully applied in symbolic model checking of probabilistic systems. In this paper we propose an encoding method for...

A wavefront parallelisation of CTMC solution using MTBDDs (2005)

Yi Zhang, David Parker, Marta Kwiatkowska

In this paper, we present a parallel implementation for the steady-state analysis of continuous-time Markov chains (CTMCs). This analysis is performed via solution of a linear equation system, which...

Evaluating the reliability of NAND multiplexing with PRISM (2005)

Gethin Norman, David Parker, Marta Kwiatkowska, Eep Shukla

Abstract — Probabilistic model checking is a formal verification technique for analysing the reliability and performance of systems exhibiting stochastic behaviour. In this paper, we demonstrate...

Symbolic model checking for probabilistic timed automata (2004)

Symbolic model checking for probabilistic timed automata (2004)

We consider probabilistic timed automata of [13], an extension of the timed automata model of [2] with discrete probability distributions. In contrast to timed automata, which model real-time systems...

Numerical vs. statistical probabilistic model checking: An empirical study (2004)

Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We present...

A Formal Analysis of Bluetooth Device Discovery (2004)

Abstract. Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare...

Marie Duflot, Marta Kwiatkowska, Gethin Norman, David Parker

Abstract. This paper presents a formal analysis of the device discovery phase of the Bluetooth wireless communication protocol. The performance of this process is the result of a complex interaction...

PRISM 2.0: A tool for probabilistic model checking (2004)

Symbolic model checking for probabilistic timed automata (2004)

This paper gives a brief overview of version 2.0 of PRISM, a tool for the automatic formal verification of probabilistic systems, and some of the case studies to which it has already been applied. 1.

Symbolic model checking for probabilistic timed automata (2004)

Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We present...

Marta Kwiatkowska, Jeremy Sproston

, and Fuzhi Wang 1 1

Evaluating the reliability of defect-tolerant architectures for nanotechnology with probabilistic model checking (2004)

Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep K. Shukla

As we move from deep submicron technology to nanotechnology for device manufacture, the need for defect-tolerant architectures is gaining importance. This is because, at the nanoscale, devices will...

Numerical vs. statistical probabilistic model checking: An empirical study (2004)

Evaluating the reliability of defect-tolerant architectures for nanotechnology with probabilistic model checking (2004)

Abstract. Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We compare...

Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep K. Shukla

As we move from deep submicron technology to nanotechnology for device manufacture, the need for defect-tolerant architectures is gaining importance. This is because, at the nanoscale, devices will...

PRISM 2.0: A Tool for Probabilistic Model Checking (2004)

Controller Dependability Analysis by Probabilistic Model Checking (2004)

This paper gives a brief overview of version 2.0 of PRISM, a tool for the automatic formal verification of probabilistic systems, and some of the case studies to which it has already been applied.

Symbolic model checking for probabilistic timed automata (2004)

We demonstrate how probabilistic model checking, a formal veri cation method for the analysis of systems which exhibit stochastic behaviour, can be applied to the study of dependability properties of...

Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang

Abstract. Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We...

Controller Dependability Analysis By Probabilistic Model Checking (2004)

CSP + Clocks: a process algebra for timed automata (2003)

Abstract: This paper demonstrates how probabilistic model checking, a formal verification method for the analysis of systems which exhibit stochastic behaviour, can be applied to the study of...

Stefano Cattani, Marta Kwiatkowska

Abstract. We propose a real-time extension to the process algebra CSP. Inspired by timed automata, a very successful formalism for the specication and verication of real-time systems, we handle real...

Performance analysis of probabilistic timed automata using digital clocks (2003)

Marta Kwiatkowska, Gethin Norman, David Parker, Jeremy Sproston

Using probabilistic model checking for dynamic power management (2003)

Gethin Norman, David Parker, Marta Kwiatkowska, Eep Shukla, Rajesh Gupta

Performance analysis of probabilistic timed automata using digital clocks (2003)

Marta Kwiatkowska, Gethin Norman, David Parker, Jeremy Sproston

Abstract. Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a modelling formalism suitable for describing formally both nondeterministic...

Probabilistic model checking of deadline properties (2003)

An Efficient BDD-Based Implementation of Gauss-Seidel for CTMC Analysis (2003)

The increasing dependence of businesses on distributed architectures and computer networking places heavy demands on the speed and reliability of data exchange, leading to the emergence of...

Rashid Mehmood, David Parker, Marta Kwiatkowska

Symbolic approaches to the analysis of Markov models, i.e. those that use BDD-based data structures, have proved to be an effective method of combating the state space explosion problem. One such...

An Efficient Symbolic Out-of-Core Solution Method for Markov Models (2003)

Rashid Mehmood, David Parker, Marta Kwiatkowska

In recent years, disk-based approaches to the analysis of Markov models have proved to be an eective method of combating the state space explosion problem. Coupled with parallel and symbolic...

Performance Analysis of Probabilistic Timed (2003)

Automata Using Digital, Marta Kwiatkowska, Gethin Norman, David Parker, Jeremy Sproston

Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a speci cation formalism suitable for describing both nondeterministic and probabilistic...

Model Checking for Probability and Time: From Theory to Practice (2003)

Using Probabilistic Model Checking for Dynamic Power Management (2003)

Probability features increasingly often in software and hardware systems: it is used in distributed co-ordination and routing problems, to model fault-tolerance and performance, and to provide...

Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla, Rajesh Gupta

We present an approach to deriving stochastic Dynamic Power Management (DPM) strategies that enables us to design both discrete time and continuous time Markov chain based strategies, in a formal and...

Performance analysis of probabilistic timed automata using digital clocks (2003)

Marta Kwiatkowska, Gethin Norman, David Parker, Jeremy Sproston

Abstract. Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a specification formalism suitable for describing both nondeterministic and...

Using probabilistic model checking for dynamic power management (2003)

Gethin Norman, David Parker, Marta Kwiatkowska, Eep Shukla, Rajesh Gupta

Abstract. We present an approach to deriving stochastic Dynamic Power Management (DPM) strategies that enables us to design both discrete time and continuous time Markov chain based strategies, in a...

CSP + Clocks: a process algebra for timed automata (2003)

Stefano Cattani, Marta Kwiatkowska

Abstract. We propose a real-time extension to the process algebra CSP. Inspired by timed automata, a very successful formalism for the specification and verification of real-time systems, we handle...

A symbolic out-of-core solution method for Markov models (2002)

Marta Kwiatkowska, Rashid Mehmood, Gethin Norman, David Parker

Despite considerable eort, the state-space explosion problem remains an issue in the analysis of Markov models. Given structure, symbolic representations can result in very compact encoding of the...

Probabilistic symbolic model checking with PRISM: A hybrid approach (2002)

Verifying Randomized Byzantine Agreement (2002)

Abstract. In this paper we introduce PRISM, a probabilistic model checker, and describe the ecient symbolic techniques we have developed during its implementation. PRISM is a tool for analysing...

PRISM: Probabilistic symbolic model checker (2002)

Abstract. Distributed systems increasingly rely on fault-tolerant and secure authorization services. An essential primitive used to implement such services is the Byzantine agreement protocol for...

PRISM: Probabilistic symbolic model checker (2002)

Abstract. In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports two probabilistic models: continuous-time...

Model checking CSL until formulae with random time bounds (2002)

Abstract. In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports three probabilistic models: discrete-time...

Marta Kwiatkowska, Gethin Norman, António Pacheco

Abstract. Continuous Time Markov Chains (CTMCs) are widely used as the underlying stochastic process in performance and dependability analysis. Model checking of CTMCs against Continuous Stochastic...

Verifying Randomized Byzantine Agreement (2002)

Probabilistic model checking of the IEEE 802.11 wireless local area network protocol (2002)

Abstract. Distributed systems increasingly rely on fault-tolerant and secure authorization services. An essential primitive used to implement such services is the Byzantine agreement protocol for...

Probabilistic symbolic model checking with PRISM: A hybrid approach (2002)

PRISM: Probabilistic symbolic model checker (2002)

In this paper we introduce PRISM, a probabilistic model checker, and describe the ecient symbolic techniques we have developed during its implementation. PRISM is a tool for analysing probabilistic...

Model checking CSL until formulae with random time bounds (2002)

Abstract. In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems. PRISM supports three probabilistic models: discrete-time...

Out-of-Core Solution of Large Linear Systems of Equations Arising from Stochastic Modelling (2002)

Abstract. Continuous Time Markov Chains (CTMCs) are widely used as the underlying stochastic process in performance and dependability analysis. Model checking of CTMCs against Continuous Stochastic...

Marta Kwiatkowska, Rashid Mehmood

Many physical or computer systems can be modelled as Markov chains. A range of solution techniques exist to address the state-space explosion problem, encountered while analysing such Markov models.

Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol (2002)

PRISM: Probabilistic Symbolic Model Checker (2002)

The international standard IEEE 802.11 was developed recently in recognition of the increased demand for wireless local area networks. Its medium access control mechanism is described according to a...

On the use of MTBDDs for performability analysis and verification of stochastic systems (2002)

In this paper we describe PRISM, a tool being developed at the University of Birmingham for the analysis of probabilistic systems.

Holger Hermanns, Marta Kwiatkowska, Gethin Norman, David Parker, Markus Siegle

This paper describes how to employ Multi-Terminal Binary Decision Diagrams (MTBDDs) for the construction and analysis of a general class of models that exhibit stochastic, probabilistic and...

Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM (2002)

Conrado Daws, Marta Kwiatkowska, Gethin Norman

We report on the automatic veri cation of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time modelchecker Kronos and the...

Probabilistic model checking of the IEEE 802.11 wireless local area network protocol (2002)

Marta Kwiatkowska, Jeremy Sproston

Abstract. The international standard IEEE 802.11 was developed recently in recognition of the increased demand for wireless local area networks. Its medium access control mechanism is described...

Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM (2002)

Conrado Daws, Marta Kwiatkowska, Gethin Norman

We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time model-checker Kronos and the...

Probabilistic symbolic model checking with PRISM: A hybrid approach (2002)

A symbolic out-of-core solution method for Markov models (2002)

Abstract. In this paper we introduce PRISM, a probabilistic model checker, and describe the efficient symbolic techniques we have developed during its implementation. PRISM is a tool for analysing...

Marta Kwiatkowska, Rashid Mehmood, Gethin Norman, David Parker

Despite considerable effort, the state-space explosion problem remains an issue in the analysis of Markov models. Given structure, symbolic representations can result in very compact encoding of the...

Symbolic computation of maximal probabilistic reachability (2001)

Symbolic Computation of Maximal Probabilistic (2001)

Abstract. We study the maximal reachability probability problem for in nite-state systems featuring both nondeterministic and probabilistic choice. The problem involves the computation of the maximal...

Reachability Marta Kwiatkowska, Marta Kwiatkowska, Gethin Norman, Jeremy Sproston

We study the maximal reachability probability problem for in nite-state systems featuring both nondeterministic and probabilistic choice. The problem involves the computation of the maximal...

Faster and Symbolic CTMC Model Checking (2001)

Joost-pieter Katoen, Marta Kwiatkowska, Gethin Norman, David Parker

This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are...

Symbolic computation of maximal probabilistic reachability (2001)

Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM (2001)

Abstract. We study the maximal reachability probability problem for infinite-state systems featuring both nondeterministic and probabilistic choice. The problem involves the computation of the...

Marta Kwiatkowska, Gethin Norman, Roberto Segala

Abstract. We consider the randomized consensus protocol of Aspnes and Herlihy for achieving agreement among N asynchronous processes that communicate via read/write shared registers. The algorithm...

Verifying randomized distributed algorithms with prism (2000)

Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation (2000)

Abstract. In this paper we describe our experience with model checking randomized distributed algorithms using PRISM, a symbolic model checker for concurrent probabilistic systems currently being...

Marta Kwiatkowska, David Parker, Roberto Segala

Abstract. Symbolic model checking for purely probabilistic processes using MTBDDs [12] was introduced in [4] and further developed in [20, 3]. In this paper we consider models for concurrent...

Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation (2000)

Marta Kwiatkowska, David Parker, Roberto Segala

Abstract. Symbolic model checking for purely probabilistic processes using MTBDDs [12] was introduced in [4] and further developed in [21, 3]. In this paper we consider models for concurrent...

Verifying randomized distributed algorithms with prism (2000)

Verifying quantitative properties of continuous probabilistic timed automata (2000)

Abstract. In this paper we describe our experience with model checking randomized distributed algorithms using PRISM, a symbolic model checker for concurrent probabilistic systems currently being...

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

Abstract. We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [19], an extension...

J.Sproston. Verifying soft deadlines with probabilistic timed automata (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

Abstract. This paper describes work in progess performed as part of an ongoing project aimed at the development of theoretical foundations and model checking algorithms for the verification of soft...

Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation (2000)

Luca De Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

Abstract. This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent...

J.Sproston. Verifying soft deadlines with probabilistic timed automata (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

Abstract. This paper describes work in progess performed as part of an ongoing project aimed at the development of theoretical foundations and model checking algorithms for the verication of soft...

Verifying quantitative properties of continuous probabilistic timed automata (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider the problem of automatically verifying real-time systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [17], an extension of the...

Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation (2000)

Luca De Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

. This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent probabilistic...

Verifying Quantitative Properties of Continuous Probabilistic Timed Automata (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [19], an extension of the...

Verifying Soft Deadlines with Probabilistic Timed Automata (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

This paper describes work in progess performed as part of an ongoing project aimed at the development of theoretical foundations and model checking algorithms for the verification of soft deadlines...

Verifying Randomized Distributed Algorithms with PRISM (2000)

Model Checking Probabilistic Systems - Notes to accompany ESSLLI00 tutorial (2000)

. In this paper we describe our experience with model checking randomized distributed algorithms using PRISM, a symbolic model checker for concurrent probabilistic systems currently being developed....

Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability (2000)

`Model checking' is an algorithmic method which allows one to automatically verify whether a system model satisfies a given specification. Specifications are usually given as formulas of...

Automatic Verification of Real-time Systems with Discrete Probability Distributions (2000)

We consider probabilistic timed automata of [13], an extension of the timed automata model of [2] with discrete probability distributions. In contrast to timed automata, which model real-time systems...

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider the timed automata model of [3], which allows the analysis of realtime systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system...

Automatic Verification of Real-time Systems with Discrete Probability Distributions (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider the timed automata model of [3], which allows the analysis of realtime systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system...

Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation (2000)

Luca De Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent probabilistic...

Verifying Quantitative Properties of Continuous (2000)

Probabilistic Timed Automata, Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [19], an extension of the...

Verifying Quantitative Properties of Continuous Probabilistic Real-Time Graphs (2000)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider the problem of automatically verifying real-time systems with continuously distributed random delays. Our system model is an extension of the timed automata variant of [15], and exhibits...

Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation (2000)

Luca De Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent probabilistic...

Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation (2000)

Luca De Alfaro, Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

Automatic verification of real-time systems with discrete probability distributions (1999)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

Abstract. We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system...

and (1999)

Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

Symbolic model checking for purely probabilistic processes using MTBDDs [12] was introduced in [4] and further developed in [20, 3]. In this paper we consider models for concurrent probabilistic...

Automatic verication of real-time systems with discrete probability distributions (1999)

Marta Kwiatkowska, Roberto Segala, Jeremy Sproston

Abstract. We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system...

Computing Probability Bounds for Linear Time Formulas over Concurrent Probabilistic Systems (1999)

Christel Baier, Marta Kwiatkowska, Gethin Norman, Fakultat Fur Mathematik

Probabilistic verification of concurrent probabilistic systems against linear time specifications is known to be expensive in terms of time and space: time is double exponential in the size of the...

Model Checking of Probabilistic Systems Against Temporal Logic Specifications (1999)

Solving Infinite Stochastic Process Algebra Models through Matrix-Geometric Methods (1999)

`Model checking' is an algorithmic method which allows one to automatically verify whether a system model satisfies a given specification. Specifications are usually given as formulae of...

Amani El-Rayes, Marta Kwiatkowska, Gethin Norman

We introduce a Stochastic Process Algebra called PEPA 1 ph , based on Hillston's Performance Evaluation Process Algebra (PEPA). PEPA 1 ph is suitable for describing and analysing the performance...

Computing Probability Bounds for Linear Time Formulas over Concurrent Probabilistic Systems (1999)

Christel Baier, Marta Kwiatkowska, Gethin Norman, Fakultat Fur Mathematik

Probabilistic verification of concurrent probabilistic systems against linear time specifications is known to be expensive in terms of time and space: time is double exponential in the size of the...

Solving Infinite Stochastic Process Algebra Models through Matrix-Geometric Methods (1999)

Amani El-Rayes, Marta Kwiatkowska, Gethin Norman

We introduce a Stochastic Process Algebra called PEPA 1 ph , based on Hillston's PEPA [6]. PEPA 1 ph is suitable for describing the behaviour of certain kinds of networks of queues, such as...

Symbolic Model Checking of Concurrent Probabilistic Systems Using MTBDDs and Simplex (1999)

Marta Kwiatkowska, Gethin Norman, David Parker, Roberto Segala

Symbolic model checking for purely probabilistic processes using MTBDDs [12] was introduced in [4] and further developed in [20, 3]. In this paper we consider models for concurrent probabilistic...

Automatic Verification of Real-time Systems with Discrete Probability Distributions (1999)

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

. We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system...

Implementation of Symbolic Model Checking for Probabilistic Systems: Progress Report 3 - Thesis Proposal (1999)

David Parker, Marta Kwiatkowska, Mark Ryan, Achim Jung

In this report, we propose research to be carried out in the area of probabilistic symbolic model checking. Model checking is an automatable technique for the formal verification of finite state...

Model checking for a probabilistic branching time logic with fairness (1998)

Model checking for a probabilistic branching time logic with fairness (1998)

We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic choice between probability distributions. These systems can be...

Fakultat Fur Mathematik, Christel Baier, Marta Kwiatkowska

Summary. We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic choice between probability distributions. These...

Christel Baier (1998)

We consider sequential and concurrent probabilistic processes and propose a general notion of fairness with respect to probabilistic choice, which allows to express various notions of fairness such...

Computing Probability Lower and Upper Bounds for (1998)

Formulae Over, Christel Baier, Marta Kwiatkowska, Gethin Norman

Probabilistic verification of sequential and concurrent Markov chains against linear time specifications is known to be expensive in terms of time and space: time is exponential in the size of the...

Computing Probability Lower and Upper Bounds for Formulae over Sequential and Concurrent Markov Chains (1998)

Christel Baier, Marta Kwiatkowska, Gethin Norman

Probabilistic verification of sequential and concurrent Markov chains against linear time specifications is known to be expensive in terms of time and space: time is exponential in the size of the...

On the Verification of Qualitative Properties of Probabilistic Processes under Fairness Constraints (1998)

Verifying Quantitative Properties of Continuous Probabilistic Real-Time Graphs (1998)

We consider sequential and concurrent probabilistic processes and propose a general notion of fairness with respect to probabilistic choice, which allows to express various notions of fairness such...

Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston

We consider an extension of probabilistic real-time graphs with continuous-time probability distributions, based on the timed automata of [3] augmented with discrete probability distributions in...

Domain Equations for Probabilistic Processes (1997)

Christel Baier Fakultat, Christel Baier, Marta Kwiatkowska

In this paper we consider Milner's calculus CCS enriched by a probabilistic choice operator. The calculus is given operational semantics based on probabilistic transition systems. We define...

Symbolic Model Checking for Probabilistic Processes (1997)

Christel Baier Edmund, Edmund M. Clarke, Marta Kwiatkowska, Mark Ryan, Fakultat Fur Mathematik

. We introduce a symbolic model checking procedure for Probabilistic Computation Tree Logic PCTL over labelled Markov chains as models. Model checking for probabilistic logics typically involves...

Domain Equations for Probabilistic Processes (Extended (1997)

Te Nd Ed, Christel Baier, Marta Kwiatkowska

) Christel Baier Fakultat fur Mathematik & Informatik Universitat Mannheim 68131 Mannheim, Germany Marta Kwiatkowska 1 School of Computer Science University of Birmingham Edgbaston, Birmingham...

Quantitative Analysis and Model Checking (1997)

Symbolic Model Checking for Probabilistic Processes (1997)

Many notions of models in computer science provide quantitative information, or uncertainties, which necessitate a quantitative model checking paradigm. We present such a framework for reactive and...

Christel Baier, Marta Kwiatkowska, Mark Ryan

We introduce a symbolic model checking procedure for Probabilistic Computation Tree Logic (PCTL) and its generalization PCTL over labelled Markov chains as models. Model checking for probabilistic...

Automatic Verification of Liveness Properties of Randomized Systems (Extended Abstract (1997)

Quantitative Analysis and Model Checking (1997)

) Christel Baier Fakultat fur Mathematik & Informatik Universitat Mannheim 68131 Mannheim, Germany baier@pi1.informatik.uni-mannheim.de Marta Kwiatkowska School of Computer Science University of...

Automatic Verification of Liveness Properties of Randomized Systems (Extended Anstract) (1997)

Many notions of models in computer science provide quantitative information, or uncertainties, which necessitate a quantitative model checking paradigm. We present such a framework for reactive and...

Domain Equations for Probabilistic Processes (1997)

) Christel Baier Fakultat fur Mathematik & Informatik Universitat Mannheim 68131 Mannheim, Germany baier@pi1.informatik.uni-mannheim.de Marta Kwiatkowska School of Computer Science University of...

Domain Equations for Probabilistic Processes (1997)

) Christel Baier Fakultat fur Mathematik & Informatik Universitat Mannheim 68131 Mannheim, Germany Marta Kwiatkowska 1 School of Computer Science University of Birmingham Edgbaston, Birmingham...

Symbolic Model Checking for Probabilistic Processes (1997)

In this paper we consider Milner's calculus CCS enriched by a probabilistic choice operator. The calculus is given operational semantics based on probabilistic transition systems. We define...

Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Kwiatkowska, Mark Ryan, Fakultat Fur Mathematik

. We introduce a symbolic model checking procedure for Probabilistic Computation Tree Logic PCTL over labelled Markov chains as models. Model checking for probabilistic logics typically involves...

Symbolic Model Checking for Probabilistic Processes (1997)

Christel Baier Edmund, Edmund M. Clarke, Vasiliki Hartonas-garmhausen, Marta Kwiatkowska, Mark Ryan

We introduce a symbolic model checking procedure for Probabilistic Computation Tree Logic PCTL over labelled Markov chains as models. Model checking for probabilistic logics typically involves...

Probabilistic metric semantics for a simple language with recursion (1996)

On probabilistic model checking (1996)

Abstract. We consider a simple divergence-free language RP for reactive processes which includes prefixing, deterministic choice, actionguarded probabilistic choice, synchronous parallel and...

Analysing performance of lift systems in PEPA (1996)

Abstract. This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs...

Amani El-rayes, Marta Kwiatkowska, Steven Minton

We use the stochastic process algebra PEPA [8] to specify lift systems and analyse their performance. We focus on the mean passenger waiting time versus the speed of the lift (given by the slowest...

Metric denotational semantics for PEPA (1996)

Probabilistic metric semantics for a simple language with recursion (1996)

Stochastic process algebras, which combine the features of a process calculus with stochastic analysis, were introduced to enable compositional performance analysis of systems. At the level of...

On Topological Hierarchies of Temporal Properties (1996)

Abstract. We consider a simple divergence-free language RP for reactive processes which includes prexing, deterministic choice, actionguarded probabilistic choice, synchronous parallel and recursion....

Metric Denotational Semantics for PEPA (1996)

. The classification of properties of concurrent programs into safety and liveness was first proposed by Lamport [20]. Since then several characterizations of hierarchies of properties have been...

Model Checking for a Probabilistic Branching Time Logic with Fairness (1996)

We consider Performance Evaluation Process Algebra (PEPA), a stochastic process algebra introduced by Hillston [8]. Following the methodology introduced by de Bakker & Zucker and our earlier...

Christel Baier Fakultat, Christel Baier, Marta Kwiatkowska

We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [53], which allow non-deterministic choice between probability distributions. These systems can be...

Model Checking for a Probabilistic Branching Time Logic with Fairness (1996)

Probabilistic Metric Semantics for a Simple Language with Recursion (1996)

We consider probabilistic transition systems, based on probabilistic automata of Segala & Lynch [43], which distinguish between non-deterministic and probabilistic choice. These systems can be...

Metric Denotational Semantics for (1996)

. We consider a simple divergence-free language RP for reactive processes which includes prefixing, deterministic choice, actionguarded probabilistic choice, synchronous parallel and recursion. We...

Pepa Marta Kwiatkowska, Marta Kwiatkowska, Gethin Norman

Stochastic process algebras, which combine the features of a process calculus with stochastic analysis, were introduced to enable compositional performance analysis of systems. At the level of...

The Semantics Of Fair Recursion With Divergence (1996)

On Probabilistic Model Checking (1996)

We recast Milner's work on SCCSffl, a calculus for finite but unbounded delay based on SCCS, by giving a denotational semantics for admissibility of infinite computations on a bifinite domain K....

Finite But Unbounded Delay In Synchronous CCS (Extended Abstract) (1996)

We give a probabilistic semantics to formulas of the modal mu-calculus, where models are probabilistic transition systems and meanings are functions from states to the unit interval. The meaning of a...

Synchronization Trees And Fairness: A Case Study (1995)

ABSTRACT We recast Milner's work on finite delay in synchronous CCS by giving a denotational semantics for admissibility of infinite computations on a bifinite domain K. Using Abramsky's...

Chrysafis Hartonas, Marta Kwiatkowska

We generalise Winskel's trees [15] (which underlie the synchronization trees) to allow for fairness constraints to be modelled. We obtain a category of generalized trees, in which semantic...

A Hierarchy of Partial Order Temporal Properties (1994)

Marta Kwiatkowska, Doron Peled, Wojciech Penczek

We propose a classification of partial order temporal properties into a hierarchy, which is a generalization of the safety-progress hierarchy of Chang, Manna and Pnueli. The classes of the hierarchy...

A Hierarchy of Partial Order Temporal Properties (1994)

Marta Kwiatkowska, Doron Peled, Wojciech Penczek

We propose a classification of partial order temporal properties into a hierarchy, which is a generalization of the safety-progress hierarchy of Chang, Manna and Pnueli. The classes of the hierarchy...

On Duality for the Modal µ-Calculus (1994)

Simon Ambler, Marta Kwiatkowska, Nicholas Measor

. We consider the modal ¯-calculus due to Kozen, which is a finitary modal logic with least and greatest fixed points of monotone operators. We extend the existing duality between the category of...

Concurrency and conflict in CSP (1993)

Marta Kwiatkowska, Also Visiting, Iain Phillips

As part of an effort to give a "truly concurrent" semantics to process algebra, we refine the failures with divergence model for CSP by adding conflict information. We show that most of the...

Infinite Behaviour and Fairness in Concurrent Constraint Programming (1992)

Marta Kwiatkowska, Leicester Le Rh

In concurrent constraint programming, divergence (i.e. an infinite computation) and failure are often identified. This is undesirable when modelling systems in which infinite behaviour arises...

Trade-offs in True Concurrency: Pomsets and Mazurkiewicz Traces (1991)

Bloom, Bard, Kwiatkowska, Marta

We compare finite pomsets and Mazurkiewicz traces, two models of true concurrency which generalize strings. We show that Mazurkiewicz traces are equivalent to a restricted class of pomsets. The...

Trade-offs in True Concurrency: Pomsets and Mazurkiewicz Traces (1991)

Bloom, Bard, Kwiatkowska, Marta

We compare finite pomsets and Mazurkiewicz traces, two models of true concurrency which generalize strings. We show that Mazurkiewicz traces are equivalent to a restricted class of pomsets. The...

Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol