32 Search Results for "Kwiatkowska, Marta"


Volume

OASIcs, Volume 36

5th Workshop on Medical Cyber-Physical Systems

MCPS 2014, April 14, 2014, Berlin, Germany

Editors: Volker Turau, Marta Kwiatkowska, Rahul Mangharam, and Christoph Weyer

Document
Invited Talk
Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk)

Authors: Marta Kwiatkowska

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
Strategic reasoning is essential to ensure stable multi-agent coordination in complex environments, as it enables synthesis of optimal (or near-optimal) agent strategies and equilibria that guarantee expected outcomes, even in adversarial scenarios. Partially-observable stochastic games (POSGs) are a natural model for real-world settings involving multiple agents, uncertainty and partial information, but lack practical algorithms for computing or approximating optimal values and strategies. Recently, progress has been made for one-sided POSGs, a subclass of two-agent, zero-sum POSGs where only one agent has partial information while the other agent is assumed to have full knowledge of the state, with heuristic search value iteration (HSVI) proposed for computing approximately optimal values and strategies in one-sided POSGs [Horák et al., 2023]. This model is well suited to safety-critical applications, when making worst-case assumptions about one agent; examples include the attacker in a security application, modelled, e.g., as a patrolling or pursuit-evasion game. However, many realistic autonomous coordination scenarios involve agents perceiving continuous environments using data-driven observation functions, typically implemented as neural networks (NNs). Examples include autonomous vehicles using NNs to perform object recognition or to estimate pedestrian intention, or NN-enabled vision in an airborne pursuit-evasion scenario. Such perception mechanisms bring new challenges, notably continuous environments, which are inherently tied to NN-enabled perception because of standard training regimes. This means that naive discretisation is difficult, since decision boundaries obtained for data-driven perception are typically irregular and can be misaligned with gridding schemes for discretisation, affecting the precision of the computed strategies. This invited paper will discuss progress with developing a model class and algorithms for one-sided POSGs with neural perception mechanisms [R. Yan et al., 2022; Yan et al., 2023] that work directly with their continuous state space. Building on continuous-state POMDPs with NN perception mechanisms [Yan et al., 2023], where the key idea is that ReLU neural network classifiers induce a finite decomposition of the continuous environment into polyhedra for each classification label, a piecewise constant representation for the value, reward and perception functions is developed that forms the basis for a variant of HSVI, a point-based solution method that computes a lower and upper bound on the value function from a given belief to compute an (approximately) optimal strategy. We extend these ideas from the single-agent (POMDP) setting [Yan et al., 2023] to zero-sum POSGs. In the game setting, this involves solving a normal form game at each stage and iteration, and goes significantly beyond HSVI for finite POSGs [Horák et al., 2023].

Cite as

Marta Kwiatkowska. Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.CSL.2024.5,
  author =	{Kwiatkowska, Marta},
  title =	{{Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.5},
  URN =		{urn:nbn:de:0030-drops-196471},
  doi =		{10.4230/LIPIcs.CSL.2024.5},
  annote =	{Keywords: Stochastic games, neural networks, formal verification, strategy synthesis}
}
Document
Invited Paper
CONCUR Test-Of-Time Award 2023 (Invited Paper)

Authors: Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the paper that received the Award in 2023.

Cite as

Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz. CONCUR Test-Of-Time Award 2023 (Invited Paper). In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.CONCUR.2023.1,
  author =	{Jonsson, Bengt and Kwiatkowska, Marta and Walukiewicz, Igor},
  title =	{{CONCUR Test-Of-Time Award 2023}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.1},
  URN =		{urn:nbn:de:0030-drops-189953},
  doi =		{10.4230/LIPIcs.CONCUR.2023.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
Invited Talk
Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk)

Authors: Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)


Abstract
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.

Cite as

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska_et_al:LIPIcs.MFCS.2022.4,
  author =	{Kwiatkowska, Marta and Norman, Gethin and Parker, David and Santos, Gabriel and Yan, Rui},
  title =	{{Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.4},
  URN =		{urn:nbn:de:0030-drops-168026},
  doi =		{10.4230/LIPIcs.MFCS.2022.4},
  annote =	{Keywords: Probabilistic model checking, stochastic games, equilibria}
}
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}
}
Document
Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491)

Authors: Antonio Filieri, Marta Kwiatkowska, Sasa Misailovic, and Todd Mytkowicz

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)


Abstract
Computing has entered the era of approximation, in which hardware and software generate and reason about estimates. Navigation applications turn maps and location estimates from hardware GPS sensors into driving directions; speech recognition turns an analog signal into a likely sentence; search turns queries into information; network protocols deliver unreliable messages; and recent advances promise that approximate hardware and software will trade result quality for energy efficiency. Millions of people already use software which computes with and reasons about approximate/probabilistic data daily. These complex systems require sophisticated algorithms to deliver accurate answers quickly, at scale, and with energy efficiency, and approximation is often the only way to meet these competing goals. Despite their ubiquity, economic significance, and societal impact, building such applications is difficult and requires expertise across the system stack, in addition to statistics and application-specific domain knowledge. Non-expert developers need tools and expertise to help them design, code, and verify these complex systems. The aim of this seminar was to bring together academic and industrial researchers from the areas of probabilistic model checking, quantitative software analysis, probabilistic programming, and approximate computing to share their recent progress, identify challenges in computing with estimates, and foster collaboration with the goal of helping non-expert developers design, code, and verify modern approximate and probabilistic systems.

Cite as

Antonio Filieri, Marta Kwiatkowska, Sasa Misailovic, and Todd Mytkowicz. Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491). In Dagstuhl Reports, Volume 5, Issue 11, pp. 151-179, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{filieri_et_al:DagRep.5.11.151,
  author =	{Filieri, Antonio and Kwiatkowska, Marta and Misailovic, Sasa and Mytkowicz, Todd},
  title =	{{Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491)}},
  pages =	{151--179},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{Filieri, Antonio and Kwiatkowska, Marta and Misailovic, Sasa and Mytkowicz, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.11.151},
  URN =		{urn:nbn:de:0030-drops-58008},
  doi =		{10.4230/DagRep.5.11.151},
  annote =	{Keywords: approximation, model checking, performance, probability, program analysis, systems, verification}
}
Document
Invited Paper
Parameter synthesis for probabilistic real-time systems (Invited Paper)

Authors: Marta Kwiatkowska

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)


Abstract
The parameter synthesis problem aims to find parameter valuations that guarantee that a given objective is satisfied for a parametric model. Applications range from automated model repair to optimisation. This lecture will focus on models with probability and real-time and give an overview of recent results concerning parameter synthesis from quantitative temporal logic objectives. Existing algorithmic approaches and experimental results will be discussed, and future research challenges outlined.

Cite as

Marta Kwiatkowska. Parameter synthesis for probabilistic real-time systems (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, p. 16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska:OASIcs.SynCoP.2015.16,
  author =	{Kwiatkowska, Marta},
  title =	{{Parameter synthesis for probabilistic real-time systems}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{16--16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.16},
  URN =		{urn:nbn:de:0030-drops-56062},
  doi =		{10.4230/OASIcs.SynCoP.2015.16},
  annote =	{Keywords: Quantitative verification, Timed automata, Parameter synthesis}
}
Document
Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041)

Authors: Samuel Kounev, Xiaoyun Zhu, Jeffrey O. Kephart, and Marta Kwiatkowska

Published in: Dagstuhl Reports, Volume 5, Issue 1 (2015)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15041 "Model-driven Algorithms and Architectures for Self-Aware Computing Systems". The design of self-aware computing systems calls for an integrated interdisciplinary approach building on results from multiple areas of computer science and engineering, including software and systems engineering, systems modeling, simulation and analysis, autonomic and organic computing, machine learning and artificial intelligence, data center resource management, and so on. The Dagstuhl Seminar 15041 served as a platform to raise the awareness about the relevant research efforts in the respective research communities as well as existing synergies that can be exploited to advance the state-of-the-art, formulate a new research agenda that takes a broader view on the problem following an integrated and interdisciplinary approach, and establish collaborations between academia and industry.

Cite as

Samuel Kounev, Xiaoyun Zhu, Jeffrey O. Kephart, and Marta Kwiatkowska. Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041). In Dagstuhl Reports, Volume 5, Issue 1, pp. 164-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{kounev_et_al:DagRep.5.1.164,
  author =	{Kounev, Samuel and Zhu, Xiaoyun and Kephart, Jeffrey O. and Kwiatkowska, Marta},
  title =	{{Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041)}},
  pages =	{164--196},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{1},
  editor =	{Kounev, Samuel and Zhu, Xiaoyun and Kephart, Jeffrey O. and Kwiatkowska, Marta},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.1.164},
  URN =		{urn:nbn:de:0030-drops-50385},
  doi =		{10.4230/DagRep.5.1.164},
  annote =	{Keywords: autonomic systems, self-adaptive, self-managing, model-driven, architecture-based, systems management, machine learning, feedback-based design}
}
Document
Complete Volume
OASIcs, Volume 36, MCPS'14, Complete Volume

Authors: Volker Turau, Marta Kwiatkowska, Rahul Mangharam, and Christoph Weyer

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
OASIcs, Volume 36, MCPS'14, Complete Volume

Cite as

5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@Proceedings{turau_et_al:OASIcs.MCPS.2014,
  title =	{{OASIcs, Volume 36, MCPS'14, Complete Volume}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014},
  URN =		{urn:nbn:de:0030-drops-45403},
  doi =		{10.4230/OASIcs.MCPS.2014},
  annote =	{Keywords: Conference proceedings}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Volker Turau, Marta Kwiatkowska, Rahul Mangharam, and Christoph Weyer

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization

Cite as

5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{turau_et_al:OASIcs.MCPS.2014.i,
  author =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{i--x},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.i},
  URN =		{urn:nbn:de:0030-drops-45174},
  doi =		{10.4230/OASIcs.MCPS.2014.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software

Authors: Paolo Masci, Yi Zhang, Paul Jones, Harold Thimbleby, and Paul Curzon

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
This paper presents a generic infusion pump user interface (GIP-UI) architecture that intends to capture the common characteristics and functionalities of interactive software incorporated in broad classes of infusion pumps. It is designed to facilitate the identification of use hazards and their causes in infusion pump designs. This architecture constitutes our first effort at establishing a model-based risk analysis methodology that helps manufacturers identify and mitigate use hazards in their products at early stages of the development life-cycle. The applicability of the GIP-UI architecture has been confirmed in a hazard analysis focusing on the number entry software of existing infusion pumps, in which the GIP-UI architecture is used to identify a substantial set of user interface design errors that may contribute to use hazards found in infusion pump incidents.

Cite as

Paolo Masci, Yi Zhang, Paul Jones, Harold Thimbleby, and Paul Curzon. A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{masci_et_al:OASIcs.MCPS.2014.1,
  author =	{Masci, Paolo and Zhang, Yi and Jones, Paul and Thimbleby, Harold and Curzon, Paul},
  title =	{{A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{1--14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.1},
  URN =		{urn:nbn:de:0030-drops-45185},
  doi =		{10.4230/OASIcs.MCPS.2014.1},
  annote =	{Keywords: Infusion Pump, Hazard analysis, Use hazards, User Interface, Interactive software, Design errors}
}
Document
An Approach to Integrate Distributed Systems of Medical Devices in High Acuity Environments

Authors: David Gregorczyk, Stefan Fischer, Timm Busshaus, Stefan Schlichting, and Stephan Pöhlsen

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
This paper presents a comprehensive solution to build a distributed system of medical devices in high acuity environments. It is based on the concept of a Service Oriented Medical Device Architecture. It uses the Devices Profile for Web Services as a transport layer protocol and enhances it to the Medical Devices Profile for Web Service (MDPWS) to meet medical requirements. By applying the ISO/IEEE 11073 Domain Information Model, device data can be semantically described and exchanged by means of a generic service interface. Data model and service interface are subsumed under the Basic Integrated Clinical Environment Specification (BICEPS). MDPWS and BICEPS are implemented as part of the publically available openSDC stack. Performance measurements and a real world setup prove that openSDC is feasible to be deployed in distributed systems of medical devices.

Cite as

David Gregorczyk, Stefan Fischer, Timm Busshaus, Stefan Schlichting, and Stephan Pöhlsen. An Approach to Integrate Distributed Systems of Medical Devices in High Acuity Environments. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 15-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{gregorczyk_et_al:OASIcs.MCPS.2014.15,
  author =	{Gregorczyk, David and Fischer, Stefan and Busshaus, Timm and Schlichting, Stefan and P\"{o}hlsen, Stephan},
  title =	{{An Approach to Integrate Distributed Systems of Medical Devices in High Acuity Environments}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{15--27},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.15},
  URN =		{urn:nbn:de:0030-drops-45191},
  doi =		{10.4230/OASIcs.MCPS.2014.15},
  annote =	{Keywords: Integrated Clinical Environment, Devices Profile for Web Services, ISO/IEEE 11073}
}
Document
Simulations of the Cardiovascular System Using the Cardiovascular Simulation Toolbox

Authors: Gabriela Ortiz-León, Marta Vílchez-Monge, and Juan J. Montero-Rodríguez

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
In the present document, six mathematical models of the cardiovascular system are studied and implemented in MATLAB R2013a using an updated version of the Cardiovascular Simulation Toolbox proposed by O. Barnea at the Tel-Aviv University. All the mathematical models are based on electrical lumped-parameter analogies. The results of the simulations are compared with a list of expected hemodynamic parameters and contrasted with laboratory values.

Cite as

Gabriela Ortiz-León, Marta Vílchez-Monge, and Juan J. Montero-Rodríguez. Simulations of the Cardiovascular System Using the Cardiovascular Simulation Toolbox. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 28-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{ortizleon_et_al:OASIcs.MCPS.2014.28,
  author =	{Ortiz-Le\'{o}n, Gabriela and V{\'\i}lchez-Monge, Marta and Montero-Rodr{\'\i}guez, Juan J.},
  title =	{{Simulations of the Cardiovascular System Using the Cardiovascular Simulation Toolbox}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{28--37},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.28},
  URN =		{urn:nbn:de:0030-drops-45207},
  doi =		{10.4230/OASIcs.MCPS.2014.28},
  annote =	{Keywords: Biomedic, Cardiovascular, MATLAB, Simulation}
}
Document
Adaptive Failure Detection and Correction in Dynamic Patient-Networks

Authors: Martin Ringwelski, Andreas Timm-Giel, and Volker Turau

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)


Abstract
Wireless sensors have been studied over recent years for different promising applications with high value for individuals and society. A good example are wireless sensor networks for patients allowing for better and more efficient monitoring of patients in hospitals or even early discharge form hospital and monitoring at home. These visions have hardly led research as reliability is and issue with wireless networks to be known error-prone. In life critical applications like health care this is not an aspect to be handled carelessly. Fail-safety is an important property for patient monitoring systems. The AA4R project of the Hamburg University of Technology researches on a fail-safe patient monitoring system. Our vision is a dynamically distributed system using suitable devices in the area of a patient. The data in the network is stored with redundancy on several nodes. Patient data is analyzed in the network and uploaded to a medical server. As devices appear, disappear and fail, so do the services being executed on those devices. This article focuses on a Reincarnation Service (RS) to track the functionality of the processes. The RS takes suitable actions when a failure is detected to correct or isolate the failure. Checking of the nodes is done adaptively to achieve a good response time to failures and reduce the power consumption.

Cite as

Martin Ringwelski, Andreas Timm-Giel, and Volker Turau. Adaptive Failure Detection and Correction in Dynamic Patient-Networks. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 38-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{ringwelski_et_al:OASIcs.MCPS.2014.38,
  author =	{Ringwelski, Martin and Timm-Giel, Andreas and Turau, Volker},
  title =	{{Adaptive Failure Detection and Correction in Dynamic Patient-Networks}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{38--48},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.38},
  URN =		{urn:nbn:de:0030-drops-45215},
  doi =		{10.4230/OASIcs.MCPS.2014.38},
  annote =	{Keywords: Wireless Sensor Networks, Fail-Safety, Health Monitoring, Failure Masking, Distributed Systems}
}
  • Refine by Author
  • 13 Kwiatkowska, Marta
  • 3 Jonsson, Bengt
  • 3 Turau, Volker
  • 2 Arney, David
  • 2 Goldman, Julian M.
  • Show More...

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

  • Refine by Keyword
  • 2 Infusion Pump
  • 2 Quantitative verification
  • 2 Simulation
  • 2 Stochastic games
  • 2 Verification
  • Show More...

  • Refine by Type
  • 31 document
  • 1 volume

  • Refine by Publication Year
  • 19 2014
  • 3 2010
  • 2 2015
  • 2 2016
  • 1 2000
  • Show More...

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