I have a problem, that I can formulate as model-finding in Linear Temporal Logic (via Büchi automata). I also have the additional knowledge, that there is always satisfied a Markov-like property, specifically, for any pair of formulas $\phi, \psi$ whenever $\vdash F (\phi \implies X \psi)$ then also $\vdash G (\phi \implies X \psi)$. I think that this property could be somehow exploited to simplify or speed up the model finding process. Any ideas?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.