Skip to main content
Share Your Experience: Take the 2024 Developer Survey

New answers tagged

3 votes
Accepted

Can CTL* express every model's behaviour

First of all, for every transition system M, there indeed exists a CTL* formula Φ such that M ⊨ Φ holds, namely the CTL* formula "true". What you may have wanted to express is the question ...
DCTLib's user avatar
  • 2,787
1 vote
Accepted

Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?

Yes your intuition is correct. The fact is that the 2 relations can be disjoint when considering just one-sided simulation relations but for bisimulation we need 1 relation with symmetry which is ...
revision's user avatar

Top 50 recent answers are included