Tableaux for constructive concurrent dynamic logic (Q2488268)

The paper presents a constructive version of concurrent dynamic logic (CCDL) that enables one to reason about statements that are true under partial information about the states of an underlying concurrent transition system. The authors define what it means for a dynamic logic formula to be forced to be true knowing only partial information about the results of assignments and tests, and provide a tableaux proof system as a generalization of the prefixed tableaux of Fitting. The proof system is shown to be sound and complete; the approach to completeness is based on the definition of consistency properties which guarantee the existence of models, then it is proved that systematic tableaux yield a consistency property.