# Modelchecking on Automata, $\phi$ not SAT and $\phi \models$ False

Given a formula $\phi$

Is $\phi \models FALSE$ equivalent to $\phi$ not SAT?

Or does $\phi \models FALSE$ means that $\phi$ is never $TRUE$ and $\phi$ not SAT means, that there existst at least one counter example?
How can I express "not SAT" then?

-
In general $\phi$ is not SAT means $\phi$ is never true which means that $\phi$ does not have an example (as apposed to not having a counterexample). You need to provide some more background into your question if you want anything more than this. –  Levon Haykazyan Mar 15 '12 at 12:00
My formula is in TCTL and I have a solver that can not solve my formula. The result is "Can not SAT $\phi$", so it has at least one counter example. That is what I want to express with my formula. –  Tarion Mar 15 '12 at 12:40

$\phi \models \text{FALSE}$ means that every model of $\phi$ is also a model of FALSE. Since FALSE does not have models (at last in any sane form of logic), this implies that $\phi$ has no model, i.e., it is not satisfiable.
If you wish to express that $\phi$ has at least one counterexample, try $\text{TRUE} \not\models \phi$.