Impartiality and Anticipation for Monitoring of Visibly Context-free Properties
| Title | Impartiality and Anticipation for Monitoring of Visibly Context-free Properties |
| Publication Type | Conference Paper |
| Year of Publication | 2013 |
| Authors | Decker, N, Leucker, M, Thoma, D |
| Conference Name | Runtime Verification 2013 |
| Series | Lecture Notes in Computer Science |
| Volume | 8174, pp. 183--200 |
| Publisher | Springer, Heidelberg |
| Abstract | We study monitoring of visibly context-free properties. These properties reflect the common concept of nesting which arises naturally in software systems. They can be expressed e.g. in the temporal logic CaRet which extends LTL by means of matching calls and returns. The future fragment of CaRet enables us to give a direct unfolding-based automaton construction, similar to LTL. We provide a four-valued, impartial semantics on finite words which is particularly suitable for monitoring. This allows us to synthesize monitors in terms of deterministic push-down Mealy machines. To go beyond impartiality, we develop a construction for anticipatory monitors from visibly push-down ω-automata by utilizing a decision procedure for emptiness. |
Bibtex:
@inproceedings {977,
title = {Impartiality and Anticipation for Monitoring of Visibly Context-free Properties},
booktitle = {Runtime Verification 2013},
series = {Lecture Notes in Computer Science},
volume = {8174, pp. 183--200},
year = {2013},
publisher = {Springer, Heidelberg},
organization = {Springer, Heidelberg},
abstract = {<p>We study monitoring of visibly context-free properties. These properties reflect the common concept of nesting which arises naturally in software systems. They can be expressed e.g. in the temporal logic CaRet which extends LTL by means of matching calls and returns. The future fragment of CaRet enables us to give a direct unfolding-based automaton construction, similar to LTL. We provide a four-valued, impartial semantics on finite words which is particularly suitable for monitoring.\ This allows us to synthesize monitors in terms of deterministic push-down Mealy machines. To go beyond impartiality, we develop a construction for anticipatory monitors from visibly push-down ω-automata by utilizing a decision procedure for emptiness.</p>
},
author = {Normann Decker and Martin Leucker and Daniel Thoma}
}PDF:
