Abstract
We consider variants of propositional dynamic logic (PDL) augmented with the converse construct. Intuitively, the converse α− of a program α is a programs whose semantics is to run α backwards. While PDL consists of assertions about weakest preconditions, the converse construct enable us to make assertions about strongest postconditions. We investigate the interaction of converse with two constructs that deal with infinite computations: loop and repeat. We show that converse - loop - PDL is decidable in exponential time, and converse - repeat - PDL is decidable in nondeterministic exponential time.
Cite
CITATION STYLE
Vardi, M. Y. (1985). The taming of converse: Reasoning about two-way computations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 193 LNCS, pp. 413–424). Springer Verlag. https://doi.org/10.1007/3-540-15648-8_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
