Program schemata vs. automata for decidability of program logics

✍ Scribed by N.V. Shilov

• Book ID: 104326207
• Publisher: Elsevier Science
• Year: 1997
• Tongue: English
• Weight: 922 KB
• Volume: 175
• Category: Article
• ISSN: 0304-3975
• DOI: 10.1016/s0304-3975(96)00168-5

✦ Synopsis

A new technique for decidability of program logics is introduced. This technique is applied to the most expressive propositional program logic -mu-calculus. 0. Introduction We would like to present program scheme technique (PST) for decidability of program and polymodal propositional logics. This technique leads to one-exponential time upper bounds usually. Second-order propositional dynamic logic (SO-PDL) of program schemata is a variant of propositional dynamic logic (PDL) [6,8] with program schemata and secondorder quantifiers. Unfortunately it is undecidable, but the validity in Herbrand models (HM) is decidable with a one-exponential upper bound. This is based on a polynomial reduction of the validity problem in HM to the same problem but for sentences in the special form. The original one-exponential algorithm solves the last problem.

The syntax and semantics of SO-PDL together with some results on the expressive power and the undecidability of this logic are presented in Section 1 of this paper. The decidability of SO-PDL in HM is proved in Section 2.

We have to remark that some authors have introduced and investigated second-order variants of program logics -quantified propositional temporal logic (QPTL), which is propositional linear temporal logic equipped with quantification over propositions. In contrast to the results mentioned above, QPTL [ 151 is decidable with a non-elementary complexity and is as expressive as the monadic second-order logic SlS. The complete calculus for QPTL has been presented quite recently [9]. In fact, the completeness