Substructural Propositional Dynamic Logic

Abstrakt

Propositional dynamic logic, PDL, is a well known modal logic with applications in formal verification of programs, dynamic epistemic logic and deontic logic. More generally, PDL can be seen as a logic for reasoning about structured actions modifying various types of objects; examples of such actions include programs modifying states of the computer, information state updates or actions of agents changing the world around them.