On the power of bounded concurrency. III. Reasoning about programs

For pt.II by T. Hirst and D. Harel see Proc. 15th Coll. Trees in Algebra and programming. Lec. Notes in Comp. Sci., Springer (1990). The difficulty of reasoning about programs is addressed. Specifically, the question of whether the additional succinctness that bounded concurrency provides influences the complexity of reasoning about regular computation sequences on the propositional level is considered. The results concern dynamic, temporal, and process logics, and supply a strongly affirmative answer. In particular, triple-exponential time upper and lower bounds on deciding the validity of propositional dynamic logic with alternating automata enriched with bounded cooperative concurrency, and quadruple-exponential time bounds for deciding validity of branching-time and process logics with such automata are proven. In addition to constituting further evidence for the inherent exponential nature of bounded concurrency, the results appear to provide the first examples of natural decision problems that are elementary and yet have lower bounds that are higher than double-exponential time