**This is an old revision of the document!**


  • Write temporal logic properties
  • Master the semantics of temporal logic


  1. (12 points) For the transition system, which states satisfy the formulas. L(s1) = {a}. L(s2) = {a}. L(s3) = {a,b}. L(s4) = {b}. s1 → s2. s2 → s3. s3 → s1. s4 → s2. s3 and s4 are initial states.
    1. X a
    2. XXX a
    3. [] b
    4. []<>a
    5. [](b U a)
    6. <>(b U a)
  2. (12 points) This problem is Exercise 5.5 in Principles of Model Checking (page 321 of the PDF document), consider an elevator system that services N > 0 floors numbered 0 through N-1. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. For simplicity, consider N=4. Present a set of atomic propositions-try to minimize that set-that are needed to describe the following properties of the elevator as LTL formulae and give the LTL formulae:
    1. Any door on any floor is never open when the elevator is not present
    2. A requested floor will be served eventually
    3. The elevator repeatedly returns to floor 0
    4. When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up
cs-486/homework-7.1487699974.txt.gz · Last modified: 2017/02/21 17:59 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0