Resource separation in dynamic logic of propositional assignments
Logic in Computer Science
2021-05-04 v1
Abstract
We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatisation via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.
Cite
@article{arxiv.2104.14884,
title = {Resource separation in dynamic logic of propositional assignments},
author = {Joseph Boudou and Andreas Herzig and Nicolas Troquard},
journal= {arXiv preprint arXiv:2104.14884},
year = {2021}
}