Visible to the public Verifying Hyperproperties with Temporal Logic of Actions (TLA)


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.


Fred B. Schneider is the Samuel B. Eckert Professor of Computer Science at Cornell University. Schneider's research has focused on various aspects of trustworthy systems --- systems that will perform as expected, despite failures and attacks. He is founding chair of the National Academy Forum on Cyber Resillience, where he remains active as Chair Emeritus.


Creative Commons 2.5
Switch to experimental viewer