In Dijkstra's do-od construct using guarded command we state that the selection of guards is nondeterministic. Can we write logical expression(s) to describe this statement? Can probabilistic logic solve this problem?
I think probabilistic logic will bring no contribution, because no probabilities are involved in the do-od construct.
Nondeterminism can be expressed in the CTL temporal logic using the "E" path quantifier.
You may want to look at the "unified theories of programming" (UTP, originally by Tony Hoare and He Jifeng, now extended to an ever broader range of programming concepts by Jeff Sanders, Andrew Butterfield, and many more) and their precursors by Eric Hehner ("Predicative Programming") and Tony Hoare ("Programs are Predicates"). These explain how such concepts like non-deterministic choice can be given a predicative semantics.
The UTP book is now free online at http://unifyingtheories.org/
Basically non-determinism is modelled as logical disjunction.
So if P and Q are predicates describing the behaviour of two programs, then
P \/ Q is the non-deterministic choice between them.
I will go read the UTP book, but this answer made me wonder about the kind of restricted non-determinism we see in Petri nets: we can have enabled transitions P or Q firing, but not both, and that doesn't seem quite like logical disjunction, which presumably also allows P and Q in addition to P alone and Q alone
I think Exclusive Or may be an answer to allow only one. But does this explicitly specifies nondeterminism?
As UTP-style semantics specify, a.o., the post states (or actually, a pre-post relation), the situation that both P and Q fire can hardly ever arise when specifying the semantics as P or Q, as this would require equivalent post states for P and Q. While such situtaions certainly can arise when only considering the plain process state, they can be avoided by appropriate state encoding and vanish when adding history-recording derived states to the predicative semantics, like recorded traces. Those derived states may not be particularly elegant, but resolve the issue.
- Badges
- Science topic
- Similar topics
- Engineering
- Control Theory