Generating optimal linear temporal logic monitors by coinduction

Koushik Sen, Grigore Rosu, Gul A Agha

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)260-275
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - 2003

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Generating optimal linear temporal logic monitors by coinduction'. Together they form a unique fingerprint.

Cite this