Published in Volume XXII, Issue 2, 2012, pages 327-365, doi: 10.7561/SACS.2012.2.327

Authors: G. Roșu


This paper addresses the problem of runtime verification from a foundational
perspective, answering questions like
“Is there a consensus among the various definitions of a safety property?”
(Answer: Yes),
“How many safety properties exist?”
(Answer: As many as real numbers),
“How difficult is the problem of monitoring a safety property?”
(Answer: Arbitrarily complex),
“Is there any formalism that can express all safety properties?”
(Answer: No),
Various definitions of safety properties as sets of execution traces
have been proposed in the literature, some over finite traces,
others over infinite traces, yet others over both finite and infinite
By employing cardinality arguments and a novel notion of
{em persistence}, this paper first establishes the existence of bijective
correspondences between the various notions of safety property.
It then shows that safety properties can be characterized as
“always past” properties.
Finally, it proposes a general notion of {em monitor}, which allows to
show that safety properties correspond precisely to the monitorable
properties, and then to establish that monitoring a safety property
is arbitrarily hard.

Full Text (PDF)


[1] Martín Abadi and Leslie Lamport. The existence of re nement mappings.
In Proceedings of the Third Annual Symposium on Logic in Computer
Science (LICS ’88), pages 165-175. IEEE Computer Society, 1988. .

[2] Martín Abadi and Leslie Lamport. The existence of re nement mappings.
Theoretical Computer Science, 82(2):253-284, 1991. .

[3] Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie Hendren,
Sascha Kuzins, Ondrej Lhotak, Oege de Moor, Damien Sereni, Ganesh
Sittampalam, and Julian Tibble. Adding trace matching with free
variables to AspectJ. In Richard P. Gabriel, editor, ACM Conference
on Object-Oriented Programming, Systems and Languages (OOPSLA),
pages 345-364. ACM Press, 2005. .

[4] Bowen Alpern and Fred B. Schneider. De ning liveness. Information
Processing Letters, 21(4):181-185, 1985. .

[5] Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness
in languages for distributed programming. In Fourteenth Annual ACM
Symposium on Principles of Programming Languages (POPL’ 87), pages
189-198, 1987. .

[6] Feng Chen, Marcelo D’Amorim, and Grigore Rosu. Checking and
correcting behaviors of Java programs at runtime with Java-MOP. In
RV’05, volume 144(4) of Electronic Notes in Theoretical Computer
Science. .

[7] Kevin W. Hamlen, J. Gregory Morrisett, and Fred B. Schneider. Computability
classes for enforcement mechanisms. ACM Trans. Program.
Lang. Syst., 28(1):175-205, 2006. .

[8] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory,
Languages, and Computation. Addison-Wesley, 1979.

[9] Leslie Lamport. Proving the correctness of multiprocess programs.
IEEE Transactions on Software Engineering., 3(2):125-143, 1977. .

[10] Leslie Lamport. Logical foundation. In M. W. Alford, J. P. Ansart,
G. Hommel, L. Lamport, B. Liskov, G. P. Mullery, F. B. Schneider,
M. Paul, and H. J. Siegert, editors, Distributed systems: Methods and
tools for speci cation. An advanced course, volume 190 of LNCS, pages
119-130. Springer-Verlag, 1985.

[11] Zohar Manna and Amir Pnueli. Temporal veri cation of reactive systems:
safety. Springer-Verlag New York, Inc., New York, NY, USA, 1995.

[12] G. Rosu and M. Viswanathan. Testing extended regular language
membership incrementally by rewriting. In RTA’03, volume 2706 of
Lecture Notes in Computer Science, pages 499-514. Springer, 2003. .

[13] Fred B. Schneider. On Concurrent Programming. Springer, 1997.

[14] Fred B. Schneider. Enforceable security policies. ACM Transactions
on Information and System Security, 3(1):30-50, 2000. .


  title={On Safety Properties and Their Monitoring},
  author={G. Ro{c s}u},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}