Skip to main content
Run-Time Checking of Dynamic Properties
Departmental Papers (CIS)
  • Oleg Sokolsky, University of Pennsylvania
  • Usa Sammapun, University of Pennsylvania
  • Insup Lee, University of Pennsylvania
  • Jesung Kim, University of Pennsylvania
Date of this Version
Document Type
Conference Paper
Postrpint version. Proceedings of the Fifth Workshop on Runtime Verification (RV'05)
Note: This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science
Publisher URL:

We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of quantifiers to bind free variables in a formula. One kind contains the usual first-order quantifiers that provide for replication of properties for dynamically created and destroyed objects in the system. The other kind, called attribute quantifiers, is used to check dynamically changing values within the same object. We show that expressions in this language can be eficiently checked over an execution trace of a system.

Citation Information
Oleg Sokolsky, Usa Sammapun, Insup Lee and Jesung Kim. "Run-Time Checking of Dynamic Properties" (2005)
Available at: