Incompleteness of behavioral logics

Samuel Buss, Grigore Rosu

Research output: Contribution to journalConference article

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 II°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. Acknowledgments: We would like to thank Joseph Goguen for his comments on various versions of this work and for his continuous belief that the behavioral logics are incomplete. Special thanks to Ugo Montanari, Andrea Corradini, and Bogdan Warinschi for various technical discussions related to the work in this paper.

Original languageEnglish (US)
Pages (from-to)61-79
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume33
DOIs
StatePublished - Dec 1 2000
Externally publishedYes
EventCMCS'2000, Coalgebraic Methods in Computer Science - Berlin, Germany
Duration: Mar 25 2000Mar 26 2000

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Incompleteness of behavioral logics'. Together they form a unique fingerprint.

  • Cite this