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.

[img]
Preview
PDF
LIPIcs-TIME-2019-20.pdf - Published Version
Creative Commons Attribution.

Download (694kB) | Preview
Official URL: https://drops.dagstuhl.de/opus/frontdoor.php?sourc...
Link to published version:: https://doi.org/10.4230/LIPIcs.TIME.2019.20
Related URLs:

    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: 19 Dec 2019 16:00
    URI: http://shura.shu.ac.uk/id/eprint/25565

    Actions (login required)

    View Item View Item

    Downloads

    Downloads per month over past year

    View more statistics