5 votes

LTL property - safety or liveness?

Your first question is answered in this paper: https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf Given an LTL formula, translate it into a Büchi automaton, and remove states that have ...
user avatar
  • 1,175
3 votes
Accepted

Is every countable, finite-branching LTS bisimilar to a tree?

Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree. Q2: No, by a cardinality argument. For instance take infinite binary trees with $L=\{a,b\}$. Each tree has countable set of states ...
user avatar
  • 7,672
3 votes

Is modal $\mu$-calculus "equivalent" to bisimulation?

For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\...
user avatar
  • 7,672
1 vote
Accepted

LTL property - safety or liveness?

To answer your second question: there is one property that is both safety and liveness: True. With this exception, however, it is fair to say that a property is either safety or liveness or neither. "...
user avatar
  • 366

Only top scored, non community-wiki answers of a minimum length are eligible