Information Technology Reference
In-Depth Information
Ta b l e 1 .
Overview of complexity results
Satisfiability
Word problem
Model checking
Prefix problem
LTL
PSpace-complete
<
Bilinear-time
PSpace-complete
PSpace-complete
LTL
FO
Undecidable
PSpace-complete
ExpSpace-membership,
PSpace-hard
Undecidable
them around until the right hand side of the
U
-operator holds. If the right hand side of
the
U
-operator never holds (or not for a very long time), the space consumption of the
monitor is
bound
to grow. Hence, unlike in standard LTL, trace-length dependence is
not merely a property of the monitor, but also of the specification.
We conjecture that trace-length dependence is generally undecidable. However, if
the formula is
not
trace-length dependent, then our monitor is trace-length indepen-
dent, as desired. Given a
ϕ
LTL
FO
of which we know that it is trace-length in-
dependent in principle, our monitor's size at runtime at any given time is bounded
by
O
(
∈
2
|ϕ|
),where
σ
is the current input to the monitor: Throughout the
depth(
ϕ
) levels of the monitor, there are a total of
O
(
depth(
ϕ
)
|
σ
|
·
depth(
ϕ
)
) submonitors, which
are of size
O
(2
|ϕ|
), respectively. In contrast, the size of a progression-based monitor,
even for obviously trace-length independent formulae, such as
ϕ
2
in Fig. 2 is, in the
worst case, proportional to the trace length.
In Table 1 we have summarised the main results of
|
σ
|
4, highlighting again the dif-
ferences of LTL compared to LTL
FO
. Note that as far as trace-length dependence goes,
for LTL it is always possible to devise a trace-length independent monitor, irrespective
of the specification at hand (cf. [8]).
§
2-
§
Acknowledgements.
Our thanks go to Patrik Haslum, Michael Norrish and Peter
Baumgartner for helpful comments on earlier drafts of this paper.
References
1. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhotak, O., de Moor,
O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to
AspectJ. In: Proc. 20th ACM SIGPLAN Conf. on Object-Oriented Programming, Systems,
Languages, and Applications (OOPSLA), pp. 345-364. ACM (2005)
2. Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Annals of Mathematics
and Artificial Intelligence 22, 5-27 (1998)
3. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
4. Basin, D., Klaedtke, F., Muller, S.: Policy monitoring in first-order temporal logic. In:
Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1-18. Springer,
Heidelberg (2010)
5. Bauer, A., Gore, R., Tiu, A.: A first-order policy language for history-based transaction mon-
itoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 96-111.
Springer, Heidelberg (2009)
6. Bauer, A., K uster, J.-C., Vegliach, G.: Runtime verification meets Android security. In: Good-
loe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 174-180. Springer, Heidelberg
(2012)
