Resource separation in dynamic logic of propositional assignments

DOI10.1007/978-3-030-38808-9_10MaRDI QIDQ5896086zbMATHOpenAlexFDO

Authors Joseph Boudou, Andreas Herzig, Nicolas Troquard

Publication date 8 July 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2104.14884

zbMATH Keywords

dynamic logicseparation logicparallel compositionpropositional assignments

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

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.

Recommendations

• Resource separation in dynamic logic of propositional assignments
• Dynamic logic of propositional assignments: a well-behaved variant of PDL
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• A modal separation logic for resource dynamics
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition

Cited in

(7)

• scientific article; zbMATH DE number 7317262 (Why is no real title available?)
• Classical BI
• A simple separation logic
• Variables as resource in separation logic
• Exponential-size model property for PDL with separating parallel composition
• A modal separation logic for resource dynamics
• Resource separation in dynamic logic of propositional assignments

This page was built for publication: Resource separation in dynamic logic of propositional assignments

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