We present an extension of past time LTL with call/return atoms, called ptCaRet, together with a monitor synthesis algorithm for it. ptCaRet includes abstract variants of past temporal operators, which can express properties over traces in which terminated function
or procedure executions are abstracted away into a call and a corresponding return. This way, ptCaRet can express safety properties about procedural programs which cannot be expressed using conventional linear temporal logics.
The generated monitors contain both a local state and a stack. The local state is encoded on as many bits as concrete temporal
operators the original formula has. The stack pushes/pops bit vectors of size the number of abstract temporal operators the
original formula has: push on begins, pop on ends of procedure executions. An optimized implementation is also discussed and
is available to download.
Supported by NSF CCF-0448501, NSF CNS-0509321, NASA ARMD safety Program and Air Force STTR phase I award (Topic Number AF07-T019,
Proposal Number F074-019-0162).