Goal:
Temporal Logic / Specification Patterns.
This assignment is a paper/pencil exercise only.
Use the KSU slides covered in the lecture as
a resource to help you formulate the following in CTL.
You should use the variables listed in typewriter font
as your primitive propositions.
started
holds, but
ready
does not hold.
request
(of some resource) occurs,
then it will eventually be
acknowledged
.
enabled
infinitely often on every computation path.
deadlocked
.
restart
state.
direction == up
,
floor == 2
,
and
Button5Pressed
.