Abstract
The run-time verification logic Eagle is equipped with two forms of binary cut operator, sequential composition (;) and concatenation (·). Essentially, a concatenation formula F 1 ·F 2 holds on a trace if that trace can be cut into two non-overlapping traces such that F 1 holds on the first and F 2 on the second. Sequential composition differs from concatenation in that the two traces must overlap by one state. Both cut operators are non-deterministic in the sense that the cutting point is not uniquely defined. In this paper we establish that sequential composition and concatenation are equally expressive. We then extend Eagle with deterministic variants of sequential composition and concatenation. These variants impose a restriction on either the left or right operand so that the cut point defines either the shortest or longest possible satisfiable cut trace. Whilst it is possible to define such deterministic operators recursively within Eagle, such definitions based on the non-deterministic cut operators impose a complexity penalty. By augmenting Eagle’s evaluation calculus for the deterministic variants, we establish that the asymptotic time and space complexity of on-line monitoring for the variants with deterministic restrictions applied to the left operand is no worse than the asymptotic time and space complexity of the sub-formulæ.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in EAGLE. In: 18th International Parallel and Distributed Processing Symposium, IPDPS 2004. IEEE Computer Society, Los Alamitos (2004)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)
Chandra, A., Halpern, J., Meyer, A., Parikh, R.: Equations between regular terms and an application to process logic. In: STOC 1981: Proceedings of the 13th Annual ACM Symposium on Theory of Computing, pp. 384–390. ACM Press, New York (1981)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Minsky, M.L.: Recursive unsolvability of Post’s problem of “tag” and other topics in theory of Turing machines. The Annals of Mathematics 74(3), 437–455 (1961)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1–2), 72–99 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baran, J., Barringer, H. (2008). Forays into Sequential Composition and Concatenation in Eagle . In: Leucker, M. (eds) Runtime Verification. RV 2008. Lecture Notes in Computer Science, vol 5289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89247-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-89247-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89246-5
Online ISBN: 978-3-540-89247-2
eBook Packages: Computer ScienceComputer Science (R0)