Information Technology Reference
In-Depth Information
15. D'Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B.,
Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: Runtime monitoring of synchronous
systems. In: Proceedings of the 12th International Symposium on Temporal Rep-
resentation and Reasoning (TIME 2005), pp. 166-174 (2005)
16. Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime
executions. Form. Method. Syst. Des. 27(3), 253-274 (2005)
17. Garcia-Molina, H., Ullman, J.D., Widom, J.: Database systems: The complete
topic. Pearson Education (2009)
18. Halle, S., Villemaire, R.: Runtime enforcement of web service message contracts
with data. IEEE Trans. Serv. Comput. 5(2), 192-206 (2012)
19. Hella, L., Libkin, L., Nurmonen, J., Wong, L.: Logics with aggregate operators. J.
ACM 48(4), 880-907 (2001)
20. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-
Time Syst. 2(4), 255-299 (1990)
21. Owe, O.: Partial logics reconsidered: A conservative approach. Form. Asp. Com-
put. 5(3), 208-223 (1993)
22. PostgreSQL Global Development Group. PostgreSQL, Version 9.1.4 (2012),
23. Sistla, A.P., Wolfson, O.: Temporal conditions and integrity constraints in active
database systems. In: Proceedings of the 1995 ACM SIGMOD International Con-
ference on Management of Data, pp. 269-280 (1995)
A Appendix
The pseudo-code of the procedures
init
and
eval
is given in Figure 4. Our pseudo-
code is written in a functional-programming style with pattern matching. The
symbol
denotes the empty sequence, ++ sequence concatenation, and
h
::
L
the sequence with head
h
and tail
L
.
We describe the
eval
procedure in the following in more detail. The cases corre-
spond to the rules defining the set of monitorable formulas. The pseudo-code for
the cases corresponding to non-temporal connectives follows closely the equali-
ties given in Section 3.3 and also given in the appendix of the full version of the
paper. The predicates
kind rig
and
kind rig
' check whether the input formula
ϕ
is indeed of the intended kind. The
get info
procedures return the parameters
used by the corresponding relational algebra operators. For instance,
get info rig
returns the singleton set consisting of the constraint corresponding to the restric-
tions
p
(
t
)or
∗
p
(
t
). Similarly,
get info rig
' returns the effective index correspond-
ing to the only variable that appears only in the right conjunct of
ϕ
. The proce-
dure
reval
(
p,k,a
) returns the set
¬
p
D
}
{
d
∈
D
|
(
a
1
,...,a
k−
1
,d,a
k
,...,a
n−
1
)
∈
,
1
,where
n
is the arity of the rigid predicate symbol
p
.
The case for the formulas of the form
n
−
for any
a
∈
D
I
ψ
is straightforward. We recursively
evaluate the subformula
ψ
, we update the state, and we return the relation
resulting from the evaluation of
ψ
at the previous time point, provided that the
temporal constraint is satisfied. Otherwise we return the empty relation.
The case for the formulas
ϕ
of the form
ψ
S
I
ψ
or
ψ
S
I
ψ
is more involved.
It is mainly handled by the sub-procedure
eval since
, given in Figure 5. The
notation
λx.f
(
x
) denotes a function
f
. For the clarity of the presentation, we
¬
