Image of parts of the group from May 2023

The Learning in Verification group (LiVe Lab) focuses on the interactions of machine learning and verification. Our research includes Explainable AI, Verification of Neural Networks, Stochastic Games and Control, Probabilistic Model Checking, Temporal Logics (mainly LTL, PCTL), and Automata Theory. Our research is applicable in the Robotics, Biomedical, and Automotive domains. The team is distributed between the Masaryk University Brno, Czech Republic, and the Technical University of Munich, Germany.

News

Older posts…

Research Areas

Neural Network Safety

Runtime Monitoring of Neural Network

Runtime Monitoring of Neural Network

We develop runtime monitors for neural networks to improve their reliability.

Read more »

Abstraction of Neural Network

We abstract neural networks to improve verification speed.

Read more »

Automata and Logic

Teaching Automata

We aim to provide support for teaching automata.

Read more »

Machine Learning for LTL Synthesis

We apply machine learning to the LTL synthesis problem.

Read more »

Translating LTL to Automata

We design algorithms for translating LTL to different types of automata.

Read more »

Learning Temporal Formulae

We apply machine learning to the LTL synthesis problem.

Read more »

Explainability

Explaining Controllers via Decision Trees

We develop methods for explaining controllers with decision trees.

Read more »

Explaining Controllers via Automata

We develop methods for explaining controllers via automata.

Read more »

Security Analysis via Learning and Model-Checking Attack-Defense Trees

Attack Defence Trees

We work on the analysis and generation of Attack-Defence Trees.

Read more »

Algorithms for Stochastic Games

Value Iteration for Stochastic Games

We develop value iteration algorithms for stochastic games.

Read more »
Concurrent Stochastic Games

Concurrent Stochastic Games

We develop techniques for the verification of concurrent stochastic games which extend turn-based stochastic games by allowing players to select actions simultaneously in each state, reflecting more realistic scenarios of interactive agents acting concurrently.

Read more »

Analysis of Probabilistic Systems

Reinforcement Learning of Known and Unknown MDPs

Read more »

Multi-Objective Optimization in Sequential Decision Making

Read more »

Chemical Reaction Networks

Read more »

Tools

QuADTool

QuADTool

We provide a highly user-friendly tool for Synthesis of Cyber-security models based on the attack-tree concept. It also features interfaces to a variety of other tools and model-checkers, as well as built-in analysis for uncertain values. Additionally, the CLI can be used to learn attack-trees from logfiles or other traces.

Read more »
SeQuaiA

SeQuaiA

This tool implements the semi-quantitative analysis of Chemical Reaction Networks.

Read more »
SemML

SemML

In this project we develop learning-based exploration heuristics for LTL Synthesis that exploit the semantic labelling of the underlying Automaton/Game.

Read more »

RABINIZER

Rabinizer is a tool for creating deterministic automata for LTL.

Read more »
Owl

Owl

Owl is designed to help researches in formal methods to work with ω-words, ω-automata and LTL.

Read more »
MONITIZER

MONITIZER

We create a tool (Monitizer) that optimizes monitors on a NN for a specific task.

Read more »
dtControl

dtControl

Represent controllers as decision trees. Improve memory footprint, boost explainability while preserving guarantees.

Read more »
Automata Tutor

Automata Tutor is an online teaching tool that aids instructors and students in large courses on automata and formal languages with many different exercise types.

Read more »

Team

Alumni