This paper presents a prefixed tableaux calculus for Propositional Dynamic Logic with Converse based on a combination of different techniques such as prefixed tableaux for modal logics and model checkers for μ-calculus. We prove the correctness and completeness of the calculus and illustrate its features. We also discuss the transformation of the tableaux method (naively NEXPTIME) into an EXPTIME algorithm. © 2000 Academic Press.
Combining deduction and model checking into tableaux and algorithms for Converse-PDL.
Massacci, Fabio
2000-01-01
Abstract
This paper presents a prefixed tableaux calculus for Propositional Dynamic Logic with Converse based on a combination of different techniques such as prefixed tableaux for modal logics and model checkers for μ-calculus. We prove the correctness and completeness of the calculus and illustrate its features. We also discuss the transformation of the tableaux method (naively NEXPTIME) into an EXPTIME algorithm. © 2000 Academic Press.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
