Gethin Norman

I&C Journal 2024 Journal Article

Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games

• Rui Yan
• Gabriel Santos
• Gethin Norman
• David Parker
• Marta Kwiatkowska

Neuro-symbolic approaches to artificial intelligence, which combine neural networks with classical symbolic techniques, are growing in prominence, necessitating formal approaches to reason about their correctness. We propose a novel modelling formalism called neuro-symbolic concurrent stochastic games (NS-CSGs), which comprise two probabilistic finite-state agents interacting in a shared continuous-state environment. Each agent observes the environment using a neural perception mechanism, which converts inputs such as images into symbolic percepts, and makes decisions symbolically. We focus on the class of NS-CSGs with Borel state spaces and prove the existence and measurability of the value function for zero-sum discounted cumulative rewards under piecewise-constant restrictions. To compute values and synthesise strategies, we first introduce a Borel measurable piecewise-constant (B-PWC) representation of value functions and propose a B-PWC value iteration. Second, we introduce two novel representations for the value functions and strategies, and propose a minimax-action-free policy iteration based on alternating player choices.

MFCS Conference 2022 Conference Paper

Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk)

• Marta Kwiatkowska
• Gethin Norman
• David Parker 0001
• Gabriel Santos
• Rui Yan 0002

Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined.

TCS Journal 2017 Journal Article

Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata

• Aleksandra Jovanović
• Marta Kwiatkowska
• Gethin Norman
• Quentin Peyras

In this paper we consider the problem of computing the optimal (minimum or maximum) expected time to reach a target and the synthesis of an optimal controller for a probabilistic timed automaton (PTA). Although this problem admits solutions that employ the digital clocks abstraction or statistical model checking, symbolic methods based on zones and priced zones fail due to the difficulty of incorporating probabilistic branching in the context of dense time. We work in a generalisation of the setting introduced by Asarin and Maler for the corresponding problem for timed automata, where simple and nice functions are introduced to ensure finiteness of the dense-time representation. We find restrictions sufficient for value iteration to converge to the optimal expected time on the uncountable Markov decision process representing the semantics of a PTA. We formulate Bellman operators on the backwards zone graph of a PTA and prove that value iteration using these operators equals that computed over the PTA's semantics. This enables us to extract an ε-optimal controller from value iteration in the standard way.

TCS Journal 2016 Journal Article

Expected reachability-time games

• Vojtěch Forejt
• Marta Kwiatkowska
• Gethin Norman
• Ashutosh Trivedi

Probabilistic timed automata are a suitable formalism to model systems with real-time, nondeterministic and probabilistic behaviour. We study two-player zero-sum games on such automata where the objective of the game is specified as the expected time to reach a target. The two players—called player Min and player Max—compete by proposing timed moves simultaneously and the move with a shorter delay is performed. The first player attempts to minimise the given objective while the second tries to maximise the objective. We observe that these games are not determined, and study decision problems related to computing the upper and lower values, showing that the problems are decidable and lie in the complexity class NEXPTIME ∩ co-NEXPTIME.

TCS Journal 2014 Journal Article

Quantitative Aspects of Programming Languages and Systems (2011–12)

• Mieke Massink
• Gethin Norman
• Herbert Wiklicky

I&C Journal 2013 Journal Article

Compositional probabilistic verification through multi-objective model checking

• Marta Kwiatkowska
• Gethin Norman
• David Parker
• Hongyang Qu

Compositional approaches to verification offer a powerful means to address the challenge of scalability. In this paper, we develop techniques for compositional verification of probabilistic systems based on the assume-guarantee paradigm. We target systems that exhibit both nondeterministic and stochastic behaviour, modelled as probabilistic automata, and augment these models with costs or rewards to reason about, for example, energy usage or performance metrics. Despite significant theoretical advances in compositional reasoning for probabilistic automata, there has been a distinct lack of practical progress regarding automated verification. We propose a new assume-guarantee framework based on multi-objective probabilistic model checking which supports compositional verification for a range of quantitative properties, including probabilistic ω-regular specifications and expected total cost or reward measures. We present a wide selection of assume-guarantee proof rules, including asymmetric, circular and asynchronous variants, and also show how to obtain numerical results in a compositional fashion. Given appropriate assumptions to be used in the proof rules, our compositional verification methods are, in contrast to previously proposed approaches, efficient and fully automated. Experimental results demonstrate their practical applicability on several large case studies, including instances where conventional probabilistic verification is infeasible.

TCS Journal 2012 Journal Article

Editorial: Quantitative Aspects of Programming Languages

• Alessandra Di Pierro
• Gethin Norman

TCS Journal 2009 Journal Article

Probabilistic Mobile Ambients

• Marta Kwiatkowska
• Gethin Norman
• David Parker
• Maria Grazia Vigliotti

The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network.

TCS Journal 2008 Journal Article

Probabilistic model checking of complex biological pathways

• John Heath
• Marta Kwiatkowska
• Gethin Norman
• David Parker
• Oksana Tymchyshyn

Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we illustrate its applicability to a complex biological system: the FGF (Fibroblast Growth Factor) signalling pathway. We give a detailed description of how this case study can be modelled in the probabilistic model checker PRISM, discussing some of the issues that arise in doing so, and show how we can thus examine a rich selection of quantitative properties of this model. We present experimental results for the case study under several different scenarios and provide a detailed analysis, illustrating how this approach can be used to yield a better understanding of the dynamics of the pathway. Finally, we outline a number of exact and approximate techniques to enable the verification of larger and more complex pathways and apply several of them to the FGF case study.

I&C Journal 2007 Journal Article

Symbolic model checking for probabilistic timed automata

• Marta Kwiatkowska
• Gethin Norman
• Jeremy Sproston
• Fuzhi Wang

Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.

TCS Journal 2002 Journal Article

Automatic verification of real-time systems with discrete probability distributions

• Marta Kwiatkowska
• Gethin Norman
• Roberto Segala
• Jeremy Sproston

We consider the timed automata model of Alur and Dill (Theoret. Comput. Sci. 126 (1994) 183–235), which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, it is often desirable to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, two approaches to model checking are introduced for this model. The first uses the algorithm of Baier and Kwiatkowska (Distributed Comput. 11 (1998) 125–155) to provide a verification technique against temporal logic formulae which can refer both to timing properties and probabilities. The second, generally more efficient, technique concerns the verification of probabilistic, real-time reachability properties.

MFCS Conference 1996 Conference Paper

Probabilistic Metric Semantics for a Simple Language with Recursion

• Marta Kwiatkowska
• Gethin Norman

Abstract We consider a simple divergence-free language RP for reactive processes which includes prefixing, deterministic choice, actionguarded probabilistic choice, synchronous parallel and recursion. We show that the probabilistic bisimulation of Larsen & Skou is a congruence for this language. Following the methodology introduced by de Bakker & Zucker we give denotational semantics to this language by means of a complete metric space of (deterministic) probabilistic trees defined in terms of the powerdomain of closed sets. This new metric, although not an ultra-metric, nevertheless specialises to the metric of de Bakker & Zucker. Our semantic domain admits a full abstraction result with respect to probabilistic bisimulation.