Skip to main content

Model Checking Timed Hyperproperties in Discrete-time Systems

Publication Type
Year of Publication
Conference/Journal Name
The 12th NASA Formal Methods Conference (NFM)
Page Numbers
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.