2 Search Results for "Kwiatkowska, Marta Z."


Document
Invited Paper
Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper)

Authors: Marta Z. Kwiatkowska

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
Computing systems are becoming ever more complex, increasingly often incorporating deep learning components. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning. This paper describes progress with developing automated verification techniques for deep neural networks to ensure safety and robustness of their decisions with respect to input perturbations. This includes novel algorithms based on feature-guided search, games, global optimisation and Bayesian methods.

Cite as

Marta Z. Kwiatkowska. Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.CONCUR.2019.1,
  author =	{Kwiatkowska, Marta Z.},
  title =	{{Safety Verification for Deep Neural Networks with Provable Guarantees}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{1:1--1:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.1},
  URN =		{urn:nbn:de:0030-drops-109036},
  doi =		{10.4230/LIPIcs.CONCUR.2019.1},
  annote =	{Keywords: Neural networks, robustness, formal verification, Bayesian neural networks}
}
Document
Invited Talk
Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk)

Authors: Marta Z. Kwiatkowska

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying quantitative probabilistic specifications such as the probability of a critical failure occurring or expected time to termination. Much progress has been made in recent years in algorithms, tools and applications of probabilistic model checking, as exemplified by the probabilistic model checker PRISM (http://www.prismmodelchecker.org). However, the unstoppable rise of autonomous systems, from robotic assistants to self-driving cars, is placing greater and greater demands on quantitative modelling and verification technologies. To address the challenges of autonomy we need to consider collaborative, competitive and adversarial behaviour, which is naturally modelled using game-theoretic abstractions, enhanced with stochasticity arising from randomisation and uncertainty. This paper gives an overview of quantitative verification and strategy synthesis techniques developed for turn-based stochastic multi-player games, summarising recent advances concerning multi-objective properties and compositional strategy synthesis. The techniques have been implemented in the PRISM-games model checker built as an extension of PRISM.

Cite as

Marta Z. Kwiatkowska. Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.ICALP.2016.4,
  author =	{Kwiatkowska, Marta Z.},
  title =	{{Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.4},
  URN =		{urn:nbn:de:0030-drops-62285},
  doi =		{10.4230/LIPIcs.ICALP.2016.4},
  annote =	{Keywords: Quantitative verification, Stochastic games, Temporal logic, Model checking, Strategy synthesis}
}
  • Refine by Author
  • 2 Kwiatkowska, Marta Z.

  • Refine by Classification
  • 1 Computing methodologies → Neural networks
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Bayesian neural networks
  • 1 Model checking
  • 1 Neural networks
  • 1 Quantitative verification
  • 1 Stochastic games
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2016
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail