# Lars Kuhtz

Lars KuhtzReactive Systems Group |

I defended my Ph.D. thesis in December 2010.

Currently, I am employed at Microsoft in Redmond, WA, USA.

## Research

During the time as a Ph.D. student, my research was about the complexity of runtime verification of temporal

logic properties. In runtime verification, we monitor the running system and

check on-the-fly whether the desired properties hold. Unlike in static

verification, where the verification algorithm is executed at design-time and

can therefore afford to spend significant time and resources, runtime

verification algorithms must run in synchrony with the monitored system and

usually even share the resources of the implementation platform.

Many questions concerning the complexity of runtime verification problems are

still open. For instance until recently the best known upper bound for the

evaluation of an LTL formula over a (finite) path was P while the best known

lower bound is NC^{1}. We were able to reduce

this gap by proving that path checking for LTL is efficiently

parallelizable.

Runtime verification is often applied within an online monitoring setting where

a possibly infinite input trace is read sequentially. A monitor for online

runtime verification of LTL properties requires in the worst case a number of

states that is doubly exponential in the size of the property. Fortunately, in

practice the worst case often can be avoided. Namely, we provide a construction

of monitor circuits for LTL with bounded and unbounded

future where bounded sub-formulas do not provide to

the exponential blow up.

Formerly, I have been studying random graphs. We developed an algorithm for

approximating the chromatic number of a random graph in expected polynomial

time. Moreover, I built a tool for deductive verification of reactive systems

and translation validation.

## Publications

[KF11b] | Lars Kuhtz and Bernd Finkbeiner. Weak Kripke Structures and LTL. CONCUR 2011, 2011. |

[KF11a] | Lars Kuhtz and Bernd Finkbeiner. Efficient Parallel Path Checking for Linear-Time Temporal Logic with Past and Bounds (Preprint). Accepted for publication in Logical Methods in Computer Science, 2011. |

[K10] | Lars Kuhtz. Model Checking Finite Paths and Trees. Dissertation, Universität des Saarlandes, 2010. |

[KF09] | Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. ICALP 09, 2009. Best Paper Award. |

[FK09] | Bernd Finkbeiner and Lars Kuhtz. Monitor Circuits for LTL with Bounded and Unbounded Future. RV 09, 2009. |

[CK06] | Amin Coja-Oghlan and Lars Kuhtz. An improved algorithm for approximating the chromatic number of Gn, p. Information Processing Letters 99 (2006), 234-238. |

[K04b] | Lars Kuhtz. Colouring G_{n,p} and Spectral Techniques. Diplomarbeit, 2004. |

[K04a] | Lars Kuhtz. TLDA und Petrinetze. Studienarbeit, Humboldt-Universität zu Berlin, 2004. |

## Awards

- Best paper of track B (Logic, Semantics, and Theory of Programming) of ICALP 2009.

## Tools

**dvt**: deductive verification of reactive systems and translation validation.**MoCS**: synthesis of monitor circuits from linear time temporal logic properties.**CirView**: a small tool for 3D visualization of LTL path checking via boolean circuits.

## Miscelaneous Slides

- Efficient Parallel Path Checking, short presentation at LICS 09.

## Recent Student Projects

[M05] | Ghulam Mujtaba. Monitoring Execution Traces using Metric Alternating Automata. Master Thesis |

[Eme05] | Pavel Emeliyanenko. Automatic Verification of Conditions for Absence of Interrupts. Bachelor Thesis |

[E07] | Franziska Ebert. Translation Validation for Optimizing Compilers. Master Thesis. 2007 |

## Teaching

## Projects

My research was supported by the German Research Foundation (DFG) as part of the

Transregional Collaborative Research Center Automatic Verification and

Analysis of Complex Systems (SFB/TR 14 AVACS).

The goal of the AVACS project is to raise the state of the art in automatic

verification and analysis techniques from its current level, where it is

applicable only to isolated facets (concurrency, time, continuous control,

stability, dependability, mobility, data structures, hardware constraints,

modularity, levels of refinement), to a level allowing the comprehensive

verification of computer systems.