Kleene Star Operator

Appeared in Volume 9/2, May 1996

ceh@medusa.sce.carleton.ca
Curtis Hrischuk
1st February 1996

Has someone talked about integrating a Kleene star operator with first order logic. The Kleene star operator would operate as follow: (P1)*(P2) is interpreted as the predicate P1 occurring zero, one, or an infinite amount of times until predicate P2 is true.

This is useful if I am examining a list of facts trying to see if a specific sequence exists. It is also interesting if P1 is a composite of several predicates.

I can code this up in Prolog but I don't know how to formally specify it in first order logic. Has anyone else done this work?

rbj@campion.demon.co.uk
Roger Bishop Jones
2nd February 1996

It's doubtful that this can be done in first order logic, in which it would not be materially different from P1 /\ P2.

Presumably, it is only of interest in Prolog because of the side effects arising from evaluation of P1, and hence differs from P1, P2 only because of the impurities of Prolog, which are not present in first order logic.

You might do better with temporal logic if you want a clean way to say things like that, though a plain temporal logic may be too limited for your other requirements.

You could probably do it in higher order logic, where the temporal notions could be modelled, if the temporal bits really are a part of what you want to say.

If side effects are crucial, then higher order logic retains the first order defects, though it is possible to treat languages with side effects in higher order logic using some kind of embedded denotational semantics.

My home page URL is: http://www.cybercom.net/~rbjones/

uli@cantor.informatik.rwth-aachen.de
Ulrike Sattler
2 February 1996

See the semantics of the "until" operator in Time Logic (Logic of time as a part of Modal Logic). I think this is exactly what you are looking for, and more precise because the temporal structure is specified (whether "time" may branch, whether it is dense, etc). There are some nice articles on these issues by Halpern, Moses, Emerson, etc.

hostuart@fit.qut.edu.au
Chris Ho-Stuart
8th February 1996

What you are describing appears to be the "until" modal connective of temporal logic, assuming P1 is a predicate true at a particular world. There are a number of texts on temporal logic which should discuss this connective.

There has also been work done on a modal operator corresponding more closely to the Kleene star, in which P1 is a predicate true for a sequence of worlds, and P1* is true for a number of those sequences appended together ("choppy" logic).

Ben-Ari and Kono have developed the Tempura programming language, based on an interval temporal logic, which you should have a look at. I think it is implemented in Prolog. There are some books available.

In modal logic, you need to be a bit careful about how first order quantification works.

Some references:

Pnueli "Applications of Temporal Logic to the Specification and Verification of Reactive Systems", LNCS 224, pp.510-584, 1986

Barrigner, Kuiper, Pnueli "Now you may Compose Temporal Logic Specifications", Proc 16th ACM Symp on Theory of Computing, pp.51-63, 1984

Gurevich "Monadic Second Order Theories", pp.479-506, Springer-Verlag, 1985

Stuart "Regular Expressions as Temporal Logic", Tech Report, Monash Uni., Australia, 1986

Wolper "Temporal Logic can be More Expressive", Inf. and Control Vol. 56, pp.72-99, 1983

goldman@src.honeywell.com
Robert P. Goldman
12th February 1996

I was waiting for someone to mention dynamic logic: a modal logic whose modality corresponds to the execution of programs. You may find information about it in the "Handbook of Theoretical Computer Science" or Gabbay's "Handbook on Philosophical Logic". The latter article, by Harel, is my favorite of the two.

David Harel, Dynamic Logic, Handbook of Philosophical Logic, D. Reidel Publishing Company, 1984, D. Gabbay and F. Guenther (eds.), Chapter II.10, Vol. II, pp.497--604

Jan vanLeeuwen (ed.), Handbook of Theoretical Computer Science, MIT Press, 1990, Vol. B: Formal Models