Monitor Circuits for LTL with Bounded and Unbounded Future

Synthesizing monitor circuits for LTL formulas is expensive, because the number of flip-flops in the circuit is exponential in the length of the formula. As a result, the IEEE standard PSL recommends to restrict monitoring to the simple subset and use the full logic only for static verification. We present a novel construction for the synthesis of monitor circuits from specifications in LTL. In our construction, only subformulas with unbounded-future operators contribute to the exponential blowup. We split the specification into a bounded and an unbounded part, apply specialized constructions for each part, and then compose the results into a monitor for the original specification. Since the unbounded part in practical specifications is often very small, we argue that, with the new construction, it is no longer necessary to restrict runtime verification to the simple subset.

• Type: Conference
• Year: 2009
• Where: RV
• Authors: Bernd Finkbeiner, Lars Kuhtz
• Keywords: Hardware, Ieee Standard Psl, Monitor Circuits, RV 2009, Simple Subset