__Journal article:__

** Samuel R. Buss and Grigore Rosu.
"Incompleteness of Behavioral Logics,"
**

** Abstract: **Incompleteness results for behavioral
logics are investigated. We show that there is a basic finite behavioral
specification for which the behavioral satisfaction problem is not recursively enumerable,
which means that there are no automatic methods for proving all true statements; in
particular, behavioral logics do not admit complete deduction systems. This holds
for all of the behavioral logics of which we are aware. We also prove that the
behavioral satisfaction problem is not co-recursively enumerable, which means that there
is no automatic way to refute false statements in behavioral logics. In fact we show
stronger results, that all behavioral logics are $\Pi^0_2$-hard, and that, for some data
algebras, the complexity of behavioral satisfaction is not even arithmetic; matching upper
bounds are established for some behavioral logics. In addition, we show for the
fixed-data case that if operations may have more than one hidden argument, then final
models need not exist, so that the coalgebraic flavor of behavioral logic is lost.

** Download postscript or PDF.**