3 citations · 3 across the 3 of their papers we have counts for
6 papers
Model Checking HyperRecHML is Decidable
Elli Anastasiadi, Kim Guldstrand Larsen, Martin Zimmermann
Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows…
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…
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 study…
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…
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…
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 th…