research
∙
08/20/2023
Formal Verification of Safety Architectures for Automated Driving
Safety architectures play a crucial role in the safety assurance of auto...
share
research
∙
08/13/2023
Formal Verification of Intersection Safety for Automated Driving
We build on our recent work on formalization of responsibility-sensitive...
research
∙
07/17/2023
Compositional Probabilistic Model Checking with String Diagrams of MDPs
We present a compositional model checking algorithm for Markov decision ...
research
∙
07/16/2023
Compositional Solution of Mean Payoff Games by String Diagrams
Following our recent development of a compositional model checking algor...
research
∙
07/06/2023
Exploiting Adjoints in Property Directed Reachability Analysis
We formulate, in lattice-theoretic terms, two novel algorithms inspired ...
research
∙
05/28/2023
Online Causation Monitoring of Signal Temporal Logic
Online monitoring is an effective validation approach for hybrid systems...
research
∙
07/27/2022
Dynamic Shielding for Reinforcement Learning in Black-Box Environments
It is challenging to use reinforcement learning (RL) in cyber-physical s...
research
∙
07/06/2022
Goal-Aware RSS for Complex Scenarios via Program Logic
We introduce a goal-aware extension of responsibility-sensitive safety (...
research
∙
06/07/2022
Responsibility-Sensitive Safety: an Introduction with an Eye to Logical Foundations and Formalization
Responsibility-sensitive safety (RSS) is an approach to the safety of au...
research
∙
03/27/2022
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
We present LT-PDR, a lattice-theoretic generalization of Bradley's prope...
research
∙
03/24/2022
Exemplifying parametric timed specifications over signals with bounded behavior
Specifying properties can be challenging work. In this paper, we propose...
research
∙
12/28/2021
A Compositional Approach to Parity Games
In this paper, we introduce open parity games, which is a compositional ...
research
∙
08/17/2021
Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
Formal reasoning on the safety of controller systems interacting with pl...
research
∙
07/22/2021
Architecture-Guided Test Resource Allocation Via Logic
We introduce a new logic named Quantitative Confidence Logic (QCL) that ...
research
∙
05/21/2021
Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation
A modal logic that is strong enough to fully characterize the behavior o...
research
∙
05/11/2021
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
The coincidence between initial algebras (IAs) and final coalgebras (FCs...
research
∙
04/23/2021
Decision Tree Learning in CEGIS-Based Termination Analysis
We present a novel decision tree-based synthesis algorithm of ranking fu...
research
∙
02/15/2021
Model-bounded monitoring of hybrid systems
Monitoring of hybrid systems attracts both scientific and practical atte...
research
∙
01/05/2021
Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs
We introduce a novel sampling algorithm for Bayesian inference on impera...
research
∙
11/26/2020
Predictive PER: Balancing Priority and Diversity towards Stable Deep Reinforcement Learning
Prioritized experience replay (PER) samples important transitions, rathe...
research
∙
07/15/2020
Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Solving stochastic games with the reachability objective is a fundamenta...
research
∙
04/11/2020
Genetic Algorithm for the Weight Maximization Problem on Weighted Automata
The weight maximization problem (WMP) is the problem of finding the word...
research
∙
07/22/2019
Codensity Games for Bisimilarity
Bisimilarity as an equivalence notion of systems has been central to pro...
research
∙
04/05/2019
Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces
We present a method to extract a weighted finite automaton (WFA) from a ...
research
∙
03/01/2019
Relational Differential Dynamic Logic
In the field of quality assurance of hybrid systems (that combine contin...
research
∙
12/21/2018
Offline timed pattern matching under uncertainty
Given a log and a specification, timed pattern matching aims at exhibiti...
research
∙
11/16/2018
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Programs with randomization constructs is an active research topic, espe...
research
∙
10/22/2018
Quantitative Simulations by Matrices
We introduce notions of simulation between semiring-weighted automata as...
research
∙
10/22/2018
Quantitative Matrix Simulation
We introduce notions of simulation between semiring-weighted automata as...
research
∙
09/25/2018
Quantitative bisimulations using coreflections and open morphisms
We investigate a canonical way of defining bisimilarity of systems when ...
research
∙
05/28/2018
Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs
Computing reachability probabilities is a fundamental problem in the ana...
research
∙
05/28/2018
Ranking and Repulsing Supermartingales for Approximating Reachability
Computing reachability probabilities is a fundamental problem in the ana...
research
∙
03/19/2018
Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors
Categorical studies of recursive data structures and their associated re...
research
∙
09/08/2017
Causality-Aided Falsification
Falsification is drawing attention in quality assurance of heterogeneous...
research
∙
12/28/2014