5
$\begingroup$

Propositional dynamic logic (PDL) is an example of a (multi)modal logic with a structure on the set of modalities. In particular, the set of its modalities is indexed by "programs" and one can use program constructors such as composition, choice and iteration to make new programs out of old (of course, there is a set of basic programs to begin with). So if π and ρ are programs, so are π;ρ, π∪ρ and ρ*. The intuitive interpretations are, respectively, "run π, then run ρ", "nondeterministically run either π or ρ", and "run ρ finite number of times".

The formulas in this language are formed from propositional letters using boolean connectives. Also, if π is a program and φ a formula, then <π>φ is a formula with intuitive interpretation "there is a state of computation accessible by program π in which φ is satisfied". Modality <π> is read "diamond π".

Not to dwell any deeper right now, I refer you to a very well written article about PDL.

Now to get to my question. PDL was created in a line of formal systems that were ment to be used to "talk about" programs, prove program correctness etc. Its predecessors were Hoare logic (HL, also known as Floyd-Hoare logic) and its modal version, the dynamic logic (DL). But, since PDL is propositional, it lacks the expressiveness given by first-order constructions found in HL and DL. So, somehow I haven't really been able to find any real example of its original use.

Does anyone know an example of a program and its specifications that I can express and verify for correctness in PDL? I would be happy with any academic or real-world example, or any reference of such an example.

I would even be happy with an example of use of PDL in other areas. Most books that I've seen mention its use in philosophy, artificial intelligence, linguistics etc., but never give an example of this use.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

The practical applications might be more obvious once you observe that these propositional "programs" are regular expressions -- which is to say, state machines. So you can expect it to have applications in the study of things like program analyses and verifying concurrent protocols.

Dexter Kozen at Cornell has done a great deal of work in this area. In fact, he's mostly focused on a subsystem of PDL, called "Kleene algebra with tests", which has an easier decision problem (PSPACE rather than EXPTIME) and tends to have nicer equational proofs.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks, compiler optimizations are just the kind of things I was looking for. $\endgroup$
    – Filip Nikšić
    Commented Nov 20, 2009 at 15:29
0
$\begingroup$

You might find something a little more robust and realistic in the semantics of programs developed by Arbib, Manes, and others of that persuasion.

Give me a while to dig up some references and I'll post them here …

My personal favorite would probably be this:

  • Ernest G. Manes and Michael A. Arbib (1986), Algebraic Approaches to Program Semantics, Springer-Verlag, New York, NY.

There may be newer editions …

Here are some excerpts that I made for use in connection with the IEEE Ontology List and Standard Upper Ontology Working Group, back when we were discussing program semantics and the "ontology of programs" or some such thing:

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .