Impartiality and Anticipation for Monitoring of Visibly Context-free Properties

Normann Decker, Martin Leucker, Daniel Thoma


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.

Original languageEnglish
Title of host publicationRuntime Verification
Number of pages18
VolumeLNCS 8174
Place of PublicationBerlin
PublisherSpringer Verlag
Publication date18.11.2013
ISBN (Print)978-3-642-40786-4
ISBN (Electronic)978-3-642-40787-1
Publication statusPublished - 18.11.2013
Event4th International Conference on Runtime Verification
- Rennes, France
Duration: 24.09.201327.09.2013
Conference number: 100802


Dive into the research topics of 'Impartiality and Anticipation for Monitoring of Visibly Context-free Properties'. Together they form a unique fingerprint.

Cite this