Author name cluster

Ruoyu Zhou

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

I&C Journal 2021 Journal Article

Timed hyperproperties

Hsi-Ming Ho
Ruoyu Zhou
Timothy M. Jones

We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMITL, a timed extension of HyperLTL. While the satisfiability problem can be solved similarly as for HyperLTL, we show that the model-checking problem for HyperMITL, 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 HyperMITL with quantifier alternations is possible under certain semantic restrictions. As an intermediate tool, we give an ‘asynchronous’ interpretation of Wilke's monadic logic of relative distance ( L d ↔ ) and show that it characterises timed languages recognised by timed automata with silent transitions.

Details DOI

TIME Conference 2019 Conference Paper

On Verifying Timed Hyperproperties

Hsi-Ming Ho
Ruoyu Zhou
Timothy M. Jones 0001

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.

Details