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?

  • $\begingroup$ 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. $\endgroup$ – SimonJ Aug 27 '19 at 6:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.