Tableaux for constructive concurrent dynamic logic

DOI10.1016/J.APAL.2004.12.001MaRDI QIDQ2488268zbMATH OpenOpenAlexFDO

Publication date 25 August 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2004.12.001

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

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.

Recommendations

Cites work

Cited in

(22)

This page was built for publication: Tableaux for constructive concurrent dynamic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2488268)