Eliminating ``converse from converse PDL

DOI10.1007/BF00173700MaRDI QIDQ1923830zbMATH OpenOpenAlexFDO

Authors Giuseppe De Giacomo

Publication date 5 May 1999

Published in Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00173700

zbMATH Keywords

converse propositional dynamic logicelimination of converse programsencoding of CPDL formulae into PDL

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70)

Recommendations

• Optimal and cut-free tableaux for propositional dynamic logic with converse
• scientific article; zbMATH DE number 3974280
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• PDL with intersection and converse: satisfiability and infinite-state model checking

Cited in

(5)

• The influence of the test operator on the expressive power of PDL-like logics
• scientific article; zbMATH DE number 3974280 (Why is no real title available?)
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Introspection as an action in relational models
• Optimal and cut-free tableaux for propositional dynamic logic with converse

This page was built for publication: Eliminating ``converse from converse PDL

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