Open Systems Laboratory at Illinois

Generating optimal linear temporal logic monitors by coinduction

By Koushik Sen, Grigore Rosu, and Gul Agha. In ASIAN, volume 2896 of Lecture Notes in Computer Science, 260–275. Springer, 2003.

Full Text:
Download PDF
Publisher Link:


A coinduction-based technique to generate an optimal monitor from a Linear Temporal Logic (LTL) formula is presented in this paper. Such a monitor receives a sequence of states (one at a time) from a running process, checks them against a requirements specification expressed as an LTL formula, and determines whether the formula has been violated or validated. It can also say whether the LTL formula is not monitorable any longer, i.e., that the formula can in the future neither be violated nor be validated. A Web interface for the presented algorithm adapted to extended regular expressions is available.


    author = "Sen, Koushik and Rosu, Grigore and Agha, Gul",
    editor = "Saraswat, Vijay A.",
    title = "Generating Optimal Linear Temporal Logic Monitors by
    booktitle = "ASIAN",
    crossref = "conf/asian/2003",
    ee = "",
    keywords = "formal methods, sensor networks, real-time systems",
    pages = "260-275",
    year = "2003",

    editor = "Saraswat, Vijay A.",
    title = "Advances in Computing Science - ASIAN 2003 Programming
             Languages and Distributed Computation, 8th Asian Computing Science
             Conference, Mumbai, India, December 10-14, 2003, Proceedings",
    isbn = "3-540-20632-9",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "2896",
    year = "2003",