# Observational Determinism using HyperPCTL

I've found no material on HyperPCTL, so if you know please help me. This is the definition of Observational Determinism expressed using HyperPCTL and i have some questions.

$$\forall \sigma \, \forall \sigma ^{'} \, (ev_{L,IN}(\sigma)= ev_{L,IN}(\sigma^{'}))\rightarrow G(ev_{L,OUT}(\sigma)= ev_{L,OUT}(\sigma^{'}))$$

$$ev_{L,IN}$$ is for input events of low type

1) Does $$\sigma$$ (and also $$\sigma ^{'}$$) represent the initial state or the whole trace?

2) Is $$(ev_{L,IN}(\sigma)= ev_{L,IN}(\sigma^{'}))$$ a state formula that have to be checked only in the initial states ?

3) Why $$G$$ is present only on the right side of the logical implication?

4) In detail, how should a formula of this type be read?

• Can you give a reference of where you have found this formula? Does it include a formal semantics of HyperPCTL? As far as I know HyperPCTL is not an established logic as of yet, and there may be different definitions around. – SimonJ Aug 27 '19 at 6:38