Affordable Access

Publisher Website

Automata-theoretic techniques for modal logics of programs

Authors
Journal
Journal of Computer and System Sciences
0022-0000
Publisher
Elsevier
Publication Date
Volume
32
Issue
2
Identifiers
DOI: 10.1016/0022-0000(86)90026-7
Disciplines
  • Computer Science
  • Logic

Abstract

Abstract We present a new technique for obtaining decision procedures for modal logics of programs. The technique centers around a new class of finite automata on infinite trees for which the emptiness problem can be solved in polynomial time. The decision procedures then consist of constructing an automaton A f for a given formula f such that A f accepts some tree if and only if f is satisfiable. We illustrate our technique by giving exponential decision procedures for several variants of deterministic propositional dynamic logic.

There are no comments yet on this publication. Be the first to share your thoughts.