[logic-ml] lectures by Prof. Marta Kwiatkowska

[hagiya at is.s.u-tokyo.ac.jp]

確率モデル検査で著名な
Marta Kwiatkowska先生(University of Oxford)の
ご講演の案内です。(2件あります。)

===

日時: 2月15日(水) 15:30〜
場所: 東京大学理学部7号館007

A Framework for Verification of Software with Time and Probabilities

Marta Kwiatkowska, University of Oxford
(joint work with Gethin Norman and David Parker)

Quantitative verification techniques are able to establish system
properties such as "the probability of an airbag failing to deploy on
demand'' or "the expected time for a network protocol to successfully
send a message packet''. In this paper, we describe a framework for
quantitative verification of software that exhibits both real-time and
probabilistic behaviour. The complexity of real software, combined with
the need to capture precise timing information, necessitates the use of
abstraction techniques. We outline a quantitative abstraction refinement
approach, which can be used to automatically construct and analyse
abstractions of probabilistic, real-time programs. As a concrete example
of the potential applicability of our framework, we discuss the
challenges involved in applying it to the quantitative verification of
SystemC, an increasingly popular system-level modelling language.

===

日時: 2月17日(金) 15:30〜
場所: 東京大学理学部7号館007

Design and Analysis of DNA Strand Displacement Devices
using Probabilistic Model Checking

Marta Kwiatkowska, University of Oxford
(joint work with Matthew Lakin, David Parker, Luca Cardelli and Andrew
Phillips, to appear in Journal of the Royal Society Interface)

Designing correct, robust DNA devices is difficult because
of the many possibilities for unwanted interference
between molecules in the system. DNA strand displacement
has been proposed as a design paradigm for DNA
devices, and the DSD programming language has been
developed as a means of formally programming and analysing
these devices to check for unwanted interference.
We demonstrate, for the first time, the use of formal verification
techniques, in particular model checking and
probabilistic model checking, to analyse the correctness,
reliability and performance of DNA devices during the
design phase. We use the probabilistic model checker
PRISM, in combination with the DSD language, to design
and debug DNA strand displacement components
and to investigate their kinetics. We show how our techniques
can be used to identify design flaws and to evaluate
the merits of contrasting design decisions, even on
devices comprising relatively few inputs. We then demonstrate
the use of these components to construct a
DNA strand displacement device for approximate majority
voting. Finally, we discuss some of the challenges
and possible directions for applying these methods to
more complex designs.