Abstract
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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
D’Souza, D., & Matteplackel, R. M. (2012). A compositional hierarchical monitoring automaton construction for LTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7521 LNCS, pp. 16–29). https://doi.org/10.1007/978-3-642-32943-2_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
