Affordable Access

Compositional hierarchical monitoring automaton construction for LTL

Springer Berlin Heidelberg
Publication Date
  • Computer Science & Automation (Formerly
  • School Of Automation)


In this paper we give a compositional (or inductive) construction of monitoring automata for LTL formulas. Our construction is similar in spirit to the compositional construction of Kesten and Pnueli [5]. We introduce the notion of hierarchical Büchi automata and phrase our constructions in the framework of these automata. We give detailed constructions for all the principal LTL operators including past operators, along with proofs of correctness of the constructions.

There are no comments yet on this publication. Be the first to share your thoughts.