4
votes
1answer
132 views

How to implement simulation on two LTSs?

Does any one know how to implement the simulation relation on two labelled transition systems (LTS)? I know how to do it for branching bi-simulation. The signature refinement theorem is used for ...
3
votes
1answer
75 views

Time to construct a GNBA for LTL formula

I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula: Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
20
votes
2answers
443 views

Equivalence of Büchi automata and linear $\mu$-calculus

It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...