Trace-length independent runtime monitoring of quantitative policies in LTL

Xiaoning Du, Yang Liu, Alwen Tiu

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

5 Citations (Scopus)


Linear temporal logic (LTL) has been widely used to specify runtime policies. Traditionally this use of LTL is to capture the qualitative aspects of the monitored systems, but recent developments in metric LTL and its extensions with aggregate operators allow some quantitative policies to be specified. Our interest in LTL-based policy languages is driven by applications in runtime Android malware detection, which requires the monitoring algorithm to be independent of the length of the system event traces so that its performance does not degrade as the traces grow. We propose a policy language based on a past-time variant of LTL, extended with an aggregate operator called the counting quantifier to specify a policy based on the number of times some sub-policies are satisfied in the past. We show that a broad class of policies, but not all policies, specified with our language can be monitored in a trace-length independent way without sacrificing completeness, and provide a concrete algorithm to do so. We implement and test our algorithm in an existing Android monitoring framework and show that our approach can effectively specify and enforce quantitative policies drawn from real-world Android malware studies.

Original languageEnglish
Title of host publicationFM 2015: Formal Methods
Subtitle of host publication20th International Symposium Oslo, Norway, June 24–26, 2015 Proceedings
EditorsNikolaj Bjorner, Frank de Boer
Place of PublicationCham Switzerland
Number of pages17
ISBN (Electronic)9783319192499
ISBN (Print)9783319192482
Publication statusPublished - 2015
Externally publishedYes
EventInternational Symposium on Formal Methods 2015 - Oslo, Norway
Duration: 24 Jun 201526 Jun 2015
Conference number: 20th (Proceedings) (Website)

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Symposium on Formal Methods 2015
Abbreviated titleFM 2015
Internet address


  • Policy Language
  • Linear Temporal Logic
  • Atomic Proposition
  • Kernel Module
  • Trace Length

Cite this