1
$\begingroup$

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?

$\endgroup$

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.