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 ...
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 ...
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 $\...
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. "...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
mu-calculus × 8lo.logic × 5
model-checking × 4
temporal-logic × 4
computability × 2
reference-request × 1
fl.formal-languages × 1
turing-machines × 1
physics × 1
linear-temporal-logic × 1
books × 1
church-turing-thesis × 1
modal-logic × 1
process-algebra × 1
formal-systems × 1