Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: On the power of bounded concurrency. III. Reasoning about programs (at LICS 1990)

Authors: Harel, D. Rosner, R. Vardi, M.


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


    author = 	 {Harel, D. and Rosner, R. and Vardi, M.},
    title = 	 {On the power of bounded concurrency. III. Reasoning about programs },
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {478--488},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}