-
Chapter and Conference Paper
A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties
We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and -player Rabin games. To our best knowledge, our tools ...
-
Chapter and Conference Paper
Verification of Quantum Systems Using Barrier Certificates
Various techniques have been used in recent years for verifying quantum computers, that is, for determining whether a quantum computer/system satisfies a given formal specification of correctness. Barrier cert...
-
Chapter
Control and Management of Active Buildings
The power network is becoming increasingly intermittent as the contribution from renewable energy generation rises. To maintain stability and functionality of the power network, storage of renewable energies a...
-
Chapter and Conference Paper
Data-Driven Reachability Analysis of Digital Twin FMI Models
Digital Twins are an emerging technology which makes it possible to couple cyber-physical assets with their virtual representation in real-time. The technology is applicable to a variety of domains and facilit...
-
Chapter and Conference Paper
A Direct Symbolic Algorithm for Solving Stochastic Rabin Games
We consider turn-based stochastic 2-player games on graphs with \(\omega \) ω ...
-
Chapter
Operation and Control of a Population of Active Buildings at Network Level
Smart grid control and management is a growing research area that affects the global goals of net-zero emissions, increased renewable energy generation, and efficient energy management. Active buildings are th...
-
Chapter and Conference Paper
Stochastic Simulation Techniques for Inference and Sensitivity Analysis of Bayesian Attack Graphs
A vulnerability scan combined with information about a computer network can be used to create an attack graph, a model of how the elements of a network could be used in an attack to reach specific states or go...
-
Chapter and Conference Paper
AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
In this paper, we propose a software tool, called AMYTISS, implemented in C++/OpenCL, for designing correct-by-construction controllers for large-scale discrete-time stochastic systems. This tool is employed to (...
-
Chapter and Conference Paper
Formal Policy Synthesis for Continuous-State Systems via Reinforcement Learning
This paper studies satisfaction of temporal properties on unknown stochastic processes that have continuous state spaces. We show how reinforcement learning (RL) can be applied for computing policies that are ...
-
Chapter and Conference Paper
Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems
In this paper, we propose a compositional approach for constructing abstractions of general Markov decision processes (gMDPs) using approximate probabilistic relations
-
Chapter and Conference Paper
Temporal Logic Verification of Stochastic Systems Using Barrier Certificates
This paper presents a methodology for temporal logic verification of discrete-time stochastic systems. Our goal is to find a lower bound on the probability that a complex temporal property is satisfied by fini...
-
Chapter and Conference Paper
Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach
Time bounded reachability is a fundamental problem in model checking continuous-time Markov chains (CTMCs) and Markov decision processes (CTMDPs) for specifications in continuous stochastic logics. It can be c...
