DROPS

Document

Verifiably Secure Process-Aware Information Systems (Dagstuhl Seminar 13341)

Authors: Rafael Accorsi, Jason Crampton, Michael Huth, and Stefanie Rinderle-Ma

Published in: Dagstuhl Reports, Volume 3, Issue 8 (2013)

Abstract

From August 18--23, 2013, the Dagstuhl Seminar "Verifiably Secure Process-aware Information Systems" was held in Schloss Dagstuhl -- Leibniz Center for Informatics. During this seminar, participants presented their current research and discussed open problems in the arising field of securing information systems driven by processes. The executive summary and abstracts of the talks given during the seminar are put together in this paper.

Cite as

Rafael Accorsi, Jason Crampton, Michael Huth, and Stefanie Rinderle-Ma. Verifiably Secure Process-Aware Information Systems (Dagstuhl Seminar 13341). In Dagstuhl Reports, Volume 3, Issue 8, pp. 73-86, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{accorsi_et_al:DagRep.3.8.73,
  author =	{Accorsi, Rafael and Crampton, Jason and Huth, Michael and Rinderle-Ma, Stefanie},
  title =	{{Verifiably Secure Process-Aware Information Systems (Dagstuhl Seminar 13341)}},
  pages =	{73--86},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{8},
  editor =	{Accorsi, Rafael and Crampton, Jason and Huth, Michael and Rinderle-Ma, Stefanie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.8.73},
  URN =		{urn:nbn:de:0030-drops-43435},
  doi =		{10.4230/DagRep.3.8.73},
  annote =	{Keywords: Business Processes, Information Security, Compliance, Risk-Aware Processes, Service Compositions}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2009.2323

Verification and Refutation of Probabilistic Specifications via Games

Authors: Mark Kattenbelt and Michael Huth

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract

We develop an abstraction-based framework to check probabilistic specifications of Markov Decision Processes (MDPs) using the stochastic two-player game abstractions (\ie ``games'') developed by Kwiatkowska et al.\ as a foundation. We define an abstraction preorder for these game abstractions which enables us to identify many new game abstractions for each MDP --- ranging from compact and imprecise to complex and precise. This added ability to trade precision for efficiency is crucial for scalable software model checking, as precise abstractions are expensive to construct in practice. Furthermore, we develop a four-valued probabilistic computation tree logic (PCTL) semantics for game abstractions. Together, the preorder and PCTL semantics comprise a powerful verification and refutation framework for arbitrary PCTL properties of MDPs.

Cite as

Mark Kattenbelt and Michael Huth. Verification and Refutation of Probabilistic Specifications via Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 251-262, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{kattenbelt_et_al:LIPIcs.FSTTCS.2009.2323,
  author =	{Kattenbelt, Mark and Huth, Michael},
  title =	{{Verification and Refutation of Probabilistic Specifications via Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{251--262},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2323},
  URN =		{urn:nbn:de:0030-drops-23233},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2323},
  annote =	{Keywords: Probabilistic model checking, Markov decision processes, Abstraction preorder, Stochastic two-player games}
}

Search Results

Documents authored by Huth, Michael

Verifiably Secure Process-Aware Information Systems (Dagstuhl Seminar 13341)

Abstract

Cite as

Verification and Refutation of Probabilistic Specifications via Games

Abstract

Cite as

Thanks for your feedback!

Could not send message