Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

529 users

+1 vote
E(Fa ∧ Fb)

Ans- EFa & EFb        As E(a & b) = Ea & Eb

 Explanation - As EFa and EFb both are CTL ,

 thus its Pure CTL.
in # Study-Organisation (Master) by (130 points)

1 Answer

+1 vote

No, this is not correct. The E-quantifier can (in general) not be distributed over a conjunction. Look, E(Fa ∧ Fb) means that there must be a path where at some point of time "a" holds and at some other or the same point of time "b" holds. But it must be one and the same path. 

In contrast, (EFa) ∧ (EFb) means that there is a path p1 where at some point "a" holds, and there may be another path p2 where at some point of time "b" holds. You can quickly find a Kripke structure with two paths satisfying this, but not E(Fa ∧ Fb).

But you can convert E(Fa ∧ Fb) to CTL by enumerating the orderings of "a" and "b", i.e., 

EF (a ∧ EFb) ⋁ EF (b ∧ EFa)

which is an equivalent CTL formula.

by (166k points)

Related questions

0 votes
1 answer
0 votes
2 answers
0 votes
1 answer
asked Aug 19, 2020 in # Study-Organisation (Master) by skkumar (300 points)
0 votes
1 answer
asked Aug 17, 2020 in # Study-Organisation (Master) by RS (770 points)
0 votes
1 answer
asked Aug 14, 2020 in # Study-Organisation (Master) by RS (770 points)
Imprint | Privacy Policy
...