On verifying timed hyperproperties

HO, Hsi-Ming, ZHOU, Ruoyu and JONES, Timothy M (2019). On verifying timed hyperproperties. In: GAMPER, Johann, PINCHINAT, Sophie and SCIAVICCO, Guido, (eds.) 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (147). DROPS - Dagstuhl Research Online Publication Server.

Preview

PDF LIPIcs-TIME-2019-20.pdf - Published Version Creative Commons Attribution. Download (694kB) | Preview

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: synchronous and asynchronous. While the satisfiability problem can be decided similarly as for HyperLTL regardless of the choice of semantics, we show that the model-checking problem for HyperMTL, 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.

Item Type:	Book Section
Additional Information:	ISSN 1868-8969
Uncontrolled Keywords:	cs.LO; cs.LO
Identification Number:	https://doi.org/10.4230/LIPIcs.TIME.2019.20
SWORD Depositor:	Symplectic Elements
Depositing User:	Symplectic Elements
Date Deposited:	19 Dec 2019 15:56
Last Modified:	18 Mar 2021 03:01
URI:	https://shura.shu.ac.uk/id/eprint/25565

Actions (login required)

View Item

Downloads

Publication Metrics