Verifying Hyperproperties with Temporal Logic of Actions (TLA)

ABSTRACT

Hyperproperties generalize ordinary properties by expressing relations among multiple executions of a system. Self- composition has been used to reduce verifying that a system satisfies certain classes of hyperproperties to verifying that a derived system satisfies an ordinary property. By describing systems and their properties in the temporal logic TLA, we use self-composition to handle a larger class of hyperproperties that includes those we have seen that express security conditions. TLA tools are used to verify that high-level designs of industrial systems satisfy properties. Now, they can also verify that those systems satisfy these hyperproperties.