Sciweavers

Share
ENTCS
2000

Incompleteness of Behavioral Logics

8 years 10 months ago
Incompleteness of Behavioral Logics
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 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 coa...
Samuel R. Buss, Grigore Rosu
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2000
Where ENTCS
Authors Samuel R. Buss, Grigore Rosu
Comments (0)
books