150 citations · 270 across the 9 of their papers we have counts for
9 papers
Safe and Near-Optimal Gate Control: A Case Study from the Danish West Coast
Martin Kristjansen, Kim Guldstrand Larsen, Marius Mikučionis +1
Ringkoebing Fjord is an inland water basin on the Danish west coast separated from the North Sea by a set of gates used to control the amount of water entering and leaving the fjor…
Data-Selective Online Battery Identification Using Extended Time Regular Expressions
Nicolai A. Weinreich, Marco Muñiz, Marius Mikučionis +2
In this paper, we propose a data-efficient online battery identification method which targets highly informative battery cell data segments based on the driving pattern of the vehi…
Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems
Asger Horn Brorholt, Andreas Holck Høeg-Petersen, Peter Gjøl Jensen +4
We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy -- or shield -- for Markov decision processes over continuous state spaces and complex hybrid dynamics.…
Scalable Computation of Inter-Core Bounds Through Exact Abstractions
Mohammed Aristide Foughali, Marius Mikučionis, Maryline Zhang
Real-time systems (RTSs) are at the heart of numerous safety-critical applications. An RTS typically consists of a set of real-time tasks (the software) that execute on a multicore…
Statistical Model Checking for Stochastic Hybrid Systems
Alexandre David, Dehui Du, Kim G. Larsen +4
This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how…
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
Peter Bulychev, Alexandre David, Kim Gulstrand Larsen +4
This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of netwo…
Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach
Peter Bulychev, Alexandre David, Kim G. Larsen +2
This paper studies the problem of computing Nash equilibrium in wireless networks modeled by Weighted Timed Automata. Such formalism comes together with a logic that can be used to…
Distributed Parametric and Statistical Model Checking
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen +2
Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if th…
Stochastic Semantics and Statistical Model Checking for Networks of Priced Timed Automata
Alexandre David, Kim G. Larsen, Axel Legay +4
This paper offers a natural stochastic semantics of Networks of Priced Timed Automata (NPTA) based on races between components. The semantics provides the basis for satisfaction of…