Program schemata technique to solve propositional program logics revised

Abstract

Propositional program (dynamic, temporal and process) logics are basis for logical specification of program systems (including parallel, distributed and multiagent systems). Therefore development of efficient algorithms (decision procedures) for validation, provability and model checking of program logics is an important research topic for the theory of programming. The essence of a program schemata technique consists in the following. Formulas of a program logic to be translated into uninterpreted nondeterministic monadic flowcharts (so called Yanov schemata) so that the scheme is total (i.e. terminates) in all special interpretations if and only if the initial formula is a tautology (i.e. is identically true). Since this generalized halting problem is solvable (with an exponential complexity), it implies the decidability of initial program logic (and leads to a decidability upper bound). The first version of the technique was developed by Nikolay V. Shilov and Valery A. Nepomnjaschy in 1983–1987 for variants of Propositional Dynamic Logic (PDL). In 1997 the technique was expanded on the propositional μ-Calculus. In both cases a special algorithm was used to solve the generalized halting problem. A recent development of program schemata technique consists in revised decision procedure for the halting problem. A new decision procedure consists in model checking of a special fairness property (presented by some fixed μ-Calculus formula) in finite models presented by Yanov schemata flowcharts. Exponential lower bound for transformation of μ- Calculus formulas to equivalent guarded form is a consequence of the new version of the decision procedure.