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 ...
- 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 ...
- 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 $\...
- 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. "...
- 366
Only top scored, non community-wiki answers of a minimum length are eligible