6 papers
Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation
Mikkel Bjørn, Mikkel Bjørn, Daniel H. Hansen +3
We study safety verification for linear time-invariant systems with bounded inputs in continuous time. The standard approach reduces to a reachability analysis in two steps: first…
Time for Timed Monitorability
Thomas M. Grosen, Sean Kauffman, Kim G. Larsen +1
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online…
The Complexity of Data-Free Nfer
Sean Kauffman, Kim Guldstrand Larsen, Martin Zimmermann
Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evalua…
Exploiting Assumptions for Effective Monitoring of Real-Time Properties under Partial Observability
Alessandro Cimatti, Thomas M. Grosen, Kim G. Larsen +2
Runtime verification of temporal properties is essential for ensuring the correctness and reliability of real-time systems, particularly in cyber-physical systems. A significant ch…
Efficient Runtime Verification of Real-Time Systems under Parametric Communication Delays
Martin Fränzle, Thomas M. Grosen, Kim G. Larsen +1
Timed Büchi automata provide a very expressive formalism for expressing requirements of real-time systems. Online monitoring and active testing of embedded real-time systems can t…
You May Delay, but Time Will Not: Timed Games Under Delayed Control
Kim G. Larsen, Martin Zimmermann
Inspired by Martin Fränzle's persistent and influential work on capturing and handling delay inherent to cyber-physical systems in the formal verification of such systems, we stud…