Repository logo
 

On verifying timed hyperproperties

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Ho, HM 
Zhou, R 
Jones, TM 

Abstract

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: asynchronous and synchronous. While the satisfiability problem can be decided similarly to HyperLTL regardless of the choice of semantics, we show that the model-checking problem, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.

Description

Keywords

cs.LO, cs.LO

Journal Title

Leibniz International Proceedings in Informatics, LIPIcs

Conference Name

Journal ISSN

1868-8969

Volume Title

147

Publisher

Sponsorship
Engineering and Physical Sciences Research Council (EP/K026399/1)
Engineering and Physical Sciences Research Council (EP/P020011/1)
EP/K026399/1 and EP/P020011/1