Resource separation in dynamic logic of propositional assignments

DOI10.1007/978-3-030-38808-9_10zbMATH Open1496.03124arXiv2104.14884OpenAlexW2999871955MaRDI QIDQ5896086FDOQ5896086

Authors: Joseph Boudou, Andreas Herzig, Nicolas Troquard 

Publication date: 8 July 2020

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

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.

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

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

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)

Cited In (7)

• Title not available (Why is that?)
• A modal separation logic for resource dynamics
• Exponential-size model property for PDL with separating parallel composition
• Resource separation in dynamic logic of propositional assignments
• A simple separation logic
• Variables as resource in separation logic
• Classical BI

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)