On the computational complexity of satisfiability in propositional logics of programs

Bogdan S. Chlebus

Research output: Contribution to journalArticle

Abstract

The satisfiability problems of propositional algorithmic logic and propositional dynamic logic are shown to be complete in the classes of languages accepted in polynomial space by the deterministic and alternating Turing machines respectively. Explicit upper and lower bounds on the space complexity are calculated. Exponential lower bounds on the space complexity of the satisfiability problems of these logics extended by adding a certain program connective are proved.

Original languageEnglish (US)
Pages (from-to)179-212
Number of pages34
JournalTheoretical Computer Science
Volume21
Issue number2
DOIs
StatePublished - Nov 1982
Externally publishedYes

Fingerprint

Turing machines
Satisfiability Problem
Space Complexity
Propositional Logic
Computational complexity
Computational Complexity
Polynomials
Logic
Dynamic Logic
Turing Machine
Upper and Lower Bounds
Lower bound
Polynomial
Language
Class

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

On the computational complexity of satisfiability in propositional logics of programs. / Chlebus, Bogdan S.

In: Theoretical Computer Science, Vol. 21, No. 2, 11.1982, p. 179-212.

Research output: Contribution to journalArticle

@article{21b83df6d92441aab3da2a9c39fed996,
title = "On the computational complexity of satisfiability in propositional logics of programs",
abstract = "The satisfiability problems of propositional algorithmic logic and propositional dynamic logic are shown to be complete in the classes of languages accepted in polynomial space by the deterministic and alternating Turing machines respectively. Explicit upper and lower bounds on the space complexity are calculated. Exponential lower bounds on the space complexity of the satisfiability problems of these logics extended by adding a certain program connective are proved.",
author = "Chlebus, {Bogdan S.}",
year = "1982",
month = "11",
doi = "10.1016/0304-3975(89)90083-2",
language = "English (US)",
volume = "21",
pages = "179--212",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - On the computational complexity of satisfiability in propositional logics of programs

AU - Chlebus, Bogdan S.

PY - 1982/11

Y1 - 1982/11

N2 - The satisfiability problems of propositional algorithmic logic and propositional dynamic logic are shown to be complete in the classes of languages accepted in polynomial space by the deterministic and alternating Turing machines respectively. Explicit upper and lower bounds on the space complexity are calculated. Exponential lower bounds on the space complexity of the satisfiability problems of these logics extended by adding a certain program connective are proved.

AB - The satisfiability problems of propositional algorithmic logic and propositional dynamic logic are shown to be complete in the classes of languages accepted in polynomial space by the deterministic and alternating Turing machines respectively. Explicit upper and lower bounds on the space complexity are calculated. Exponential lower bounds on the space complexity of the satisfiability problems of these logics extended by adding a certain program connective are proved.

UR - http://www.scopus.com/inward/record.url?scp=49049143180&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=49049143180&partnerID=8YFLogxK

U2 - 10.1016/0304-3975(89)90083-2

DO - 10.1016/0304-3975(89)90083-2

M3 - Article

AN - SCOPUS:49049143180

VL - 21

SP - 179

EP - 212

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -