Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-32943-2_2 | ICTAC |
Keywords | Field | DocType |
hierarchical b,detailed construction,past operator,principal ltl operator,ltl formula,compositional hierarchical monitoring automaton,chi automaton,compositional construction | Discrete mathematics,Computer science,Automaton,Correctness,Phrase,Theoretical computer science,Mathematical proof,Operator (computer programming),Büchi automaton | Conference |
Citations | PageRank | References |
0 | 0.34 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Deepak D'souza | 1 | 239 | 17.90 |
| M. Raj Mohan | 2 | 4 | 1.49 |