Many important timed requirements of computing systems cannot be described by the behavior of individual execution traces. Examples include countermeasures to deal with side-channel timing attacks and service-level agreements, which are examples of timed hyperproperties. In this paper, we propose the temporal logic HyperMTL, that extends MTL by allowing explicit and simultaneous quantification over multiple timed traces in the point-wise semantics. We demonstrate the application of HyperMTL in expressing important properties in information-flow security and cyber-physical systems. We also introduce a model checking algorithm for a nontrivial fragment of HyperMTL by reducing the problem to model checking untimed hyperproperties.
CITATION STYLE
Bonakdarpour, B., Prabhakar, P., & Sánchez, C. (2020). Model Checking Timed Hyperproperties in Discrete-Time Systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12229 LNCS, pp. 311–328). Springer. https://doi.org/10.1007/978-3-030-55754-6_18
Mendeley helps you to discover research relevant for your work.