-
Learning Algorithms for Verification of Markov Decision Processes
Authors:
Tomáš Brázdil,
Krishnendu Chatterjee,
Martin Chmelik,
Vojtěch Forejt,
Jan Křetínský,
Marta Kwiatkowska,
Tobias Meggendorfer,
David Parker,
Mateusz Ujma
Abstract:
We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}z…
▽ More
We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{á}zdil et al., significantly extending it as well as refining several details and fixing errors.
The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stop** criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.
△ Less
Submitted 20 March, 2024; v1 submitted 14 March, 2024;
originally announced March 2024.
-
Consumer Wearables and Affective Computing for Wellbeing Support
Authors:
Stanisław Saganowski,
Przemysław Kazienko,
Maciej Dzieżyc,
Patrycja Jakimów,
Joanna Komoszyńska,
Weronika Michalska,
Anna Dutkowiak,
Adam Polak,
Adam Dziadek,
Michał Ujma
Abstract:
Wearables equipped with pervasive sensors enable us to monitor physiological and behavioral signals in our everyday life. We propose the WellAff system able to recognize affective states for wellbeing support. It also includes health care scenarios, in particular patients with chronic kidney disease (CKD) suffering from bipolar disorders. For the need of a large-scale field study, we revised over…
▽ More
Wearables equipped with pervasive sensors enable us to monitor physiological and behavioral signals in our everyday life. We propose the WellAff system able to recognize affective states for wellbeing support. It also includes health care scenarios, in particular patients with chronic kidney disease (CKD) suffering from bipolar disorders. For the need of a large-scale field study, we revised over 50 off-the-shelf devices in terms of usefulness for emotion, stress, meditation, sleep, and physical activity recognition and analysis. Their usability directly comes from the types of sensors they possess as well as the quality and availability of raw signals. We found there is no versatile device suitable for all purposes. Using Empatica E4 and Samsung Galaxy Watch, we have recorded physiological signals from 11 participants over many weeks. The gathered data enabled us to train a classifier that accurately recognizes strong affective states.
△ Less
Submitted 12 August, 2021; v1 submitted 30 April, 2020;
originally announced May 2020.
-
Emotion Recognition Using Wearables: A Systematic Literature Review Work in progress
Authors:
Stanisław Saganowski,
Anna Dutkowiak,
Adam Dziadek,
Maciej Dzieżyc,
Joanna Komoszyńska,
Weronika Michalska,
Adam Polak,
Michał Ujma,
Przemysław Kazienko
Abstract:
Wearables like smartwatches or wrist bands equipped with pervasive sensors enable us to monitor our physiological signals. In this study, we address the question whether they can help us to recognize our emotions in our everyday life for ubiquitous computing. Using the systematic literature review, we identified crucial research steps and discussed the main limitations and problems in the domain.
Wearables like smartwatches or wrist bands equipped with pervasive sensors enable us to monitor our physiological signals. In this study, we address the question whether they can help us to recognize our emotions in our everyday life for ubiquitous computing. Using the systematic literature review, we identified crucial research steps and discussed the main limitations and problems in the domain.
△ Less
Submitted 15 January, 2020; v1 submitted 22 December, 2019;
originally announced December 2019.
-
Permissive Controller Synthesis for Probabilistic Systems
Authors:
Klaus Drager,
Vojtech Forejt,
Marta Kwiatkowska,
David Parker,
Mateusz Ujma
Abstract:
We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system ch…
▽ More
We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissivity using penalties, which are incurred each time a possible control action is disallowed by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.
△ Less
Submitted 29 June, 2015; v1 submitted 17 April, 2015;
originally announced April 2015.
-
Verification of Markov Decision Processes using Learning Algorithms
Authors:
Tomáš Brázdil,
Krishnendu Chatterjee,
Martin Chmelík,
Vojtěch Forejt,
Jan Křetínský,
Marta Kwiatkowska,
David Parker,
Mateusz Ujma
Abstract:
We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations…
▽ More
We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stop** criteria for the approximation. The latter is the first extension of statistical model-checking for unbounded properties in MDPs. In contrast with other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular properties of the MDP. We also show how our techniques extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.
△ Less
Submitted 30 March, 2015; v1 submitted 10 February, 2014;
originally announced February 2014.
-
jpf-concurrent: An extension of Java PathFinder for java.util.concurrent
Authors:
Mateusz Ujma,
Nastaran Shafiei
Abstract:
One of the main challenges when verifying multi-threaded Java applications is the state space explosion problem. Due to thread interleavings, the number of states that the model checker has to verify can grow rapidly and impede the feasibility of verification. In the Java language, the source of thread interleavings can be the system under test as well as the Java Development Kit (JDK) itself. In…
▽ More
One of the main challenges when verifying multi-threaded Java applications is the state space explosion problem. Due to thread interleavings, the number of states that the model checker has to verify can grow rapidly and impede the feasibility of verification. In the Java language, the source of thread interleavings can be the system under test as well as the Java Development Kit (JDK) itself. In our paper, we propose a method to minimize the state space explosion problem for applications verified under the Java PathFinder (JPF) model checker. Our method is based on abstracting the state of the application to a smaller domain and implementing application behavior using the Model Java Interface (MJI) of JPF. To show the capabilities of our approach, we have created a JPF extension called jpf-concurrent which abstracts classes from the Java Concurrency Utilities. Several benchmarks proved the usefulness of our approach. In all cases, our implementation was faster than the JDK implementation when running under the JPF model checker. Moreover, our implementation led to significantly smaller state spaces.
△ Less
Submitted 30 April, 2012;
originally announced May 2012.
